Document Open Access Logo

MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm

Authors S. Akshay , Paul Gastin , R. Govind , B. Srivathsan

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.5.pdf
  • Filesize: 1.13 MB
  • 19 pages

Document Identifiers

Author Details

S. Akshay
  • Department of CSE, Indian Institute of Technology Bombay, Mumbai, India
Paul Gastin
  • Université Paris-Saclay, ENS Paris-Saclay, CNRS, LMF, 91190, Gif-sur-Yvette, France
  • CNRS, ReLaX, IRL 2000, Siruseri, India
R. Govind
  • Uppsala University, Sweden
B. Srivathsan
  • Chennai Mathematical Institute, India
  • CNRS, ReLaX, IRL 2000, Siruseri, India

Cite As Get BibTex

S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan. MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CONCUR.2024.5

Abstract

The translation of Metric Interval Temporal Logic (MITL) to timed automata is a topic that has been extensively studied. A key challenge here is the conversion of future modalities into equivalent automata. Typical conversions equip the automata with a guess-and-check mechanism to ascertain the truth of future modalities. Guess-and-check can be naturally implemented via alternation. However, since timed automata tools do not handle alternation, existing methods perform an additional step of converting the alternating timed automata into timed automata. This "de-alternation" step proceeds by an intricate finite abstraction of the space of configurations of the alternating automaton. 
Recently, a model of generalized timed automata (GTA) has been proposed. The model comes with several powerful additional features, and yet, the best known zone-based reachability algorithms for timed automata have been extended to the GTA model, with the same complexity for all the zone operations. An attractive feature of GTAs is the presence of future clocks which act like timers that guess a time to an event and stay alive until a timeout. Future clocks seem to provide another natural way to implement the guess-and-check: start the future clock with a guessed time to an event and check its occurrence using a timeout. Indeed, using this feature, we provide a new concise translation from MITL to GTA. In particular, for the timed until modality, our translation offers an exponential improvement w.r.t. the state-of-the-art.
Thanks to this conversion, MITL model checking reduces to checking liveness for GTAs. However, no liveness algorithm is known for GTAs. Due to the presence of future clocks, there is no finite time-abstract bisimulation (region equivalence) for GTAs, whereas liveness algorithms for timed automata crucially rely on the presence of the finite region equivalence. As our second contribution, we provide a new zone-based algorithm for checking Büchi non-emptiness in GTAs, which circumvents this fundamental challenge.

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
  • Theory of computation → Quantitative automata
  • Theory of computation → Logic and verification
Keywords
  • MITL model checking
  • timed automata
  • zones
  • liveness

Metrics

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

Related Versions

