Document Open Access Logo

Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory

Authors Luca Aceto , Antonis Achilleos , Duncan Paul Attard , Léo Exibard , Adrian Francalanza , Anna Ingólfsdóttir , Karoliina Lehtinen

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.4.pdf
  • Filesize: 0.97 MB
  • 21 pages
HTML5 Logo HTML (experimental)
LIPIcs.CONCUR.2025.4.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Automata over infinite objects
Keywords
  • Runtime verification
  • monitorability
  • μHML with data
  • register automata

Metrics

Abstract

Runtime verification consists in checking whether a system satisfies a given specification by observing the execution trace it produces. In the regular setting, the modal μ-calculus provides a versatile formalism for expressing specifications of the control flow of the system. This paper focuses on the data flow and studies an extension of that logic that allows it to express data-dependent properties, identifying fragments that can be verified at runtime and with what correctness guarantees. The logic studied here is closely related with register automata with guessing. That correspondence yields a monitor synthesis algorithm, and a strict hierarchy among the various fragments of the logic, in contrast to the regular setting. We then exhibit a fragment of the logic that can express all monitorable formulae in the logic without greatest fixed-points but not in the full logic, and show this is the best we can get.

Cite As Get BibTex

Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.4

Author Details

Luca Aceto
  • Dept. of Computer Science, Reykjavik University, Iceland
  • Gran Sasso Science Institute, L'Aquila, Italy
Antonis Achilleos
  • Dept. of Computer Science, Reykjavik University, Iceland
Duncan Paul Attard
  • University of Malta, Msida, Malta
Léo Exibard
  • LIGM, CNRS, Univ Gustave Eiffel, F77454 Marne-la-Vallée, France
Adrian Francalanza
  • University of Malta, Msida, Malta
Anna Ingólfsdóttir
  • Dept. of Computer Science, Reykjavik University, Iceland
Karoliina Lehtinen
  • CNRS, Aix-Marseille University, LIS, Marseille, France

