Document Open Access Logo

Timed-Automata-Based Verification of MITL over Signals

Authors Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, Benjamin Monmege

PDF
Thumbnail PDF

File

LIPIcs.TIME.2017.7.pdf
  • Filesize: 0.7 MB
  • 19 pages

Document Identifiers

Author Details

Thomas Brihaye
Gilles Geeraerts
Hsi-Ming Ho
Benjamin Monmege

Cite As Get BibTex

Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, and Benjamin Monmege. Timed-Automata-Based Verification of MITL over Signals. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.TIME.2017.7

Abstract

It has been argued that the most suitable semantic model for real-time formalisms is the non-negative real line (signals), i.e. the continuous semantics, which naturally captures the continuous evolution of system states. Existing tools like UPPAAL are, however, based on omega-sequences with timestamps (timed words), i.e. the pointwise semantics. Furthermore, the support for logic formalisms is very limited in these tools. In this article, we amend these issues by a compositional translation from Metric Temporal Interval Logic (MITL) to signal automata. Combined with an emptiness-preserving encoding of signal automata into timed automata, we obtain a practical automata-based approach to MITL model-checking over signals. We implement the translation in our tool MightyL and report on case studies using LTSmin as the back-end.

Subject Classification

Keywords
  • real-time temporal logic
  • timed automata
  • real-time systems

Metrics

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

