Document Open Access Logo

Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete

Authors Shankara Narayanan Krishna , Khushraj Nanik Madnani , Rupak Majumdar , Paritosh Pandya

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.23.pdf
  • Filesize: 1.16 MB
  • 18 pages

Document Identifiers

Author Details

Shankara Narayanan Krishna
  • IIT Bombay, Mumbai, India
Khushraj Nanik Madnani
  • MPI-SWS, Kaiserslautern, Germany
Rupak Majumdar
  • MPI-SWS, Kaiserslautern, Germany
Paritosh Pandya
  • IIT Bombay, Mumbai, India

Funding

This research was sponsored in part by the Deutsche Forschungsgemeinschaft project 389792660 TRR 248—CPEC.

Acknowledgements

We thank Tom Henzinger for encouraging us to explore non-punctual subclasses for multi-clock TPTL and ATA. We also thank Hsi-Ming Ho for an insightful discussion.

Cite As Get BibTex

Shankara Narayanan Krishna, Khushraj Nanik Madnani, Rupak Majumdar, and Paritosh Pandya. Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CONCUR.2023.23

Abstract

We investigate the decidability of the {0,∞} fragment of Timed Propositional Temporal Logic (TPTL). We show that the satisfiability checking of TPTL^{0,∞} is PSPACE-complete. Moreover, even its 1-variable fragment (1-TPTL^{0,∞}) is strictly more expressive than Metric Interval Temporal Logic (MITL) for which satisfiability checking is EXPSPACE complete. Hence, we have a strictly more expressive logic with computationally easier satisfiability checking. To the best of our knowledge, TPTL^{0,∞} is the first multi-variable fragment of TPTL for which satisfiability checking is decidable without imposing any bounds/restrictions on the timed words (e.g. bounded variability, bounded time, etc.). The membership in PSPACE is obtained by a reduction to the emptiness checking problem for a new "non-punctual’’ subclass of Alternating Timed Automata with multiple clocks called Unilateral Very Weak Alternating Timed Automata (VWATA^{0,∞}) which we prove to be in PSPACE. We show this by constructing a simulation equivalent non-deterministic timed automata whose number of clocks is polynomial in the size of the given VWATA^{0,∞}.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • TPTL
  • Satisfiability
  • Non-Punctuality
  • Decidability
  • Expressiveness
  • ATA

Metrics

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

Related Versions

References

  1. R. Alur, T. Feder, and T. Henzinger. The benefits of relaxing punctuality. J.ACM, 43(1):116-146, 1996. Google Scholar
  2. Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci., 126(2):183-235, 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  3. 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.
  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, Pittsburgh, Pennsylvania, USA, 24-27 October 1992, pages 177-186. IEEE Computer Society, 1992. URL: https://doi.org/10.1109/SFCS.1992.267774.
  5. 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.
  6. Rajeev Alur and Thomas A. Henzinger. A really temporal logic. J. ACM, 41(1):181-203, January 1994. URL: https://doi.org/10.1145/174644.174651.
  7. 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. Google Scholar
  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. Paul Gastin and Denis Oddoux. LTL with past and two-way very-weak alternating automata. In Branislav Rovan and Peter Vojtás, editors, Mathematical Foundations of Computer Science 2003, 28th International Symposium, MFCS 2003, Bratislava, Slovakia, August 25-29, 2003, Proceedings, volume 2747 of Lecture Notes in Computer Science, pages 439-448. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45138-9_38.
  10. Christoph Haase, Joël Ouaknine, and James Worrell. On process-algebraic extensions of metric temporal logic. In A. W. Roscoe, Clifford B. Jones, and Kenneth R. Wood, editors, Reflections on the Work of C. A. R. Hoare, pages 283-300. Springer, 2010. URL: https://doi.org/10.1007/978-1-84882-912-1_13.
  11. Moritz Hammer, Alexander Knapp, and Stephan Merz. Truly on-the-fly ltl model checking. In Nicolas Halbwachs and Lenore D. Zuck, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 191-205, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  12. Thomas A. Henzinger. It’s about time: Real-time logics reviewed. In Davide Sangiorgi and Robert de Simone, editors, CONCUR'98 Concurrency Theory, pages 439-454, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg. Google Scholar
  13. 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.
  14. Y. Hirshfeld and A. Rabinovich. An expressive temporal logic for real time. In MFCS, pages 492-504, 2006. Google Scholar
  15. Yoram Hirshfeld and Alexander 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. Google Scholar
  16. 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.
  17. James Jerson Ortiz, Axel Legay, and Pierre-Yves Schobbens. Memory event clocks. In Krishnendu Chatterjee and Thomas A. Henzinger, editors, Formal Modeling and Analysis of Timed Systems, pages 198-212, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  18. S. N. Krishna K. Madnani and P. K. Pandya. On unary fragments of mtl over timed words. In ICTAC, pages 333-350, 2014. Google Scholar
  19. 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.
  20. Shankara Narayanan Krishna, Khushraj Madnani, and Paritosh K. Pandya. Logics meet 1-clock alternating timed automata. In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs, pages 39:1-39:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.39.
  21. 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.
  22. Christof Loding and Wolfgang Thomas. Alternating automata and logics over infinite words. In Jan van Leeuwen, Osamu Watanabe, Masami Hagiya, Peter D. Mosses, and Takayasu Ito, editors, Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics, pages 521-535, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg. Google Scholar
  23. Khushraj Nanik Madnani. On Decidable Extensions of Metric Temporal Logic. PhD thesis, Indian Institute of Technology Bombay, Mumbai, India, 2019. Google Scholar
  24. J. Ouaknine and J. Worrell. On the decidability of metric temporal logic. In LICS, pages 188-197, 2005. Google Scholar
  25. J. Ouaknine and J. Worrell. Safety metric temporal logic is fully decidable. In TACAS, pages 411-425, 2006. Google Scholar
  26. 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.
  27. Paritosh K. Pandya and Simoni S. Shah. The unary fragments of metric interval temporal logic: Bounded versus lower bound constraints. In Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012. Proceedings, pages 77-91, 2012. Google Scholar
  28. Radek Pelánek and Jan Strejček. Deeper connections between ltl and alternating automata. In Jacques Farré, Igor Litovsky, and Sylvain Schmitz, editors, Implementation and Application of Automata, pages 238-249, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  29. A. Rabinovich. Complexity of metric temporal logic with counting and pnueli modalities. In FORMATS, pages 93-108, 2008. Google Scholar
  30. Alexander Rabinovich. Complexity of metric temporal logics with counting and the pnueli modalities. Theor. Comput. Sci., 411(22-24):2331-2342, 2010. URL: https://doi.org/10.1016/j.tcs.2010.03.017.
  31. Jean Francois Raskin. Logics, Automata and Classical Theories for Deciding Real Time. PhD thesis, Universite de Namur, 1999. Google Scholar
  32. Gareth Scott Rohde. Alternating Automata and the Temporal Logic of Ordinals. PhD thesis, University of Illinois at Urbana-Champaign, USA, 1997. AAI9812757. Google Scholar
  33. Heikki Tauriainen. Automata and linear temporal logic: Translations with transition-based acceptance. Doctoral thesis, Helsinki University of Technology, 2006. Google Scholar
  34. Moshe Y. Vardi. An automata-theoretic approach to linear temporal logic. In Faron Moller and Graham Birtwistle, editors, Logics for Concurrency: Structure versus Automata, pages 238-266, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-60915-6_6.
  35. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact