Document Open Access Logo

Expressive Equivalence Between Decidable Freeze and Metric Timed Temporal Logics.

Authors Hsi-Ming Ho , Shankara Narayanan Krishna , Khushraj Madnani , Rupak Majumdar , Paritosh Pandya

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.24.pdf
  • Filesize: 1.07 MB
  • 24 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • Timed Propositional Temporal Logic
  • Expressiveness
  • Metric Interval Temporal Logic
  • Satisfiability
  • Decidability

Metrics

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

Abstract

We demonstrate a surprising and first-of-its-kind expressive equivalence between decidable metric and freeze logics over timed words in pointwise semantics. Our main result states that Metric Interval Temporal Logic with future, past and Pnueli modalities, MITPPL, and full unilateral timed propositional temporal logic with both future and past temporal modalities, UPTL, have identical expressiveness. One of the highlights of this paper, which allows for this equivalence, is to prove that UPTL formulas admit monadic decomposition. Our result also implies that several decidable logics for real-time specifications, such as one-variable UPTL, unilateral MITPPL, and Q2MLO, are all expressively equivalent, and the reductions between them are effective. Hence, our result unifies the fragmented expressiveness boundary of timed temporal logics. As corollaries, we resolve the open question of the decidability for full UPTL, and the variable or clock hierarchy problem for the future fragment of UPTL.

Cite As Get BibTex

Hsi-Ming Ho, Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, and Paritosh Pandya. Expressive Equivalence Between Decidable Freeze and Metric Timed Temporal Logics.. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 24:1-24:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.24

Author Details

Hsi-Ming Ho
  • University of Sussex, UK
Shankara Narayanan Krishna
  • Indian Institute of Technology Bombay, Mumbai, India
Khushraj Madnani
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
  • Indian Institute of Technology Guwahati, India
Rupak Majumdar
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Paritosh Pandya
  • Indian Institute of Technology Bombay, Mumbai, India

Funding

This research was funded in part by the Deutsche Forschungsgemeinschaft (DFG) project 389792660 TRR 248-CPEC.

