Document Open Access Logo

A Theory of (Linear-Time) Timed Monitors

Authors Mouloud Amara, Giovanni Bernardi , Mohammed Aristide Foughali , Adrian Francalanza

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2025.1.pdf
  • Filesize: 1.14 MB
  • 30 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Timed logics
  • Runtime Verification
  • Monitorability

Metrics

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

Abstract

Runtime Verification (RV) is gaining popularity due to its scalability and ability to analyse block-box systems. Monitoring is at the heart of RV; a logical formula ϕ, formalising some property of interest, is typically translated into a monitor that checks whether the system under scrutiny satisfies ϕ during its execution. A logical formula ϕ is violation (resp. satisfaction) monitorable iff there exists a monitor for ϕ that is both sound and complete w.r.t. its violation (resp. satisfaction). The monitorability problem is thus concerned with determining the largest subset of a logic L that is monitorable. Although this problem has been solved for expressive untimed logics, it remains open for timed logics, where formulae can express both the order of events and the quantity of time separating them. This paper solves the monitorability problem for T^lin, a new expressive (linear-time) timed μ-calculus that we propose. First, we show that T^lin is strictly more expressive than MTL, the de facto timed extension of LTL. Second, we identify MT^lin, the largest monitorable fragment of T^lin: we characterise its largest subsets of formulae that are violation monitorable, satisfaction monitorable, and complete monitorable (both satisfaction and violation monitorable). To wit, this is the first work that answers the monitorability question for such an expressive timed logic.

Cite As Get BibTex

Mouloud Amara, Giovanni Bernardi, Mohammed Aristide Foughali, and Adrian Francalanza. A Theory of (Linear-Time) Timed Monitors. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 1:1-1:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ECOOP.2025.1

Author Details

Mouloud Amara
  • Université Paris Cité, CNRS, IRIF, F-75013 Paris, France
Giovanni Bernardi
  • Université Paris Cité, CNRS, IRIF, F-75013 Paris, France
Mohammed Aristide Foughali
  • Université Paris Cité, CNRS, IRIF, F-75013 Paris, France
Adrian Francalanza
  • Dept. of Computer Science, ICT, University of Malta, Msida, Malta

Funding

This work has received support under the program "Investissement d’Avenir" launched by the French Government and implemented by ANR, with the reference "ANR-18-IdEx-000" as part of its program "Émergence". Other fundings include the ANR-JST Grant CyPhAI as well as the ANR project MAVEriQ.

Supplementary Materials

