Document Open Access Logo

Making Metric Temporal Logic Rational

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

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2017.77.pdf
  • Filesize: 0.67 MB
  • 14 pages

Document Identifiers

Author Details

Shankara Narayanan Krishna
Khushraj Madnani
Paritosh K. Pandya

Cite AsGet BibTex

Shankara Narayanan Krishna, Khushraj Madnani, and Paritosh K. Pandya. Making Metric Temporal Logic Rational. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 77:1-77:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.MFCS.2017.77

Abstract

We study an extension of MTL in pointwise time with regular expression guarded modality Reg_I(re) where re is a rational expression over subformulae. We study the decidability and expressiveness of this extension (MTL+Ureg+Reg), called RegMTL, as well as its fragment SfrMTL where only star-free rational expressions are allowed. Using the technique of temporal projections, we show that RegMTL has decidable satisfiability by giving an equisatisfiable reduction to MTL. We also identify a subclass MITL+UReg of RegMTL for which our equisatisfiable reduction gives rise to formulae of MITL, yielding elementary decidability. As our second main result, we show a tight automaton-logic connection between SfrMTL and partially ordered (or very weak) 1-clock alternating timed automata.
Keywords
  • Metric Temporal Logic
  • Timed Automata
  • Regular Expression
  • Equisatisfiability
  • Expressiveness

Metrics

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

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 Thomas A. Henzinger. Real-time logics: Complexity and expressiveness. Inf. Comput., 104(1):35-77, 1993. URL: http://dx.doi.org/10.1006/inco.1993.1025.
  3. Eugene Asarin, Paul Caspi, and Oded Maler. Timed regular expressions. J. ACM, 49(2):172-206, 2002. URL: http://dx.doi.org/10.1145/506147.506151.
  4. Augustin Baziramwabo, Pierre McKenzie, and Denis Thérien. Modular temporal logic. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 344-351, 1999. URL: http://dx.doi.org/10.1109/LICS.1999.782629.
  5. 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.
  6. Cindy Eisner and Dana Fisman. A Practical Introduction to PSL. Springer, 2006. Google Scholar
  7. IEEE P1850-Standard for PSL-Property Specification Language, 2005. Google Scholar
  8. Jesper G. Henriksen and P. S. Thiagarajan. Dynamic linear time temporal logic. Ann. Pure Appl. Logic, 96(1-3):187-207, 1999. URL: http://dx.doi.org/10.1016/S0168-0072(98)00039-6.
  9. Philippe Herrmann. Renaming is necessary in timed regular expressions. In Foundations of Software Technology and Theoretical Computer Science, 19th Conference, Chennai, India, December 13-15, 1999, Proceedings, pages 47-59, 1999. URL: http://dx.doi.org/10.1007/3-540-46691-6_4.
  10. P. Hunter. When is metric temporal logic expressively complete? In CSL, pages 380-394, 2013. Google Scholar
  11. S. N. Krishna K. Madnani and P. K. Pandya. Partially punctual metric temporal logic is decidable. In TIME, pages 174-183, 2014. Google Scholar
  12. Shankara Narayanan Krishna, Khushraj Madnani, and Paritosh K. Pandya. Metric temporal logic with counting. In Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, pages 335-352, 2016. Google Scholar
  13. F. Laroussinie, A. Meyer, and E. Petonnet. Counting ltl. In TIME, pages 51-58, 2010. Google Scholar
  14. K. Lodaya and A. V. Sreejith. Ltl can be more succinct. In ATVA, pages 245-258, 2010. Google Scholar
  15. J. Ouaknine and J. Worrell. On the decidability of metric temporal logic. In LICS, pages 188-197, 2005. Google Scholar
  16. A. Rabinovich. Complexity of metric temporal logic with counting and pnueli modalities. In FORMATS, pages 93-108, 2008. 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