Document Open Access Logo

Metric Linear-Time Temporal Logic with Strict First-Time Semantics

Authors Eric Alsmann , Martin Lange

PDF

File

Thumbnail PDF
PDF
LIPIcs.TIME.2025.3.pdf
  • Filesize: 0.73 MB
  • 14 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Automata over infinite objects
Keywords
  • linear-time temporal logic
  • metric temporal logic
  • computational complexity
  • Streett automata

Metrics

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

Abstract

We introduce strict first-time semantics for the Until operator from linear-time temporal logic which makes assertions not just about some future moment but about the first time in the future that its argument should hold. We investigate Metric Linear-Time Temporal Logic under this interpretation in terms of expressive power, relative succinctness and computational complexity. While the expressiveness does not exceed that of pure LTL, there are properties definable in this logic which can only be expressed in LTL with exponentially larger formulas. Yet, we show that the complexity of the satisfiability problem remains PSPACE-complete which is in contrast to the EXPSPACE-completeness of Metric LTL. The motivation for this logic originates in a study of the expressive power of State Space Models, a recently proposed alternative to the popular transformer architectures in machine learning.

Cite As Get BibTex

Eric Alsmann and Martin Lange. Metric Linear-Time Temporal Logic with Strict First-Time Semantics. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 3:1-3:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.TIME.2025.3

Author Details

Eric Alsmann
  • Theoretical Computer Science / Formal Methods, University of Kassel, Germany
Martin Lange
  • Theoretical Computer Science / Formal Methods, University of Kassel, Germany

References

  1. R. Alur and T. Henzinger. Real-time logics: Complexity and expressiveness. Information and Computation, 104(1):35-77, 1993. URL: https://doi.org/10.1006/INCO.1993.1025.
  2. S. Arora and B. Barak. Computational Complexity: A Modern Approach. Cambridge Univ. Press, 2006. Google Scholar
  3. B. Banieqbal and H. Barringer. Temporal logic with fixed points. In Proc. Coll. on Temporal Logic in Specification, volume 398 of LNCS, pages 62-73. Springer, 1989. URL: https://doi.org/10.1007/3-540-51803-7_22.
  4. S. Demri, V. Goranko, and M. Lange. Temporal Logics in Computer Science. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. Google Scholar
  5. C. Eisner and D. Fisman. A Practical Introduction to PSL. Series on Integrated Circuits and Systems. Springer, 2006. URL: https://doi.org/10.1007/978-0-387-36123-9.
  6. D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In Proc. 7th Symp. on Principles of Programming Languages, POPL'80, pages 163-173. ACM, 1980. URL: https://doi.org/10.1145/567446.567462.
  7. G. De Giacomo and M. Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In Proc. 23rd Int. Joint Conf. on A.I., IJCAI'13, pages 854-860. IJCAI/AAAI, 2013. URL: http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6997.
  8. M. Rauch Henzinger and J. A. Telle. Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning. In Proc. 5th Scand. Workshop on Algorithm Theory, SWAT'96, volume 1097 of LNCS, pages 16-27. Springer, 1996. URL: https://doi.org/10.1007/3-540-61422-2_117.
  9. 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.
  10. F. Laroussinie, N. Markey, and Ph. Schnoebelen. Efficient timed model checking for discrete-time systems. Theoretical Computer Science, 353(1):249-271, 2006. URL: https://doi.org/10.1016/j.tcs.2005.11.020.
  11. F. Laroussinie, A. Meyer, and E. Petonnet. Counting LTL. In Proc. 17th Int. Symp. on Temporal Representation and Reasoning, TIME'10, pages 51-58. IEEE, 2010. URL: https://doi.org/10.1109/TIME.2010.20.
  12. T. Latvala and K. Heljanko. Coping with strong fairness. Fundam. Informaticae, 43(1-4):175-193, 2000. URL: https://doi.org/10.3233/FI-2000-43123409.
  13. W. Merrill, J. Petty, and A. Sabharwal. The illusion of state in state-space models. In Proc. 41st Int. Conf. on Machine Learning, ICML'24, volume 235, pages 35492-35506. JMLR.org, 2024. Google Scholar
  14. A. Pnueli. The temporal logic of programs. In Proc. 18th Symp. on Foundations of Computer Science, FOCS'77, pages 46-57. IEEE, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  15. W. J. Savitch. Relationships between nondeterministic and deterministic tape complexities. Journal of Computer and System Sciences, 4:177-192, 1970. URL: https://doi.org/10.1016/S0022-0000(70)80006-X.
  16. A. P. Sistla. Theoretical Issues in the Design of Distributed and Concurrent Systems. PhD thesis, Harvard Univ., Cambridge, MA, 1983. Google Scholar
  17. A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32(3):733-749, 1985. URL: https://doi.org/10.1145/3828.3837.
  18. R. S. Streett. Propositional dynamic logic of looping and converse is elementarily decidable. Information and Control, 54(1/2):121-141, 1982. URL: https://doi.org/10.1016/S0019-9958(82)91258-X.
  19. M. Y. Vardi. A temporal fixpoint calculus. In Proc. Conf. on Principles of Programming Languages, POPL'88, pages 250-259. ACM, 1988. URL: https://doi.org/10.1145/73560.73582.
  20. M. Y. Vardi. An Automata-Theoretic Approach to Linear Temporal Logic, volume 1043 of LNCS, pages 238-266. Springer, New York, NY, USA, 1996. URL: https://doi.org/10.1007/3-540-60915-6_6.
  21. M. Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1-37, 1994. URL: https://doi.org/10.1006/INCO.1994.1092.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact