Document Open Access Logo

On the Expressive Equivalence of TPTL in the Pointwise and Continuous Semantics

Authors Raveendra Holla, Nabarun Deka, Deepak D'Souza

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2021.45.pdf
  • Filesize: 0.7 MB
  • 21 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Real-Time Logics
  • First-Order Logics

Metrics

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

Abstract

We consider a first-order logic with linear constraints interpreted in a pointwise and continuous manner over timed words. We show that the two interpretations of this logic coincide in terms of expressiveness, via an effective transformation of sentences from one logic to the other. As a consequence it follows that the pointwise and continuous semantics of the logic TPTL with the since operator also coincide. Along the way we exhibit a useful normal form for sentences in these logics.

Cite As Get BibTex

Raveendra Holla, Nabarun Deka, and Deepak D'Souza. On the Expressive Equivalence of TPTL in the Pointwise and Continuous Semantics. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 45:1-45:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.FSTTCS.2021.45

Author Details

Raveendra Holla
  • Citrix Systems India Pvt. Ltd., Bangalore, India
Nabarun Deka
  • Indian Institute of Science Bangalore, India
Deepak D'Souza
  • Indian Institute of Science Bangalore, India

References

  1. Rajeev Alur, Tomas Feder, and Thomas A. Henzinger. The benefits of relaxing punctuality. In 10th ACM Symposium on Principles of Distributed Computing, pages 139-152, 1991. Google Scholar
  2. Rajeev Alur and Thomas A. Henzinger. A Really Temporal Logic. In IEEE Symposium on Foundations of Computer Science, pages 164-169, 1989. Google Scholar
  3. Rajeev Alur and Thomas A. Henzinger. A Really Temporal Logic. J. ACM, 41(1):181-204, 1994. URL: https://doi.org/10.1145/174644.174651.
  4. Patricia Bouyer, Fabrice Chevalier, and Nicolas Markey. On the expressiveness of TPTL and MTL. In Foundations of Software Technology and Theoretical Computer Science, 2005. Google Scholar
  5. Patricia Bouyer, Fabrice Chevalier, and Nicolas Markey. On the expressiveness of TPTL and MTL. Inf. Comput., 208(2):97-116, 2010. URL: https://doi.org/10.1016/j.ic.2009.10.004.
  6. Deepak D'Souza, Raveendra Holla, and Raj Mohan M. Equivalence of the pointwise and continuous semantics of first order logic with linear constraints, 2010. URL: https://www.csa.iisc.ac.in/~deepakd/papers/tptl.pdf.
  7. Deepak D'Souza and Pavithra Prabhakar. On the expressiveness of MTL in the pointwise and continuous semantics. In Formal Methods Letters, Software Tools for Technology Transfer, Vol. 9, No. 1, pages 1-4. Springer, 2007. Google Scholar
  8. Dov Gabbay, Amir Pnueli, Saharon Shelah, and Jonathan Stavi. On the temporal analysis of fairness. In 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 163-173, 1980. Google Scholar
  9. Hsi-Ming Ho, Joël Ouaknine, and James Worrell. On the Expressiveness and Monitoring of Metric Temporal Logic. Log. Methods Comput. Sci., 15(2), 2019. URL: https://doi.org/10.23638/LMCS-15(2:13)2019.
  10. Ron Koymans. Specifying Real-Time Properties with Metric Temporal Logic. In Real Time Systems, pages 2(4):255-299, 1990. Google Scholar
  11. Joël Ouaknine, Alexander Rabinovich, and James Worrell. Time-Bounded Verification. In Mario Bravetti and Gianluigi Zavattaro, editors, 20th International Conference on Concurreny Theory, volume 5710 of Lecture Notes in Computer Science, pages 496-510. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04081-8_33.
  12. Joël Ouaknine and James Worrell. On the Decidability of Metric Temporal Logic. In 20th Annual IEEE Symposium on Logic in Computer Science, pages 188-197, 2005. Google Scholar
  13. Pavithra Prabhakar and Deepak D'Souza. On the expressiveness of MTL with past operators. In 4th Intl. Conference on Formal Modelling and Analysis of Timed Systems, pages 322-336, 2006. URL: https://doi.org/10.1007/11867340_23.
  14. Alexander Schrijver. Theory of Linear and Integer Programming, pages 155-157. John Wiley & Sons, 2000. 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