References

  1. Rajeev Alur, Tomás Feder, and Thomas A. Henzinger. The benefits of relaxing punctuality. In Luigi Logrippo, editor, Proceedings of the Tenth Annual ACM Symposium on Principles of Distributed Computing, Montreal, Quebec, Canada, August 19-21, 1991, pages 139-152. ACM, 1991. URL: https://doi.org/10.1145/112600.112613.
  2. 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.
  3. Rajeev Alur and Thomas A. Henzinger. A really temporal logic. In 30th Annual Symposium on Foundations of Computer Science, pages 164-169, 1989. URL: https://doi.org/10.1109/SFCS.1989.63473.
  4. Rajeev Alur and Thomas A. Henzinger. Real-time logics: Complexity and expressiveness. Inf. Comput., 104(1):35-77, 1993. URL: https://doi.org/10.1006/inco.1993.1025.
  5. Patricia Bouyer, Fabrice Chevalier, and Nicolas Markey. On the expressiveness of TPTL and MTL. In Sundar Sarukkai and Sandeep Sen, editors, FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, pages 432-443, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11590156_35.
  6. Thomas Brihaye, Morgane Estiévenart, and Gilles Geeraerts. On mitl and alternating timed automata over infinite words. In Formal Modeling and Analysis of Timed Systems: 12th International Conference, FORMATS 2014, Florence, Italy, September 8-10, 2014. Proceedings 12, pages 69-84. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-10512-3_6.
  7. 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, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, volume 10426 of Lecture Notes in Computer Science, pages 421-440. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63387-9_21.
  8. Thomas Ferrère. The compound interest in relaxing punctuality. In Klaus Havelund, Jan Peleska, Bill Roscoe, and Erik P. de Vink, editors, Formal Methods - 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 15-17, 2018, Proceedings, volume 10951 of Lecture Notes in Computer Science, pages 147-164. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-95582-7_9.
  9. Thomas A. Henzinger, Jean-François Raskin, and Pierre-Yves Schobbens. The regular real-time languages. In Kim Guldstrand Larsen, Sven Skyum, and Glynn Winskel, editors, Automata, Languages and Programming, 25th International Colloquium, ICALP'98, Aalborg, Denmark, July 13-17, 1998, Proceedings, volume 1443 of Lecture Notes in Computer Science, pages 580-591. Springer, 1998. URL: https://doi.org/10.1007/BFb0055086.
  10. Frédéric Herbreteau and Gérald Point. The tchecker tool and libraries. URL: https://github.com/ticktac-project/tchecker.
  11. Yoram Hirshfeld and Alexander Moshe Rabinovich. A framework for decidable metrical logics. In Jirí Wiedermann, Peter van Emde Boas, and Mogens Nielsen, editors, Automata, Languages and Programming, 26th International Colloquium, ICALP'99, Prague, Czech Republic, July 11-15, 1999, Proceedings, volume 1644 of Lecture Notes in Computer Science, pages 422-432. Springer, 1999. URL: https://doi.org/10.1007/3-540-48523-6_39.
  12. Yoram Hirshfeld and Alexander Moshe Rabinovich. Logics for real time: Decidability and complexity. Fundamenta Informaticae, 62(1):1-28, 2004. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi62-1-02.
  13. Yoram Hirshfeld and Alexander Moshe Rabinovich. An expressive temporal logic for real time. In MFCS, pages 492-504, 2006. URL: https://doi.org/10.1007/11821069_43.
  14. Yoram Hirshfeld and Alexander Moshe Rabinovich. Expressiveness of metric modalities for continuous time. In Dima Grigoriev, John Harrison, and Edward A. Hirsch, editors, Computer Science - Theory and Applications, pages 211-220, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11753728_23.
  15. Hsi-Ming Ho. Revisiting timed logics with automata modalities. In Necmiye Ozay and Pavithra Prabhakar, editors, Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, April 16-18, 2019, pages 67-76. ACM, 2019. URL: https://doi.org/10.1145/3302504.3311818.
  16. Hsi-Ming Ho and Khushraj Madnani. When do you start counting? revisiting counting and pnueli modalities in timed logics. In DCM. EPTCS, 2023. Google Scholar
  17. Hsi-Ming Ho and Khushraj Madnani. Metric quantifiers and counting in timed logics and automata. Information and Computation, 303:105268, 2025. URL: https://doi.org/10.1016/j.ic.2025.105268.
  18. Paul Hunter. When is metric temporal logic expressively complete? In 22nd EACSL Conference on Computer Science Logic, CSL, pages 380-394, 2013. URL: https://doi.org/10.4230/LIPICS.CSL.2013.380.
  19. Paul Hunter, Joël Ouaknine, and James Worrell. Expressive completeness for metric temporal logic. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 349-357. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.41.
  20. Ron Koymans. Specifying real-time properties with metric temporal logic. Real Time Syst., 2(4):255-299, 1990. URL: https://doi.org/10.1007/BF01995674.
  21. Shankara Narayanan Krishna, Khushraj Madnani, Manuel Mazo Jr., and Paritosh K. Pandya. Generalizing non-punctuality for timed temporal logic with freeze quantifiers. In Marieke Huisman, Corina S. Pasareanu, and Naijun Zhan, editors, Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings, volume 13047 of Lecture Notes in Computer Science, pages 182-199. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-90870-6_10.
  22. Shankara Narayanan Krishna, Khushraj Madnani, and Paritosh K. Pandya. Metric temporal logic with counting. In Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, pages 335-352, 2016. URL: https://doi.org/10.1007/978-3-662-49630-5_20.
  23. Shankara Narayanan Krishna, Khushraj Madnani, and Paritosh K. Pandya. Making metric temporal logic rational. In Kim G. Larsen, Hans L. Bodlaender, and Jean-François Raskin, editors, 42nd International Symposium on Mathematical Foundations of Computer Science, MFCS 2017, August 21-25, 2017 - Aalborg, Denmark, volume 83 of LIPIcs, pages 77:1-77:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.MFCS.2017.77.
  24. Shankara Narayanan Krishna, Khushraj Nanik Madnani, Rupak Majumdar, and Paritosh K. Pandya. Satisfiability checking of multi-variable TPTL with unilateral intervals is pspace-complete. In Guillermo A. Pérez and Jean-François Raskin, editors, 34th International Conference on Concurrency Theory, CONCUR 2023, September 18-23, 2023, Antwerp, Belgium, volume 279 of LIPIcs, pages 23:1-23:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.CONCUR.2023.23.
  25. Slawomir Lasota and Igor Walukiewicz. Alternating timed automata. ACM Trans. Comput. Log., 9(2):10:1-10:27, 2008. URL: https://doi.org/10.1145/1342991.1342994.
  26. Nicolas Markey. Temporal logic with past is exponentially more succinct. Bulletin-European Association for Theoretical Computer Science, 79:122-128, 2003. Google Scholar
  27. MightyPPL. URL: https://github.com/hsimho/MightyPPL.
  28. Joël Ouaknine and James Worrell. On the decidability of metric temporal logic. In LICS, pages 188-197, 2005. URL: https://doi.org/10.1109/LICS.2005.33.
  29. Paritosh K. Pandya and Simoni S. Shah. On expressive powers of timed logics: Comparing boundedness, non-punctuality, and deterministic freezing. In Joost-Pieter Katoen and Barbara König, editors, CONCUR 2011 - Concurrency Theory - 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings, volume 6901 of Lecture Notes in Computer Science, pages 60-75. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23217-6_5.
  30. Jean Francois Raskin. Logics, Automata and Classical Theories for Deciding Real Time. PhD thesis, Universite de Namur, 1999. Google Scholar
  31. Howard Straubing. Finite Automata, Formal Logic and Circuit Complexity. Birkhauser, 1994. Google Scholar
  32. Thomas Wilke. Specifying timed state sequences in powerful decidable logics and timed automata. In Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems - ProCoS, Lübeck, Germany, September 19-23, Proceedings, pages 694-715, 1994. URL: https://doi.org/10.1007/3-540-58468-4_191.
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