Document Open Access Logo

More Than 0s and 1s: Metric Quantifiers and Counting over Timed Words

Authors Hsi-Ming Ho , Khushraj Madnani

PDF
Thumbnail PDF

File

LIPIcs.TIME.2023.7.pdf
  • Filesize: 0.85 MB
  • 15 pages

Document Identifiers

Author Details

Hsi-Ming Ho
  • Department of Informatics, University of Sussex, UK
Khushraj Madnani
  • Max Planck Institute for Software Systems, Kaiserslautern, Germany

Cite AsGet BibTex

Hsi-Ming Ho and Khushraj Madnani. More Than 0s and 1s: Metric Quantifiers and Counting over Timed Words. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.TIME.2023.7

Abstract

We study the expressiveness of the pointwise interpretations (i.e. over timed words) of some predicate and temporal logics with metric and counting features. We show that counting in the unit interval (0, 1) is strictly weaker than counting in (0, b) with arbitrary b ≥ 0; moreover, allowing the latter indeed leads to expressive completeness for the metric predicate logic Q2MLO, recovering the corresponding result for the continuous interpretations (i.e. over signals). Exploiting this connection, we show that in contrast to the continuous case, adding "punctual" predicates into Q2MLO is still insufficient for the full expressive power of the Monadic First-Order Logic of Order and Metric (FO[<,+1]). Finally, we propose a generalisation of the recently proposed Pnueli automata modalities and show that the resulting metric temporal logic is expressively complete for FO[<,+1].

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Temporal Logic
  • Expressiveness
  • Automata

Metrics

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

References

  1. 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
  2. Rajeev Alur and Thomas A. Henzinger. Back to the future: Towards a theory of timed regular languages. In FOCS, pages 177-186. IEEE Computer Society Press, 1992. Google Scholar
  3. Rajeev Alur and Thomas A. Henzinger. Real-time logics: Complexity and expressiveness. Information and Computation, 104(1):35-77, 1993. URL: https://doi.org/10.1006/inco.1993.1025.
  4. 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: https://doi.org/10.1007/s00236-015-0229-y.
  5. Patricia Bouyer, Fabrice Chevalier, and Nicolas Markey. On the expressiveness of TPTL and MTL. Information and Computation, 208(2):97-116, 2010. Google Scholar
  6. Patricia Bouyer, François Laroussinie, Nicolas Markey, Joël Ouaknine, and James Worrell. Timed temporal logics. In Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, volume 10460 of LNCS, pages 211-230. Springer, 2017. Google Scholar
  7. Deepak D'Souza and Pavithra Prabhakar. On the expressiveness of mtl in the pointwise and continuous semantics. International Journal on Software Tools for Technology, 9(1):1-4, 2007. Google Scholar
  8. Deepak D'Souza and Nicolas Tabareau. On timed automata with input-determined guards. In Yassine Lakhnech and Sergio Yovine, editors, FORMATS/FTRTFT, volume 3253 of LNCS, pages 68-83. Springer, 2004. Google Scholar
  9. Deepak D’Souza and Raveendra Holla. Equivalance of pointwise and continuous semantics of fo with linear constraints. In ICLA, pages 40-45, 2021. Google Scholar
  10. R Govind, Frédéric Herbreteau, and Igor Walukiewicz. Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods. In LICS, pages 1-14. ACM/IEEE, 2022. Google Scholar
  11. Frédéric Herbreteau, B Srivathsan, and Igor Walukiewicz. Checking timed büchi automata emptiness using the local-time semantics. In CONCUR, volume 243 of LIPIcs, pages 12:1-12:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  12. Yoram Hirshfeld and Alexander Rabinovich. A framework for decidable metrical logics. In ICALP, volume 1644 of LNCS, pages 422-432. Springer, 1999. Google Scholar
  13. Yoram Hirshfeld and Alexander Rabinovich. Expressiveness of metric modalities for continuous time. Logical Methods in Computer Science, 3(1):1-11, 2007. Google Scholar
  14. Yoram Hirshfeld and Alexander Rabinovich. Continuous time temporal logic with counting. Information and Computation, 214:1-9, 2012. Google Scholar
  15. Yoram Hirshfeld and Alexander Moshe Rabinovich. Logics for real time: Decidability and complexity. Fundamenta Informaticae, 62(1):1-28, 2004. Google Scholar
  16. Yoram Hirshfeld and Alexander Moshe Rabinovich. An expressive temporal logic for real time. In MFCS, volume 4162 of LNCS, pages 492-504. Springer, 2006. Google Scholar
  17. Hsi-Ming Ho. On the expressiveness of metric temporal logic over bounded timed words. In RP, volume 8762 of LNCS, pages 138-150. Springer, 2014. Google Scholar
  18. Hsi-Ming Ho. Revisiting timed logics with automata modalities. In HSCC, pages 67-76. ACM, 2019. Google Scholar
  19. Hsi-Ming Ho and Khushraj Madnani. When do you start counting? revisiting counting and pnueli modalities in timed logics. In DCM. EPTCS, 2023. To appear. Google Scholar
  20. Paul Hunter. When is metric temporal logic expressively complete? In CSL, volume 23 of LIPIcs, pages 380-394. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. Google Scholar
  21. Paul Hunter, Joël Ouaknine, and James Worrell. Expressive completeness for metric temporal logic. In LICS, pages 349-357. IEEE Computer Society Press, 2013. Google Scholar
  22. Ron Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255-299, 1990. Google Scholar
  23. Shankara Narayanan Krishna, Khushraj Madnani, Manuel Mazo Jr., and Paritosh Pandya. From non-punctuality to non-adjacency: A quest for decidability of timed temporal logics with quantifiers. Formal Aspects of Computing, 2022. Google Scholar
  24. Shankara Narayanan Krishna, Khushraj Madnani, and Paritosh K. Pandya. Metric temporal logic with counting. In FoSSaCS, volume 9634 of LNCS, pages 335-352. Springer, 2016. Google Scholar
  25. Shankara Narayanan Krishna, Khushraj Madnani, and Paritosh K. Pandya. Making metric temporal logic rational. In MFCS, volume 83 of LIPIcs, pages 77:1-77:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. Google Scholar
  26. Shankara Narayanan Krishna, Khushraj Madnani, and Paritosh K. Pandya. Logics meet 1-clock alternating timed automata. In CONCUR, volume 118 of LIPIcs, pages 39:1-39:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  27. 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
  28. Joël Ouaknine, Alexander Rabinovich, and James Worrell. Time-bounded verification. In CONCUR, volume 5710 of LNCS, pages 496-510. Springer, 2009. Google Scholar
  29. Joël Ouaknine and James Worrell. On metric temporal logic and faulty turing machines. In FoSSaCS, volume 3921 of LNCS, pages 217-230. Springer, 2006. Google Scholar
  30. Paritosh K. Pandya and Simoni S. Shah. On expressive powers of timed logics: Comparing boundedness, non-punctuality, and deterministic freezing. In CONCUR, volume 6901 of LNCS, pages 60-75. Springer, 2011. Google Scholar
  31. Amir Pnueli. The temporal logic of programs. In FOCS, pages 46-57. IEEE, 1977. Google Scholar
  32. Saharon Shelah. The monadic theory of order. The Annals of Mathematics, 102(3):379, November 1975. Google Scholar
  33. Thomas Wilke. Specifying timed state sequences in powerful decidable logics and timed automata. In FTRTFT, volume 863 of LNCS, pages 694-715. Springer, 1994. Google Scholar
  34. Pierre Wolper and Moshe Y. Vardi. Reasoning about infinite computations. Information and Computation, 115(1):1-37, 1994. Google Scholar
  35. Yuchen Zhou, Dipankar Maity, and John S. Baras. Timed automata approach for motion planning using metric interval temporal logic. In ECC, pages 690-695. IEEE, 2016. 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 Imprint Privacy Contact