References

  1. S. Akshay, Paul Gastin, R. Govind, Aniruddha R. Joshi, and B. Srivathsan. A unified model for real-time systems: Symbolic techniques and implementation. In CAV (1), volume 13964 of Lecture Notes in Computer Science, pages 266-288. Springer, 2023. Google Scholar
  2. S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan. MITL model checking via generalized timed automata and a new liveness algorithm, 2024. URL: https://arxiv.org/abs/2407.08452.
  3. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183-235, 1994. Google Scholar
  4. Rajeev Alur, Tomás Feder, and Thomas A. Henzinger. The benefits of relaxing punctuality. J. ACM, 43(1):116-146, 1996. Google Scholar
  5. Rajeev Alur, Limor Fix, and Thomas A. Henzinger. Event-clock automata: A determinizable class of timed automata. Theor. Comput. Sci., 211(1-2):253-273, 1999. Google Scholar
  6. Rajeev Alur and Thomas A. Henzinger. Real-time logics: Complexity and expressiveness. In LICS, pages 390-401. IEEE Computer Society, 1990. Google Scholar
  7. Gerd Behrmann, Patricia Bouyer, Kim G. Larsen, and Radek Pelánek. Lower and upper bounds in zone-based abstractions of timed automata. International Journal on Software Tools for Technology Transfer, 8(3):204-215, 2006. Google Scholar
  8. Laura Bozzelli, Angelo Montanari, and Adriano Peron. Complexity issues for timeline-based planning over dense time under future and minimal semantics. Theor. Comput. Sci., 901:87-113, 2022. Google Scholar
  9. Thomas Brihaye, Morgane Estiévenart, and Gilles Geeraerts. On MITL and alternating timed automata. In FORMATS, volume 8053 of Lecture Notes in Computer Science, pages 47-61. Springer, 2013. Google Scholar
  10. Thomas Brihaye, Morgane Estiévenart, and Gilles Geeraerts. On MITL and alternating timed automata over infinite words. In FORMATS, volume 8711 of Lecture Notes in Computer Science, pages 69-84. Springer, 2014. Google Scholar
  11. Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, and Benjamin Monmege. MightyL: A compositional translation from MITL to timed automata. In CAV (1), volume 10426 of Lecture Notes in Computer Science, pages 421-440. Springer, 2017. Google Scholar
  12. Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, and Marco Roveri. NUSMV: A new symbolic model verifier. In CAV, volume 1633 of Lecture Notes in Computer Science, pages 495-499. Springer, 1999. Google Scholar
  13. David L. Dill. Timing assumptions and verification of finite-state concurrent systems. In Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 197-212. Springer, 1989. Google Scholar
  14. Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. Spot 2.0 - A framework for LTL and ω-automata manipulation. In ATVA, volume 9938 of Lecture Notes in Computer Science, pages 122-129, 2016. Google Scholar
  15. Thomas Ferrère, Oded Maler, Dejan Nickovic, and Amir Pnueli. From real-time logic to timed automata. J. ACM, 66(3):19:1-19:31, 2019. Google Scholar
  16. Paul Gastin, Sayan Mukherjee, and B. Srivathsan. Reachability in timed automata with diagonal constraints. In CONCUR, volume 118 of LIPIcs, pages 28:1-28:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  17. Paul Gastin, Sayan Mukherjee, and B. Srivathsan. Fast algorithms for handling diagonal constraints in timed automata. In CAV (1), volume 11561 of Lecture Notes in Computer Science, pages 41-59. Springer, 2019. Google Scholar
  18. Paul Gastin and Denis Oddoux. Fast LTL to Büchi automata translation. In CAV, volume 2102 of Lecture Notes in Computer Science, pages 53-65. Springer, 2001. Google Scholar
  19. Gilles Geeraerts, Jean-François Raskin, and Nathalie Sznajder. On regions and zones for event-clock automata. Formal Methods Syst. Des., 45(3):330-380, 2014. Google Scholar
  20. Rob Gerth, Doron A. Peled, Moshe Y. Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic. In PSTV, volume 38 of IFIP Conference Proceedings, pages 3-18. Chapman & Hall, 1995. Google Scholar
  21. F. Herbreteau and G. Point. TChecker. https://github.com/fredher/tchecker, v0.2 - April 2019.
  22. Frédéric Herbreteau, B. Srivathsan, Thanh-Tung Tran, and Igor Walukiewicz. Why liveness for timed automata is hard, and what we can do about it. ACM Trans. Comput. Log., 21(3):17:1-17:28, 2020. URL: https://doi.org/10.1145/3372310.
  23. Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Better abstractions for timed automata. In LICS, pages 375-384. IEEE Computer Society, 2012. Google Scholar
  24. Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Efficient emptiness check for timed büchi automata. Formal Methods Syst. Des., 40(2):122-146, 2012. Google Scholar
  25. Gerard J. Holzmann. The model checker SPIN. IEEE Trans. Software Eng., 23(5):279-295, 1997. Google Scholar
  26. Henrik Ejersbo Jensen, Kim G. Larsen, and Arne Skou. Modelling and analysis of a collision avoidance protocol using SPIN and UPPAAL. In The Spin Verification System, volume 32 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 33-49. DIMACS/AMS, 1996. Google Scholar
  27. Leslie Lamport. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002. Google Scholar
  28. Guangyuan Li. Checking timed Büchi automata emptiness using LU-abstractions. In Joël Ouaknine and Frits W. Vaandrager, editors, Formal Modeling and Analysis of Timed Systems, 7th International Conference, FORMATS 2009, Budapest, Hungary, September 14-16, 2009. Proceedings, volume 5813 of Lecture Notes in Computer Science, pages 228-242. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04368-0_18.
  29. Oded Maler, Dejan Nickovic, and Amir Pnueli. From MITL to timed automata. In FORMATS, volume 4202 of Lecture Notes in Computer Science, pages 274-289. Springer, 2006. Google Scholar
  30. Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger. Strix: Explicit reactive synthesis strikes back! In CAV (1), volume 10981 of Lecture Notes in Computer Science, pages 578-586. Springer, 2018. Google Scholar
  31. Joël Ouaknine and James Worrell. On metric temporal logic and faulty turing machines. In FoSSaCS, volume 3921 of Lecture Notes in Computer Science, pages 217-230. Springer, 2006. Google Scholar
  32. Amir Pnueli. The temporal logic of programs. In FOCS, pages 46-57. IEEE Computer Society, 1977. Google Scholar
  33. Amir Pnueli. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. In Current Trends in Concurrency, volume 224 of Lecture Notes in Computer Science, pages 510-584. Springer, 1986. Google Scholar
  34. Amir Pnueli and Eyal Harel. Applications of temporal logic to the specification of real-time systems. In FTRTFT, volume 331 of Lecture Notes in Computer Science, pages 84-98. Springer, 1988. Google Scholar
  35. Stavros Tripakis, Sergio Yovine, and Ahmed Bouajjani. Checking timed Büchi automata emptiness efficiently. Formal Methods Syst. Des., 26(3):267-292, 2005. Google Scholar
  36. Moshe Y Vardi. An automata-theoretic approach to linear temporal logic. Lecture Notes in Computer Science, 1043:238-266, 1996. Google Scholar
  37. Thomas Wilke. Specifying timed state sequences in powerful decidable logics and timed automata. In FTRTFT, volume 863 of Lecture Notes in Computer Science, pages 694-715. Springer, 1994. Google Scholar
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact