Document Open Access Logo

Time for Timed Monitorability

Authors Thomas M. Grosen , Sean Kauffman , Kim G. Larsen , Martin Zimmermann

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.19.pdf
  • Filesize: 1.05 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Modal and temporal logics
Keywords
  • Monitorability
  • Monitoring
  • Timed Automata
  • MITL

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Monitoring is an important part of the verification toolbox, in particular in situations where exhaustive verification using, e.g., model-checking is infeasible. The goal of online monitoring is to determine the satisfaction or violation of a specification during runtime, i.e., based on finite execution prefixes. However, not every specification is amenable to monitoring, e.g., properties for which no finite execution can witness satisfaction or violation. Monitorability is the question of whether a given specification is amenable to monitoring, and has been extensively studied in discrete time.
Here, we study the monitorability problem for real-time properties expressed as Timed Automata. For specifications given by deterministic Timed Muller Automata, we prove decidability while we show that the problem is undecidable for specifications given by nondeterministic Timed Büchi automata. 
Furthermore, we refine monitorability to also determine bounds on the number of events as well as the time that must pass before monitoring the property may yield an informative verdict. We prove that for deterministic Timed Muller automata, such bounds can be effectively computed. In contrast we show that for nondeterministic Timed Büchi automata such bounds are not computable.

Cite As Get BibTex

Thomas M. Grosen, Sean Kauffman, Kim G. Larsen, and Martin Zimmermann. Time for Timed Monitorability. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 19:1-19:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.19

Author Details

Thomas M. Grosen
  • Aalborg University, Aalborg, Denmark
Sean Kauffman
  • Queen’s University, Kingston, Canada
Kim G. Larsen
  • Aalborg University, Aalborg, Denmark
Martin Zimmermann
  • Aalborg University, Aalborg, Denmark

Funding

T. M. Grosen and K. G. Larsen have been funded by the Villum Investigator Grant S4OS. T. M. Grosen, K. G. Larsen, and M. Zimmermann have been supported by DIREC - Digital Research Centre Denmark. T. M. Grosen has been supported by Mitacs. S. Kauffman has been supported by the Natural Sciences and Engineering Research Council of Canada.

Acknowledgements

We would like to thank Corto Mascle, who brought Rampersad et al.’s work on the complexity of suffix-universality [Narad Rampersad et al., 2012] to our attention, which inspired our undecidability proof for weak monitorability.

References

  1. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. Adventures in monitorability: From branching to linear time and back again. In Symposium on Principles of Programming Languages (POPL'19), volume 3. ACM, January 2019. URL: https://doi.org/10.1145/3290365.
  2. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. An operational guide to monitorability with applications to regular properties. Software and Systems Modeling, 20(2):335-361, April 2021. URL: https://doi.org/10.1007/s10270-020-00860-z.
  3. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  4. Rajeev Alur, Tomás Feder, and Thomas A. Henzinger. The benefits of relaxing punctuality. J. ACM, 43(1):116-146, 1996. URL: https://doi.org/10.1145/227595.227602.
  5. Rajeev Alur and P. Madhusudan. Decision problems for timed automata: A survey. In Formal Methods for the Design of Real-Time Systems: International School on Formal Methods for the Design of Computer, Communication, and Software Systems, volume 3185 of LNCS, pages 1-24. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30080-9_1.
  6. Mouloud Amara, Giovanni Bernardi, Mohammed Foughali, and Adrian Francalanza. A theory of (linear-time) timed monitors. In 39th European Conference on Object-Oriented Programming (ECOOP 2025), volume 333, Bergen (NO), Norway, June 2025. URL: https://hal.science/hal-05043055.
  7. Eugene Asarin and Oded Maler. As soon as possible: Time optimal control for timed automata. In Frits W. Vaandrager and Jan H. van Schuppen, editors, Hybrid Systems: Computation and Control, Second International Workshop, HSCC'99, Berg en Dal, The Netherlands, March 29-31, 1999, Proceedings, volume 1569 of LNCS, pages 19-30. Springer, 1999. URL: https://doi.org/10.1007/3-540-48983-5_6.
  8. David Basin, Felix Klaedtke, and Eugen Zălinescu. Algorithms for monitoring real-time properties. In Runtime Verification, pages 260-275. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-29860-8_20.
  9. Andreas Bauer, Martin Leucker, and Christian Schallhart. Monitoring of real-time properties. In Foundations of Software Technology and Theoretical Computer Science, pages 260-272, Berlin, Heidelberg, 2006. Springer. URL: https://doi.org/10.1007/11944836_25.
  10. Andreas Bauer, Martin Leucker, and Christian Schallhart. Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (TOSEM), 20(4):14:1-14:64, September 2011. URL: https://doi.org/10.1145/2000799.2000800.
  11. Johan Bengtsson and Wang Yi. Timed automata: Semantics, algorithms and tools. In Jörg Desel, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Lectures on Concurrency and Petri Nets, Advances in Petri Nets [This tutorial volume originates from the 4th Advanced Course on Petri Nets, ACPN 2003, held in Eichstätt, Germany in September 2003. In addition to lectures given at ACPN 2003, additional chapters have been commissioned], volume 3098 of Lecture Notes in Computer Science, pages 87-124. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-27755-2_3.
  12. Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, and Benjamin Monmege. MightyL: A compositional translation from MITL to timed automata. In Rupak Majumdar and Viktor Kuncak, editors, CAV 2017, Part I, volume 10426 of LNCS, pages 421-440, Cham, 2017. Springer. URL: https://doi.org/10.1007/978-3-319-63387-9_21.
  13. Zhe Chen, Yifan Wu, Ou Wei, and Bin Sheng. Deciding weak monitorability for runtime verification. In Int. Conference on Software Engineering (ICSE'18), pages 163-164. ACM, 2018. URL: https://doi.org/10.1145/3183440.3195077.
  14. Alessandro Cimatti, Thomas Møller Grosen, Kim G. Larsen, Stefano Tonetta, and Martin Zimmermann. Exploiting assumptions for effective monitoring of real-time properties under partial observability. In Alexandre Madeira and Alexander Knapp, editors, SEFM, volume 15280 of LNCS, pages 70-88. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-77382-2_5.
  15. Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal logics for hyperproperties. In Int. Conference on Principles of Security and Trust (POST'14), volume 8414 of LNCS, pages 265-284. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54792-8_15.
  16. Volker Diekert and Martin Leucker. Topology, monitorable properties and runtime verification. Theoretical Computer Science, 537:29-41, 2014. URL: https://doi.org/10.1016/j.tcs.2014.02.052.
  17. Volker Diekert and Anca Muscholl. On distributed monitoring of asynchronous systems. In Logic, Language, Information and Computation, volume 7456 of LNTCS, pages 70-84. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32621-9_5.
  18. Volker Diekert, Anca Muscholl, and Igor Walukiewicz. A note on monitors and Büchi automata. In Theoretical Aspects of Computing - ICTAC 2015, volume 9399 of LNTCS, pages 39-57. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-25150-9_3.
  19. Adrian Francalanza, Luca Aceto, and Anna Ingolfsdottir. Monitorability for the Hennessy-Milner logic with recursion. Formal Methods in System Design, 51(1):87-116, August 2017. URL: https://doi.org/10.1007/s10703-017-0273-z.
  20. Martin Fränzle, Thomas Møller Grosen, Kim G. Larsen, and Martin Zimmermann. Monitoring real-time systems under parametric delay. In Nikolai Kosmatov and Laura Kovács, editors, IFM 2024, volume 15234 of LNCS, pages 194-213. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-76554-4_11.
  21. Kalpana Gondi, Yogeshkumar Patel, and A. Prasad Sistla. Monitoring the full range of ω-regular properties of stochastic systems. In Neil D. Jones and Markus Müller-Olm, editors, Verification, Model Checking, and Abstract Interpretation, pages 105-119, Berlin, Heidelberg, 2009. Springer. URL: https://doi.org/10.1007/978-3-540-93900-9_12.
  22. Thomas Møller Grosen, Sean Kauffman, Kim G. Larsen, and Martin Zimmermann. Time for timed monitorability. arXiv, 2504.10008, 2025. URL: https://doi.org/10.48550/arXiv.2504.10008.
  23. Thomas Møller Grosen, Sean Kauffman, Kim Guldstrand Larsen, and Martin Zimmermann. Monitoring timed properties (revisited). In Sergiy Bogomolov and David Parker, editors, FORMATS 2022, volume 13465 of LNCS, pages 43-62. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-15839-1_3.
  24. Sean Kauffman, Klaus Havelund, and Sebastian Fischmeister. What can we monitor over unreliable channels? International Journal on Software Tools for Technology Transfer, 23:579-600, June 2021. URL: https://doi.org/10.1007/s10009-021-00625-z.
  25. Kim Guldstrand Larsen, Marius Mikucionis, and Brian Nielsen. Online testing of real-time systems using uppaal. In Formal Approaches to Software Testing, volume 3395 of LNCS, pages 79-94. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-31848-4_6.
  26. N.G. Leveson and C.S. Turner. An investigation of the therac-25 accidents. Computer, 26(7):18-41, 1993. URL: https://doi.org/10.1109/MC.1993.274940.
  27. Corto Mascle, Daniel Neider, Maximilian Schwenger, Paulo Tabuada, Alexander Weinert, and Martin Zimmermann. From LTL to rltl monitoring: improved monitorability through robust semantics. Formal Methods Syst. Des., 59(1):170-204, 2021. URL: https://doi.org/10.1007/S10703-022-00398-4.
  28. Doron Peled and Klaus Havelund. Refining the safety-liveness classification of temporal properties according to monitorability. In Models, Mindsets, Meta: The What, the How, and the Why Not? Essays Dedicated to Bernhard Steffen on the Occasion of His 60th Birthday, volume 11200 of LNCS, pages 218-234. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-22348-9_14.
  29. A. Pnueli and A. Zaks. PSL model checking and run-time verification via testers. In Jayadev Misra, Tobias Nipkow, and Emil Sekerinski, editors, FM 2006: Formal Methods, pages 573-586, Berlin, Heidelberg, 2006. Springer. URL: https://doi.org/10.1007/11813040_38.
  30. Narad Rampersad, Jeffrey O. Shallit, and Zhi Xu. The computational complexity of universality problems for prefixes, suffixes, factors, and subwords of regular languages. Fundam. Informaticae, 116(1-4):223-236, 2012. URL: https://doi.org/10.3233/FI-2012-680.
  31. Fred B. Schneider. Enforceable security policies. ACM Trans. Inf. Syst. Secur., 3(1):30-50, February 2000. URL: https://doi.org/10.1145/353323.353382.
  32. A. Prasad Sistla, Miloš Žefran, and Yao Feng. Monitorability of stochastic dynamical systems. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification, pages 720-736, Berlin, Heidelberg, 2011. Springer. URL: https://doi.org/10.1007/978-3-642-22110-1_58.
  33. Alfred Tarski. A decision method for elementary algebra and geometry. In Bob F. Caviness and Jeremy R. Johnson, editors, Quantifier Elimination and Cylindrical Algebraic Decomposition, pages 24-84, Vienna, 1998. Springer Vienna. Google Scholar
  34. Prasanna Thati and Grigore Roşu. Monitoring algorithms for metric temporal logic specifications. Electronic Notes in Theoretical Computer Science, 113:145-162, 2005. URL: https://doi.org/10.1016/j.entcs.2004.01.029.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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