References

  1. L. Aceto, A. Ingólfsdóttir, K. G. Larsen, and J. Srba. Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007. Google Scholar
  2. 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.
  3. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. An operational guide to monitorability. In International Conference on Software Engineering and Formal Methods (SEFM), pages 433-453. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-30446-1_23.
  4. 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:335-361, 2021. URL: https://doi.org/10.1007/s10270-020-00860-z.
  5. 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.
  6. Rajeev Alur and Thomas A Henzinger. Real-time logics: complexity and expressiveness. Information and Computation, 104(1):35-77, 1993. URL: https://doi.org/10.1006/inco.1993.1025.
  7. Rajeev Alur and Thomas A Henzinger. A really temporal logic. Journal of the ACM (JACM), 41(1):181-203, 1994. URL: https://doi.org/10.1145/174644.174651.
  8. Rajeev Alur and Thomas A Henzinger. Modularity for timed and hybrid systems. In International Conference on Concurrency Theory (CONCUR), pages 74-88. Springer, 1997. URL: https://doi.org/10.1007/3-540-63141-0_6.
  9. Kevin Baldor and Jianwei Niu. Monitoring dense-time, continuous-semantics, metric temporal logic. In International Conference on Runtime Verification (RV), pages 245-259. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-35632-2_24.
  10. Ezio Bartocci, Yliès Falcone, Adrian Francalanza, and Giles Reger. Introduction to runtime verification. Lectures on Runtime Verification: Introductory and Advanced Topics, pages 1-33, 2018. URL: https://doi.org/10.1007/978-3-319-75632-5_1.
  11. David A. Basin, Felix Klaedtke, Samuel Müller, and Eugen Zalinescu. Monitoring metric first-order temporal properties. J. ACM, 62(2):15:1-15:45, 2015. URL: https://doi.org/10.1145/2699444.
  12. Andreas Bauer, Martin Leucker, and Christian Schallhart. Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol., 20(4):14:1-14:64, 2011. URL: https://doi.org/10.1145/2000799.2000800.
  13. Edmund Clarke, Orna Grumberg, and Kiyoharu Hamaguchi. Another look at LTL model checking. In International Conference on Computer Aided Verification (CAV), pages 415-427. Springer, 1994. URL: https://doi.org/10.1007/3-540-58179-0_72.
  14. Rance Cleaveland, Jeroen JA Keiren, and Peter Fontana. An expressive timed modal mu-calculus for timed automata. In International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems (QEST+FORMATS), pages 160-178. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-68416-6_10.
  15. Christian Dax, Martin Hofmann, and Martin Lange. A proof system for the linear time μ-calculus. In S. Arun-Kumar and Naveen Garg, editors, International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pages 273-284. Springer, 2006. URL: https://doi.org/10.1007/11944836_26.
  16. Alexandre Donzé and Oded Maler. Robust satisfaction of temporal logic over real-valued signals. In International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), pages 92-106. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15297-9_9.
  17. Mohammed Foughali, Saddek Bensalem, Jacques Combaz, and Félix Ingrand. Runtime verification of timed properties in autonomous robots. In International Conference on Formal Methods and Models for System Design (MEMOCODE), pages 1-12. IEEE, 2020. URL: https://doi.org/10.1109/MEMOCODE51338.2020.9315156.
  18. Mohammed Foughali, Pierre-Emmanuel Hladik, and Alexander Zuepke. Compositional verification of embedded real-time systems. J. Syst. Archit., 142:102928, 2023. URL: https://doi.org/10.1016/j.sysarc.2023.102928.
  19. A. Francalanza, L. Aceto, and A. Ingólfsdóttir. Monitorability for the Hennessy-Milner logic with recursion. Formal Methods Syst. Des., 51(1), 2017. URL: https://doi.org/10.1007/s10703-017-0273-z.
  20. Adrian Francalanza. A theory of monitors. Inf. Comput., 281:104704, 2021. URL: https://doi.org/10.1016/j.ic.2021.104704.
  21. Adrian Francalanza, Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Ian Cassar, Dario Della Monica, and Anna Ingólfsdóttir. A foundation for runtime monitoring. In RV, volume 10548 of Lecture Notes in Computer Science, pages 8-29. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-67531-2_2.
  22. Thomas Møller Grosen, Sean Kauffman, Kim Guldstrand Larsen, and Martin Zimmermann. Monitoring timed properties (revisited). In International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), pages 43-62. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-15839-1_3.
  23. Thomas A Henzinger. Sooner is safer than later. Information Processing Letters, 43(3):135-141, 1992. URL: https://doi.org/10.1016/0020-0190(92)90005-G.
  24. Hsi-Ming Ho, Joël Ouaknine, and James Worrell. Online monitoring of metric temporal logic. In International Conference on Runtime Verification (RV), pages 178-192. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11164-3_15.
  25. Ullrich Hustadt, Ana Ozaki, and Clare Dixon. Theorem proving for pointwise metric temporal logic over the naturals via translations. Journal of Automated Reasoning, 64(8):1553-1610, 2020. URL: https://doi.org/10.1007/s10817-020-09541-4.
  26. Donald Ervin Knuth. Semantics of context-free languages. Mathematical systems theory, 2:127-145, 1968. URL: https://doi.org/10.1007/BF01692511.
  27. Ron Koymans. Specifying real-time properties with metric temporal logic. Real-time systems, 2(4):255-299, 1990. URL: https://doi.org/10.1007/BF01995674.
  28. Dexter Kozen. Results on the propositional μ-calculus. Theoretical computer science, 27(3):333-354, 1983. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  29. Kim G Larsen. Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theoretical Computer Science, 72(2-3):265-288, 1990. URL: https://doi.org/10.1016/0304-3975(90)90038-J.
  30. Martin Leucker and Christian Schallhart. A brief account of runtime verification. The journal of logic and algebraic programming, 78(5):293-303, 2009. URL: https://doi.org/10.1016/j.jlap.2008.08.004.
  31. Orna Lichtenstein and Amir Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Symposium on Principles of Programming Languages (POPL), pages 97-107, 1985. URL: https://doi.org/10.1145/318593.318622.
  32. Leonardo Lima, Andrei Herasimau, Martin Raszyk, Dmitriy Traytel, and Simon Yuan. Explainable online monitoring of metric temporal logic. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 473-491. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30820-8_28.
  33. Frank D Macías-Escrivá, Rodolfo Haber, Raul Del Toro, and Vicente Hernandez. Self-adaptive systems: A survey of current approaches, research challenges and applications. Expert Systems with Applications, 40(18):7267-7279, 2013. URL: https://doi.org/10.1016/j.eswa.2013.07.033.
  34. Oded Maler and Dejan Nickovic. Monitoring temporal properties of continuous signals. In International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT), volume 3253, pages 152-166. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30206-3_12.
  35. Oded Maler, Dejan Nickovic, and Amir Pnueli. On synthesizing controllers from bounded-response properties. In International Conference on Computer Aided Verification (CAV), pages 95-107. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73368-3_12.
  36. Joël Ouaknine and James Worrell. On metric temporal logic and faulty turing machines. In International Conference on Foundations of Software Science and Computation Structures, pages 217-230. Springer, 2006. URL: https://doi.org/10.1007/11690634_15.
  37. Srinivas Pinisetty, Thierry Jéron, Stavros Tripakis, Yliès Falcone, Hervé Marchand, and Viorel Preoteasa. Predictive runtime verification of timed properties. Journal of Systems and Software, 132:353-365, 2017. URL: https://doi.org/10.1016/j.jss.2017.06.060.
  38. Amir Pnueli. The temporal logic of programs. In Annual Symposium on Foundations of Computer Science (SFCS), pages 46-57. ieee, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  39. Amir Pnueli and Aleksandr Zaks. PSL model checking and run-time verification via testers. In International Symposium on Formal Methods (FM), pages 573-586. Springer, 2006. URL: https://doi.org/10.1007/11813040_38.
  40. Vasumathi Raman, Mehdi Maasoumy, and Alexandre Donzé. Model predictive control from signal temporal logic specifications: A case study. In International Workshop on Design, Modeling, and Evaluation of Cyber-Physical Systems, pages 52-55, 2014. URL: https://doi.org/10.1145/2593458.2593472.
  41. Martin Raszyk, David Basin, Srđan Krstić, and Dmitriy Traytel. Multi-head monitoring of metric temporal logic. In International Symposium on Automated Technology for Verification and Analysis (ATVA), pages 151-170. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_9.
  42. Neha Rino, Mohammed Foughali, and Eugene Asarin. Efficiently computable distance-based robustness for a practical fragment of STL. In International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems (QEST+FORMATS), pages 179-195. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-68416-6_11.
  43. Victor Roussanaly and Yliès Falcone. Decentralised runtime verification of timed regular expressions. In International Symposium on Temporal Representation and Reasoning (TIME), pages 6:1-6:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.TIME.2022.6.
  44. Fred B. Schneider. Enforceable security policies. ACM Trans. Inf. Syst. Secur., 3(1):30-50, 2000. URL: https://doi.org/10.1145/353323.353382.
  45. 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.
  46. Dogan Ulus, Thomas Ferrère, Eugene Asarin, and Oded Maler. Online timed pattern matching using derivatives. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 736-751. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49674-9_47.
  47. Moshe Y Vardi. An automata-theoretic approach to linear temporal logic. Logics for concurrency: structure versus automata, pages 238-266, 2005. Google Scholar
  48. Pierre Wolper. Temporal logic can be more expressive. In Annual Symposium on Foundations of Computer Science (SFCS), pages 340-348. IEEE Computer Society, 1981. URL: https://doi.org/10.1109/SFCS.1981.44.
  49. W. Yi. Real-time behaviour of asynchronous agents. In International Conference on Concurrency Theory (CONCUR), 1990. URL: https://doi.org/10.1007/BFb0039080.
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