References

  1. Rajeev Alur, Costas Courcoubetis, and David Dill. Model-checking in dense real-time. Information and Computation, 104(1):2-34, 1993. Google Scholar
  2. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. Google Scholar
  3. Rajeev Alur, Tomás Feder, and Thomas A. Henzinger. The benefits of relaxing punctuality. Journal of the ACM, 43(1):116-146, 1996. Google Scholar
  4. Rajeev Alur and Thomas A. Henzinger. Back to the future: Towards a theory of timed regular languages. In 33rd Annual Symposium on Foundations of Computer Science, pages 177-186. IEEE, 1992. Google Scholar
  5. Rajeev Alur and Thomas A. Henzinger. Real-time logics: Complexity and expressiveness. Information and Computation, 104(1):35-77, 1993. URL: http://dx.doi.org/10.1006/inco.1993.1025.
  6. Rajeev Alur and Thomas A. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181-203, January 1994. URL: http://dx.doi.org/10.1145/174644.174651.
  7. Eugene Asarin, Paul Caspi, and Oded Maler. A Kleene theorem for timed automata. In LICS'97, pages 160-171. IEEE Computer Society Press, 1997. Google Scholar
  8. Ezio Bartocci, Luca Bortolussi, and Laura Nenzi. A temporal logic approach to modular design of synthetic biological circuits. In CMSB'13, volume 8130 of LNCS, pages 164-177. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-40708-6.
  9. Marcello M. Bersani, Matteo Rossi, and Pierluigi San Pietro. A tool for deciding the satisfiability of continuous-time metric temporal logic. Acta Informatica, 53(2):171-206, 2016. URL: http://dx.doi.org/10.1007/s00236-015-0229-y.
  10. Patricia Bouyer, Maximilien Colange, and Nicolas Markey. Symbolic optimal reachability in weighted timed automata. In CAV'16, volume 9779 of LNCS, pages 513-530. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-41528-4.
  11. Marius Bozga, Conrado Daws, Oded Maler, Alfredo Olivero, Stavros Tripakis, and Sergio Yovine. KRONOS: A model-checking tool for real-time systems (tool-presentation). In FTRTFT'98, volume 1486 of LNCS, pages 298-302. Springer, 1998. URL: http://dx.doi.org/10.1007/BFb0055357.
  12. Thomas Brihaye, Morgane Estiévenart, and Gilles Geeraerts. On MITL and alternating timed automata. In FORMATS'13, volume 8053 of LNCS, pages 47-61. Springer, 2013. Google Scholar
  13. Thomas Brihaye, Morgane Estiévenart, and Gilles Geeraerts. On MITL and alternating timed automata of infinite words. In FORMATS'14, volume 8711 of LNCS. Springer, 2014. Google Scholar
  14. Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, and Benjamin Monmege. MightyL: A compositional translation from MITL to timed automata. In CAV'17, LNCS. Springer, 2017. URL: https://hal.archives-ouvertes.fr/hal-01525524.
  15. Peter E. Bulychev, Alexandre David, Kim G. Larsen, and Guangyuan Li. Efficient controller synthesis for a fragment of MTL_0,∞. Acta Informatica, 51(3-4):165-192, 2014. URL: http://dx.doi.org/10.1007/s00236-013-0189-z.
  16. Koen Claessen, Niklas Een, and Baruch Sterin. A circuit approach to LTL model checking. In FMCAD'13. IEEE, 2013. Google Scholar
  17. Julien Cristau. Automata and temporal logic over arbitrary linear time. In FSTTCS'09, volume 4 of LIPIcs, pages 133-144. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2009. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2009.2313.
  18. Leonardo De Moura and Nikolaj Bjørner. Satisfiability modulo theories: introduction and applications. Communications of the ACM, 54(9):69-77, September 2011. URL: http://dx.doi.org/10.1145/1995376.1995394.
  19. Adel Dokhanchi, Bardh Hoxha, and Georgios Fainekos. Formal requirement debugging for testing and verification of cyber-physical systems. Research Report 1607.02549, arXiv, 2016. Google Scholar
  20. Deepak D'Souza and RM Matteplackel. A clock-optimal hierarchical monitoring automaton construction for mitl. Research Report 2013-1, IIS, 2013. URL: http://www.csa.iisc.ernet.in/TR/2013/1/lics2013-tr.pdf.
  21. Deepak D'Souza, M Raj Mohan, and Pavithra Prabhakar. Eliminating past operators in metric temporal logic. Perspectives in Concurrency, pages 86-106, 2008. Google Scholar
  22. A. Pnueli E. Asarin, O. Maler and J. Sifakis. Controller synthesis for timed automata. In SSC'98, pages 469-474. Elsevier, 1998. Google Scholar
  23. Javier Esparza and Jan Kretínský. From LTL to deterministic automata: A safraless compositional approach. In CAV'14, volume 8559 of LNCS, pages 192-208. Springer, 2014. Google Scholar
  24. Paul Gastin and Denis Oddoux. Fast LTL to Büchi automata translation. In CAV'01, volume 2102 of LNCS, pages 53-65. Springer, 2001. Google Scholar
  25. Marc Geilen. An improved on-the-fly tableau construction for a real-time temporal logic. In CAV'03, volume 2725 of LNCS, pages 394-406. Springer, 2003. URL: http://dx.doi.org/10.1007/978-3-540-45069-6_37.
  26. Marc Geilen and Dennis Dams. An on-the-fly tableau construction for a real-time temporal logic. In FTRTFT, volume 1926 of LNCS, pages 276-290. Springer, 2000. URL: http://dx.doi.org/10.1007/3-540-45352-0_23.
  27. Rob Gerth, Doron Peled, Moshe Y. Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic. In PSTV'95, pages 3-18. Chapman &Hall, 1995. Google Scholar
  28. Thomas A. Henzinger, Jean-François Raskin, and Pierre-Yves Schobbens. The regular real-time languages. In ICALP'98, volume 1443 of LNCS, pages 580-591. Springer, 1998. URL: http://dx.doi.org/10.1007/BFb0055086.
  29. Yoram Hirshfeld and Alexander Moshe Rabinovich. Logics for real time: Decidability and complexity. Fundamenta Informaticae, 62(1):1-28, 2004. Google Scholar
  30. Gijs Kant, Alfons Laarman, Jeroen Meijer, Jaco van de Pol, Stefan Blom, and Tom van Dijk. LTSmin: High-performance language-independent model checking. In TACAS'15, volume 9035 of LNCS, pages 692-707. Springer, 2015. Google Scholar
  31. Roland Kindermann, Tommi A. Junttila, and Ilkka Niemelä. Bounded model checking of an MITL fragment for timed automata. In ACSD'13, pages 216-225. IEEE Computer Society, 2013. Google Scholar
  32. Dileep Raghunath Kini, Shankara Narayanan Krishna, and Paritosh K. Pandya. On construction of safety signal automata for MITL[𝒰, 𝒮] using temporal projections. In FORMATS, volume 6919 of LNCS, pages 225-239. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-24310-3_16.
  33. Ron Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255-299, 1990. Google Scholar
  34. Alfons Laarman, Mads Chr. Olesen, Andreas Engelbredt Dalsgaard, Kim Guldstrand Larsen, and Jaco van de Pol. Multi-core emptiness checking of timed Büchi automata using inclusion abstraction. In CAV'13, volume 8044 of LNCS, pages 968-983. Springer, 2013. Google Scholar
  35. Kim G. Larsen, Paul Pettersson, and Wang Yi. Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer, 1(1-2):134-152, 1997. Google Scholar
  36. Oded Maler, Dejan Nickovic, and Amir Pnueli. From MITL to timed automata. In FORMATS'06, volume 4202 of LNCS, pages 274-289. Springer, 2006. Google Scholar
  37. Dejan Nickovic. Checking Timed and Hybrid Properties: Theory and Applications. (Vérification de propriétés temporisées et hybrides: théorie et applications). PhD thesis, Joseph Fourier University, Grenoble, France, 2008. Google Scholar
  38. Joël Ouaknine and James Worrell. On the decidability of metric temporal logic. In LICS'05, pages 188-197. IEEE Computer Society Press, 2005. Google Scholar
  39. Joël Ouaknine and James Worrell. On the decidability and complexity of metric temporal logic over finite words. Logical Methods in Computer Science, 3(1), 2007. Google Scholar
  40. Amir Pnueli and Aleksandr Zaks. On the merits of temporal testers. In 25 Years of Model Checking, volume 5000 of LNCS, pages 172-195. Springer, 2008. URL: http://dx.doi.org/10.1007/978-3-540-69850-0_11.
  41. Vasumathi Raman, Alexandre Donzé, Dorsa Sadigh, Richard M. Murray, and Sanjit A. Seshia. Reactive synthesis from signal temporal logic specifications. In HSCC'15, pages 239-248. ACM, 2015. Google Scholar
  42. Mark Reynolds. The complexity of the temporal logic with "until" over general linear time. Journal of Computer and System Sciences, 66(2):393-426, 2003. Google Scholar
  43. Kristin Y. Rozier and Moshe Y. Vardi. A multi-encoding approach for LTL symbolic satisfiability checking. In FM'11, volume 6664 of LNCS, pages 417-431. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-21437-0.
  44. Thomas Wilke. Specifying timed state sequences in powerful decidable logics and timed automata. In FTRTFT'94, volume 863 of LNCS, 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