Skip to main content
SpringerLink
Log in

On the Expressiveness of TPTL and MTL

  • Conference paper
FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2005)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3821))

Abstract

TPTL and MTL are two classical timed extensions of LTL. In this paper, we positively answer a 15-year-old conjecture that TPTL is strictly more expressive than MTL. But we show that, surprisingly, the TPTL formula proposed in [4] for witnessing this conjecture can be expressed in MTL. More generally, we show that TPTL formulae using only the F modality can be translated into MTL.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R.: Techniques for Automatic Verification of Real-Time Systems. Ph.D thesis, Stanford Univ., Stanford, CA, USA (1991)

    Google Scholar 

  2. Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Information. and Computation 104(1), 2–34 (1993)

    MATH  MathSciNet  Google Scholar 

  3. Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. Journal of the ACM 43(1), 116–146 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  4. Alur, R., Henzinger, T.A.: Real-time logics: Complexity and expressiveness. In: Proc. 5th Ann. Symp. Logic in Computer Science (LICS 1990), pp. 390–401. IEEE Comp. Soc. Press, Los Alamitos (1990)

    Chapter  Google Scholar 

  5. Alur, R., Henzinger, T.A.: Back to the future: towards a theory of timed regular languages. In: Proc. 33rd Ann. Symp. Foundations of Computer Science (FOCS 1992), pp. 177–186. IEEE Comp. Soc. Press, Los Alamitos (1992)

    Chapter  Google Scholar 

  6. Alur, R., Henzinger, T.A.: Logics and models of real-time: A survey. In Real- Time: Theory in Practice. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 74–106. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  7. Alur, R., Henzinger, T.A.: Real-time logics: Complexity and expressiveness. Information and Computation 104(1), 35–77 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  8. Alur, R., Henzinger, T.A.: A really temporal logic. Journal of the ACM 41(1), 181–204 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  9. Bouyer, P., Chevalier, F., Markey, N.: About the expressiveness of TPTL and MTL. Research Report LSV-05-05, LSV, ENS Cachan, France (2005)

    Google Scholar 

  10. D’Souza, D., Prabhakar, P.: On the expressiveness of MTL in the pointwise and continuous semantics. Technical Report IISc-CSA-TR-2005-7, Indian Institute of Science, Bangalore, India (2005)

    Google Scholar 

  11. Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Conf. Record 7th ACM Symp. Principles of Programming Languages (POPL 1980), pp. 163–173. ACM Press, New York (1980)

    Chapter  Google Scholar 

  12. Henzinger, T.A.: It’s about time: Real-time logics reviewed. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 439–454. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  13. Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model-checking for real-time systems. Information and Computation 111(2), 193–244 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  14. Kamp, J.A.: Tense Logic and the Theory of Linear Order. Ph.D thesis, UCLA, Los Angeles, CA, USA (1968)

    Google Scholar 

  15. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems 2(4), 255–299 (1990)

    Article  Google Scholar 

  16. Lasota, S., Walukiewicz, I.: Alternating timed automata. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 250–265. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  17. Markey, N., Raskin, J.-F.: Model checking restricted sets of timed paths. Theoretical Computer Science (2005) (to appear)

    Google Scholar 

  18. Ouaknine, J., Worrell, J.B.: On the decidability of metric temporal logic. In: Proc. 19th Ann. Symp. Logic in Computer Science (LICS 2005), pp. 188–197. IEEE Comp. Soc. Press, Los Alamitos (2005)

    Chapter  Google Scholar 

  19. Pnueli, A.: The temporal logic of programs. In: Proc. 18th Ann. Symp. Foundations of Computer Science (FOCS 1977), pp. 46–57. IEEE Comp. Soc. Press, Los Alamitos (1977)

    Chapter  Google Scholar 

  20. Raskin, J.-F.: Logics, Automata and Classical Theories for Deciding Real-Time. Ph.D thesis, Univ. Namur, Namur, Belgium (1999)

    Google Scholar 

  21. Sistla, P., Clarke, E.M.: The complexity of propositional linear temporal logics. Journal of the ACM 32(3), 733–749 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  22. Thati, P., Rosu, G.: Monitoring algorithms for metric temporal logic specifications. In: Proc. 4th International Workshop on Runtime Verification (RV 2004). ENTCS, vol. 113, pp. 145–162. Elsevier, Amsterdam (2005)

    Google Scholar 

  23. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st Ann. Symp. Logic in Computer Science (LICS 1986), pp. 322–344. IEEE Comp. Soc. Press, Los Alamitos (1986)

    Google Scholar 

  24. Yovine, S.: Méthodes et outils pour la vérification symbolique de systèmes temporis és. Ph.D thesis, INPG, Grenoble, France (1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LSV CNRS & ENS de Cachan, France

    Patricia Bouyer, Fabrice Chevalier & Nicolas Markey

Authors
  1. Patricia Bouyer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fabrice Chevalier
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Nicolas Markey
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. National Institute of Advanced Studies, Indian Institute of Science Campus, 560012, Bangalore, India

    Sundar Sarukkai

  2. Department of Comp. Sc. & Engg., Indian Institute of Technology Delhi, 110016, New Delhi, India

    Sandeep Sen

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bouyer, P., Chevalier, F., Markey, N. (2005). On the Expressiveness of TPTL and MTL . In: Sarukkai, S., Sen, S. (eds) FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2005. Lecture Notes in Computer Science, vol 3821. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11590156_35

Download citation

  • DOI: https://doi.org/10.1007/11590156_35

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-30495-1

  • Online ISBN: 978-3-540-32419-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation