Document Open Access Logo

Logics Meet 1-Clock Alternating Timed Automata

Authors Shankara Narayanan Krishna, Khushraj Madnani, Paritosh K. Pandya

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2018.39.pdf
  • Filesize: 0.75 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Metric Temporal Logic
  • Alternating Timed Automata
  • MSO
  • Regular Expressions
  • Expressive Completeness

Metrics

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

Abstract

This paper investigates a decidable and highly expressive real time logic QkMSO which is obtained by extending MSO[<] with guarded quantification using block of less than k metric quantifiers. The resulting logic is shown to be expressively equivalent to 1-clock ATA where loops are without clock resets, as well as, RatMTL, a powerful extension of MTL[U_I] with regular expressions. We also establish 4-variable property for QkMSO and characterize the expressive power of its 2-variable fragment. Thus, the paper presents progress towards expressively complete logics for 1-clock ATA.

Cite As Get BibTex

Shankara Narayanan Krishna, Khushraj Madnani, and Paritosh K. Pandya. Logics Meet 1-Clock Alternating Timed Automata. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 39:1-39:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CONCUR.2018.39

Author Details

Shankara Narayanan Krishna
  • Department of Computer Science & Engineering IIT Bombay, India
Khushraj Madnani
  • Department of Computer Science & Engineering IIT Bombay, India
Paritosh K. Pandya
  • School of Technology and Computer Science, TIFR, India

References

  1. Rajeev Alur, Tomás Feder, and Thomas A. Henzinger. The benefits of relaxing punctuality. In Proceedings of the Tenth Annual ACM Symposium on Principles of Distributed Computing, Montreal, Quebec, Canada, August 19-21, 1991, pages 139-152, 1991. URL: http://dx.doi.org/10.1145/112600.112613.
  2. Rajeev Alur and Thomas A. Henzinger. Real-time logics: Complexity and expressiveness. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), Philadelphia, Pennsylvania, USA, June 4-7, 1990, pages 390-401, 1990. URL: http://dx.doi.org/10.1109/LICS.1990.113764.
  3. Patricia Bouyer, Fabrice Chevalier, and Nicolas Markey. On the expressiveness of TPTL and MTL. In FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference, Hyderabad, India, December 15-18, 2005, Proceedings, pages 432-443, 2005. URL: http://dx.doi.org/10.1007/11590156_35.
  4. J. Engelfriet and H. Hoogeboom. MSO definable string transductions and two-way finite-state transducers. ACM Trans. Comput. Log., 2(2):216-254, 2001. Google Scholar
  5. C. Haase, J. Ouaknine, and J. Worrell. On process-algebraic extensions of metric temporal logic. In Reflections on the Work of C. A. R. Hoare., pages 283-300. 2010. Google Scholar
  6. Thomas A. Henzinger, Jean-François Raskin, and Pierre-Yves Schobbens. The regular real-time languages. In Automata, Languages and Programming, 25th International Colloquium, ICALP'98, Aalborg, Denmark, July 13-17, 1998, Proceedings, pages 580-591, 1998. URL: http://dx.doi.org/10.1007/BFb0055086.
  7. Y. Hirshfeld and A. Rabinovich. An expressive temporal logic for real time. In MFCS, pages 492-504, 2006. Google Scholar
  8. P. Hunter. When is metric temporal logic expressively complete? In CSL, pages 380-394, 2013. Google Scholar
  9. P. Hunter, J. Ouaknine, and J. Worrell. Expressive completeness for metric temporal logic. In LICS, pages 349-357, 2013. Google Scholar
  10. Neil Immerman and Dexter Kozen. Definability with bounded number of bound variables. Inf. Comput., 83(2):121-139, 1989. URL: http://dx.doi.org/10.1016/0890-5401(89)90055-2.
  11. J.R.Büchi. On a decision method in restricted second-order arithmetic. In Proceedings of the 1960 Congress on Logic, Methdology and Philosophy of Science, Stanford Univeristy Press, Stanford, 1962. Google Scholar
  12. S. N. Krishna K. Madnani and P. K. Pandya. Partially punctual metric temporal logic is decidable. In TIME, pages 174-183, 2014. Google Scholar
  13. Hans Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, Ucla, 1968. Google Scholar
  14. Ron Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255-299, 1990. URL: http://dx.doi.org/10.1007/BF01995674.
  15. Shankara Narayanan Krishna, Khushraj Madnani, and Paritosh K. Pandya. Büchi-kamp theorems for 1-clock ATA. CoRR, abs/1802.02514, 2018. URL: http://arxiv.org/abs/1802.02514.
  16. S. Lasota and I. Walukiewicz. Alternating timed automata. ACM Trans. Comput. Log., 9(2):10:1-10:27, 2008. URL: http://dx.doi.org/10.1145/1342991.1342994.
  17. J. Ouaknine and J. Worrell. On the decidability of metric temporal logic. In LICS, pages 188-197, 2005. Google Scholar
  18. Paritosh K. Pandya and Simoni S. Shah. On expressive powers of timed logics: Comparing boundedness, non-punctuality, and deterministic freezing. In CONCUR 2011 - Concurrency Theory - 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings, pages 60-75, 2011. URL: http://dx.doi.org/10.1007/978-3-642-23217-6_5.
  19. Jean Francois Raskin. Logics, Automata and Classical Theories for Deciding Real Time. PhD thesis, Universite de Namur, 1999. Google Scholar
  20. S.Krishna, K. Madnani, and P. K. Pandya. Metric temporal logic with counting. In FoSSaCS, pages 335-352, 2016. Google Scholar
  21. P. K. Pandya S.Krishna, K. Madnani. Making metric temporal logic rational. In MFCS, 2017. Google Scholar
  22. T. Wilke. Specifying timed state sequences in powerful decidable logics and timed automata. In FTRTFT, pages 694-715, 1994. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact