Document Open Access Logo

Revisiting the Expressiveness of Metric Temporal Logic

Author Mohammed Aristide Foughali

PDF

File

Thumbnail PDF
PDF
OASIcs.TIME.2026.1.pdf
  • Filesize: 0.74 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Timed logics
  • Metric temporal logic

Metrics

Abstract

The expressiveness of Metric Temporal Logic (MTL) has been extensively studied throughout the last two decades. In particular, it has been shown that the interval-based semantics of MTL is strictly more expressive than the pointwise one. These results may suggest that enabling the evaluation of formulae at arbitrary time points instead of positions of timed events increases the expressive power of MTL. In this paper, we formally argue otherwise. We demonstrate that under standard models of finite or non-Zeno infinite (action-based) timed executions, the interval-based and the pointwise semantics are incomparable. We then propose a new mixed semantics that embeds both the pointwise and the interval-based ones.

Cite As Get BibTex

Mohammed Aristide Foughali. Revisiting the Expressiveness of Metric Temporal Logic. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 1:1-1:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/OASIcs.TIME.2026.1

Author Details

Mohammed Aristide Foughali
  • Université Paris Cité, CNRS, IRIF, F-75013, Paris, France

Funding

This work received partial support from the ANR project ERVoRS (ANR-25-CE48-6220).

References

  1. 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.
  2. Rajeev Alur, Limor Fix, and Thomas A Henzinger. A determinizable class of timed automata. In International conference on computer aided verification (CAV), pages 1-13. Springer, 1994. URL: https://doi.org/10.1007/3-540-58179-0_39.
  3. Rajeev Alur and Thomas A Henzinger. Logics and models of real time: A survey. In Workshop/School/Symposium of the REX Project (Research and Education in Concurrent Systems), pages 74-106. Springer, 1991. URL: https://doi.org/10.1007/BFB0031988.
  4. 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.
  5. 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.
  6. Mouloud Amara, Giovanni Bernardi, Mohammed Aristide Foughali, and Adrian Francalanza. A theory of (linear-time) timed monitors. In European Conference on Object-Oriented Programming (ECOOP), volume 333, pages 1:1-1:30, 2025. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2025.1.
  7. Eugene Asarin, Paul Caspi, and Oded Maler. Timed regular expressions. Journal of the ACM, 49(2):172-206, 2002. URL: https://doi.org/10.1145/506147.506151.
  8. Béatrice Bérard, Paul Gastin, and Antoine Petit. Refinements and abstractions of signal-event (timed) languages. In International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), pages 67-81. Springer, 2006. URL: https://doi.org/10.1007/11867340_6.
  9. Patricia Bouyer, Fabrice Chevalier, and Nicolas Markey. On the expressiveness of TPTL and MTL. In International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pages 432-443. Springer, 2005. URL: https://doi.org/10.1007/11590156_35.
  10. Patricia Bouyer, Fabrice Chevalier, and Nicolas Markey. On the expressiveness of TPTL and MTL. Information and Computation, 208(2):97-116, 2010. URL: https://doi.org/10.1016/J.IC.2009.10.004.
  11. Bjorn B Brandenburg. Scheduling and locking in multiprocessor real-time operating systems. PhD thesis, The University of North Carolina at Chapel Hill, 2011. Google Scholar
  12. Rocco De Nicola and Frits Vaandrager. Action versus state based logics for transition systems. In LITP Spring School on Theoretical Computer Science, pages 407-419. Springer, 1990. URL: https://doi.org/10.1007/3-540-53479-2_17.
  13. David L Dill. Timing assumptions and verification of finite-state concurrent systems. In International Conference on Computer Aided Verification (CAV), pages 197-212. Springer, 1989. URL: https://doi.org/10.1007/3-540-52148-8_17.
  14. Deepak D’Souza and Pavithra Prabhakar. On the expressiveness of MTL in the pointwise and continuous semantics. International Journal on Software Tools for Technology Transfer, 9(1):1-4, 2007. URL: https://doi.org/10.1007/S10009-005-0214-9.
  15. Colin Fidge. Logical time in distributed computing systems. Computer, 24(8):28-33, 2002. Google Scholar
  16. 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.
  17. Mohammed Aristide Foughali. Revisiting the expressiveness of metric temporal logic: A tale of "je t'aime, moi non plus.". arXiv preprint arXiv:2603.15379, 2026. URL: https://doi.org/10.48550/arXiv.2603.15379.
  18. Mohammed Aristide Foughali, Marius Mikucionis, and Maryline Zhang. Scalable computation of inter-core bounds through exact abstractions. In Annual Computers, Software, and Applications Conference (COMPSAC), pages 61-70, 2024. URL: https://doi.org/10.1109/COMPSAC61105.2024.00019.
  19. Carlo Alberto Furia and Matteo Rossi. On the expressiveness of MTL variants over dense time. In International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), pages 163-178. Springer, 2007. Google Scholar
  20. Christoph Haase, Joël Ouaknine, and James Worrell. On process-algebraic extensions of metric temporal logic. Reflections on the Work of CAR Hoare, pages 283-300, 2010. URL: https://doi.org/10.1007/978-1-84882-912-1_13.
  21. 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.
  22. 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.
  23. Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. In Concurrency: the Works of Leslie Lamport, pages 179-196. Association for Computing Machinery, 2019. URL: https://doi.org/10.1145/3335772.3335934.
  24. Christoph Liebig, Mariano Cilia, and Alejandro Buchmann. Event composition in time-dependent distributed systems. In International Conference on Cooperative Information Systems (COOPIS), pages 70-78. IEEE, 1999. URL: https://doi.org/10.1109/COOPIS.1999.792159.
  25. Joël Ouaknine and James Worrell. On the decidability of metric temporal logic. In Symposium on Logic in Computer Science (LICS), pages 188-197. IEEE, 2005. URL: https://doi.org/10.1109/LICS.2005.33.
  26. Joël Ouaknine and James Worrell. On the decidability and complexity of metric temporal logic over finite words. Logical Methods in Computer Science, 3, 2007. URL: https://doi.org/10.2168/LMCS-3(1:8)2007.
  27. Joël Ouaknine and James Worrell. Some recent results in metric temporal logic. In International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), pages 1-13. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85778-5_1.
  28. 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.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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