References

  1. Luca Aceto, Antonis Achilleos, Elli Anastasiadi, Adrian Francalanza, and Anna Ingólfsdóttir. Complexity results for modal logic with recursion via translations and tableaux. Logical Methods in Computer Science, Volume 20, Issue 3, August 2024. URL: https://doi.org/10.46298/lmcs-20(3:14)2024.
  2. Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, and Anna Ingólfsdóttir. A monitoring tool for linear-time μHML. Sci. Comput. Program., 232:103031, 2024. URL: https://doi.org/10.1016/J.SCICO.2023.103031.
  3. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Sævar Örn Kjartansson. Determinizing monitors for HML with recursion. J. Log. Algebraic Methods Program., 111:100515, 2020. URL: https://doi.org/10.1016/J.JLAMP.2019.100515.
  4. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. Adventures in monitorability: from branching to linear time and back again. Proc. ACM Program. Lang., 3(POPL):52:1-52:29, 2019. URL: https://doi.org/10.1145/3290365.
  5. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. The best a monitor can do. In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference), volume 183 of LIPIcs, pages 7:1-7:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.7.
  6. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. An operational guide to monitorability with applications to regular properties. Softw. Syst. Model., 20(2):335-361, 2021. URL: https://doi.org/10.1007/s10270-020-00860-z.
  7. Luca Aceto, Ian Cassar, Adrian Francalanza, and Anna Ingólfsdóttir. On Runtime Enforcement via Suppressions. In CONCUR, volume 118 of LIPIcs, pages 34:1-34:17, 2018. URL: https://doi.org/10.4230/LIPICS.CONCUR.2018.34.
  8. Chris Allan, Pavel Avgustinov, Aske Simon Christensen, Laurie J. Hendren, Sascha Kuzins, Ondrej Lhoták, Oege de Moor, Damien Sereni, Ganesh Sittampalam, and Julian Tibble. Adding trace matching with free variables to AspectJ. In Ralph E. Johnson and Richard P. Gabriel, editors, Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2005, October 16-20, 2005, San Diego, CA, USA, pages 345-364. ACM, 2005. URL: https://doi.org/10.1145/1094811.1094839.
  9. Bowen Alpern and Fred B. Schneider. Recognizing safety and liveness. Distributed Comput., 2(3):117-126, 1987. URL: https://doi.org/10.1007/BF01782772.
  10. Krzysztof R. Apt and Gordon D. Plotkin. Countable nondeterminism and random assignment. J. ACM, 33(4):724-767, 1986. URL: https://doi.org/10.1145/6490.6494.
  11. Howard Barringer, Yliès Falcone, Klaus Havelund, Giles Reger, and David E. Rydeheard. Quantified event automata: Towards expressive and efficient runtime monitors. In Dimitra Giannakopoulou and Dominique Méry, editors, FM 2012: Formal Methods - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings, volume 7436 of Lecture Notes in Computer Science, pages 68-84. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32759-9_9.
  12. Howard Barringer, Allen Goldberg, Klaus Havelund, and Koushik Sen. Rule-based runtime verification. In Bernhard Steffen and Giorgio Levi, editors, Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings, volume 2937 of Lecture Notes in Computer Science, pages 44-57. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24622-0_5.
  13. Howard Barringer, David E. Rydeheard, and Klaus Havelund. Rule systems for run-time monitoring: From Eagle to RuleR. In Oleg Sokolsky and Serdar Tasiran, editors, Runtime Verification, 7th International Workshop, RV 2007, Vancouver, Canada, March 13, 2007, Revised Selected Papers, volume 4839 of Lecture Notes in Computer Science, pages 111-125. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-77395-5_10.
  14. Ezio Bartocci, Yliès Falcone, Adrian Francalanza, and Giles Reger. Introduction to Runtime Verification. In Lectures on Runtime Verification: Introductory and Advanced Topics, volume 10457 of LNCS, pages 1-33. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-75632-5_1.
  15. David A. Basin, Felix Klaedtke, and Samuel Müller. Policy monitoring in first-order temporal logic. In Tayssir Touili, Byron Cook, and Paul B. Jackson, editors, Computer Aided Verification, 22nd International Conference, CAV2010, Edinburgh, UK, July 15-19, 2010. Proceedings, volume 6174 of Lecture Notes in Computer Science, pages 1-18. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14295-6_1.
  16. Andreas Bauer, Jan-Christoph Küster, and Gil Vegliach. From propositional to first-order monitoring. In Axel Legay and Saddek Bensalem, editors, Runtime Verification - 4th International Conference, RV 2013, Rennes, France, September 24-27, 2013. Proceedings, volume 8174 of Lecture Notes in Computer Science, pages 59-75. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40787-1_4.
  17. Henrik Björklund and Thomas Schwentick. On notions of regularity for data languages. Theor. Comput. Sci., 411(4-5):702-715, 2010. URL: https://doi.org/10.1016/j.tcs.2009.10.009.
  18. Mikołaj Bojańczyk. Slightly infinite sets, 2019. URL: https://www.mimuw.edu.pl/~bojan/paper/atom-book.
  19. Mikolaj Bojanczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. ACM Trans. Comput. Log., 12(4):27:1-27:26, 2011. URL: https://doi.org/10.1145/1970398.1970403.
  20. Benedikt Bollig, Aiswarya Cyriac, Paul Gastin, and K. Narayan Kumar. Model checking languages of data words. In Lars Birkedal, editor, Foundations of Software Science and Computational Structures, pages 391-405, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-28729-9_26.
  21. Julian C. Bradfield and Colin Stirling. Modal mu-calculi. In Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors, Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning, pages 721-756. North-Holland, 2007. URL: https://doi.org/10.1016/S1570-2464(07)80015-2.
  22. Randal E. Bryant. Binary decision diagrams. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 191-217. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_7.
  23. Feng Chen and Grigore Rosu. Parametric trace slicing and monitoring. In Stefan Kowalewski and Anna Philippou, editors, Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5505 of Lecture Notes in Computer Science, pages 246-261. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00768-2_23.
  24. Mads Dam. CTL* and ECTL* as fragments of the modal μ-calculus. Theoretical Computer Science, 126(1):77-96, 1994. URL: https://doi.org/10.1016/0304-3975(94)90269-0.
  25. Mads Dam. Temporal logic, automata and classical theories. In Proceedings of the 6th European Summer School in Logic, Language and Information (ESSLLI'94), August 1994. Google Scholar
  26. Marcelo d'Amorim and Grigore Rosu. Efficient monitoring of omega-languages. In Kousha Etessami and Sriram K. Rajamani, editors, Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings, volume 3576 of Lecture Notes in Computer Science, pages 364-378. Springer, 2005. URL: https://doi.org/10.1007/11513988_36.
  27. Loris D'Antoni. In the maze of data languages. CoRR, abs/1208.5980, 2012. URL: https://arxiv.org/abs/1208.5980.
  28. Normann Decker, Martin Leucker, and Daniel Thoma. Monitoring modulo theories. Int. J. Softw. Tools Technol. Transf., 18(2):205-225, 2016. URL: https://doi.org/10.1007/S10009-015-0380-3.
  29. Stéphane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log., 10(3):16:1-16:30, 2009. URL: https://doi.org/10.1145/1507244.1507246.
  30. Stéphane Demri, Ranko Lazic, and David Nowak. On the freeze quantifier in constraint LTL: decidability and complexity. Inf. Comput., 205(1):2-24, 2007. URL: https://doi.org/10.1016/j.ic.2006.08.003.
  31. Rüdiger Ehlers, Sanjit A. Seshia, and Hadas Kress-Gazit. Synthesis with identifiers. In Kenneth L. McMillan and Xavier Rival, editors, Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings, volume 8318 of Lecture Notes in Computer Science, pages 415-433. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54013-4_23.
  32. E. Allen Emerson. Temporal and modal logic. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pages 995-1072. Elsevier and MIT Press, 1990. URL: https://doi.org/10.1016/b978-0-444-88074-1.50021-4.
  33. Léo Exibard, Emmanuel Filiot, and Pierre-Alain Reynier. Synthesis of data word transducers. Logical Methods in Computer Science, 17(1), 2021. URL: https://lmcs.episciences.org/7279.
  34. Yliès Falcone, Srdan Krstic, Giles Reger, and Dmitriy Traytel. A taxonomy for classifying runtime verification tools. Int. J. Softw. Tools Technol. Transf., 23(2):255-284, 2021. URL: https://doi.org/10.1007/S10009-021-00609-Z.
  35. Diego Figueira. Reasoning on words and trees with data. (Raisonnement sur mots et arbres avec données). PhD thesis, École normale supérieure de Cachan, France, 2010. URL: https://tel.archives-ouvertes.fr/tel-00718605.
  36. Diego Figueira. Alternating register automata on finite words and trees. Log. Methods Comput. Sci., 8(1), 2012. URL: https://doi.org/10.2168/LMCS-8(1:22)2012.
  37. Diego Figueira, Piotr Hofman, and Slawomir Lasota. Relating timed and register automata. Math. Struct. Comput. Sci., 26(6):993-1021, 2016. URL: https://doi.org/10.1017/S0960129514000322.
  38. Diego Figueira, Anirban Majumdar, and M. Praveen. Playing with repetitions in data words using energy games. Log. Methods Comput. Sci., 16(3), 2020. URL: https://lmcs.episciences.org/6614.
  39. Bernd Finkbeiner, Felix Klein, Ruzica Piskac, and Mark Santolucito. Temporal stream logic: Synthesis beyond the bools. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, volume 11561 of Lecture Notes in Computer Science, pages 609-629. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-25540-4_35.
  40. Radu Grigore, Dino Distefano, Rasmus Lerchedahl Petersen, and Nikos Tzevelekos. Runtime verification based on register automata. In Nir Piterman and Scott A. Smolka, editors, Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, volume 7795 of Lecture Notes in Computer Science, pages 260-276. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-36742-7_19.
  41. Jan Friso Groote and Radu Mateescu. Verification of temporal properties of processes in a setting with data. In Armando Martin Haeberer, editor, Algebraic Methodology and Software Technology, 7th International Conference, AMAST '98, Amazonia, Brasil, January 4-8, 1999, Proceedings, volume 1548 of Lecture Notes in Computer Science, pages 74-90. Springer, 1998. URL: https://doi.org/10.1007/3-540-49253-4_8.
  42. Klaus Havelund and Doron Peled. Efficient runtime verification of first-order temporal properties. In María-del-Mar Gallardo and Pedro Merino, editors, Model Checking Software - 25th International Symposium, SPIN 2018, Malaga, Spain, June 20-22, 2018, Proceedings, volume 10869 of Lecture Notes in Computer Science, pages 26-47. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94111-0_2.
  43. Klaus Havelund, Giles Reger, Daniel Thoma, and Eugen Zalinescu. Monitoring events that carry data. In Ezio Bartocci and Yliès Falcone, editors, Lectures on Runtime Verification - Introductory and Advanced Topics, volume 10457 of Lecture Notes in Computer Science, pages 61-102. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-75632-5_3.
  44. Hsi-Ming Ho, Joël Ouaknine, and James Worrell. Online monitoring of metric temporal logic. In Borzoo Bonakdarpour and Scott A. Smolka, editors, Runtime Verification - 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings, volume 8734 of Lecture Notes in Computer Science, pages 178-192. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11164-3_15.
  45. Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994. URL: https://doi.org/10.1016/0304-3975(94)90242-9.
  46. Marcin Jurdzinski and Ranko Lazic. Alternation-free modal mu-calculus for data trees. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings, pages 131-140. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/LICS.2007.11.
  47. Patrick O'Neil Meredith, Dongyun Jin, Dennis Griffith, Feng Chen, and Grigore Rosu. An overview of the MOP runtime verification framework. Int. J. Softw. Tools Technol. Transf., 14(3):249-289, 2012. URL: https://doi.org/10.1007/S10009-011-0198-6.
  48. Robin Milner. Is computing an experimental science? J. Inf. Technol., 2(2):58-66, 1987. URL: https://doi.org/10.1057/JIT.1987.12.
  49. Frank Neven, Thomas Schwentick, and Victor Vianu. Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log., 5(3):403-435, 2004. URL: https://doi.org/10.1145/1013560.1013562.
  50. Amir Pnueli and Aleksandr Zaks. PSL model checking and run-time verification via testers. In Jayadev Misra, Tobias Nipkow, and Emil Sekerinski, editors, FM 2006: Formal Methods, 14th International Symposium on Formal Methods, volume 4085 of Lecture Notes in Computer Science, pages 573-586. Springer, 2006. URL: https://doi.org/10.1007/11813040_38.
  51. Luc Segoufin. Automata and logics for words and trees over an infinite alphabet. In Zoltán Ésik, editor, Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings, volume 4207 of Lecture Notes in Computer Science, pages 41-57. Springer, 2006. URL: https://doi.org/10.1007/11874683_3.
  52. Robert S. Streett and E. Allen Emerson. An automata theoretic decision procedure for the propositional mu-calculus. Information and Computation, 81(3):249-264, 1989. URL: https://doi.org/10.1016/0890-5401(89)90031-X.
  53. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5(2):285-309, 1955. URL: https://doi.org/10.2140/pjm.1955.5.285.
  54. Moshe Y. Vardi. A temporal fixpoint calculus. In Jeanne Ferrante and Peter Mager, editors, Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, California, USA, January 10-13, 1988, pages 250-259. ACM Press, 1988. URL: https://doi.org/10.1145/73560.73582.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact