Skip to main content
SpringerLink
Log in

An Expressive Temporal Logic for Real Time

  • Conference paper
Mathematical Foundations of Computer Science 2006 (MFCS 2006)

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

Abstract

We add to the standard temporal logic with the modalities ”Until” and ”Since”, a sequence of “counting modalities”: For each n the modality C n (X), which says that X will be true at least at n points in the next unit of time, and its past counterpart \({\overleftarrow{C}_n}\), which says that X has happened at least n times in the last unit of time. We prove that this temporal logic is as expressive as can be hoped for; all the modalities that can be expressed in a strong natural decidable predicate logic framework, are expressible in this temporal logic.

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., Feder, T., Henzinger, T.A.: The Benefits of Relaxing Punctuality. Journal of the ACM 43, 116–146 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  2. Alur, R., Henzinger, T.A.: Logics and Models of Real Time: a survey. 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 

  3. Brzozowski, J.A., Knast, R.: The dot depth hierarchy of star free languages is infinite. J. of Computing Systems Science 16, 37–55 (1978)

    Article  MATH  MathSciNet  Google Scholar 

  4. Barringer, B.H., Kuiper, R., Pnueli, A.: A really abstract concurrent model and its temporal logic. In: Proceedings of the 13th annual symposium on principles of programing languages, pp. 173–183 (1986)

    Google Scholar 

  5. Ebbinghaus, H.D., Flum, J.: Finite Model Theory. Perspectives in mathematical logic. Springer, Heidelberg (1991)

    Google Scholar 

  6. Ehrenfeucht, A.: An application of games to the completeness problem for formalized theories. Fundamenta Mathematicae 49, 129–141 (1961)

    MATH  MathSciNet  Google Scholar 

  7. Feferman, S., Vaught, R.L.: The first-order properties of products of algebraic systems. Fundamenta Mathematicae 47, 57–103 (1959)

    MATH  MathSciNet  Google Scholar 

  8. Gabbay, D.M., Hodkinson, I., Reynolds, M.: Temporal Logics, vol. 1. Clarendon Press, Oxford (1994)

    Book  Google Scholar 

  9. Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the Temporal Analysis of Fairness. In: 7th ACM Symposium on Principles of Programming Languages, Las Vegas, pp. 163–173 (1980)

    Google Scholar 

  10. 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 

  11. Gurevich, Y.: Monadic second-order theories. In: Barwise, J., Feferman, S. (eds.) Model-Theoretic Logics, pp. 479–506. Springer, Heidelberg (1985)

    Google Scholar 

  12. Hirshfeld, Y., Rabinovich, A.: A Framework for Decidable Metrical Logics. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 422–432. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  13. Hirshfeld, Y., Rabinovich, A.: Quantitative Temporal Logic. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 172–187. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  14. Hirshfeld, Y., Rabinovich, A.: Logics for Real Time: Decidability and Complexity. Fundam. Inform. 62(1), 1–28 (2004)

    MATH  MathSciNet  Google Scholar 

  15. Hirshfeld, Y., Rabinovich, A.: Timer formulas and decidable metric temporal logic. Information and Computation 198(2), 148–178 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  16. Hirshfeld, Y., Rabinovich, A.: Expressiveness of Metric Modalities for Continuous Time. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 211–220. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  17. Hirshfeld, Y., Rabinovich, A.: On The complexity of the temporal logic with counting modalities. Manuscript (2006)

    Google Scholar 

  18. Kamp, H.: Tense Logic and the Theory of Linear Order. Ph.D. thesis, University of California L.A. (1968)

    Google Scholar 

  19. Manna, Z., Pnueli, A.: Models for reactivity. Acta informatica 30, 609–678 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  20. Makowsky, J.A.: Algorithmic aspects of the Feferman-Vaught theorem. Annals of Pure and Applied Logic 126(1-3), 159–213 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  21. Rabinovich, A.: Expressive Power of Temporal Logics. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 57–75. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  22. Shelah, S.: The monadic theory of order. Ann. of Math. 102, 349–419 (1975)

    Article  Google Scholar 

  23. Thomas, W.: Ehrenfeucht games, the composition method, and the monadic theory of ordinal words. In: Mycielski, J., Rozenberg, G., Salomaa, A. (eds.) Structures in Logic and Computer Science. LNCS, vol. 1261, pp. 118–143. Springer, Heidelberg (1997)

    Google Scholar 

  24. Wilke, T.: Specifying Time State Sequences in Powerful Decidable Logics and Time Automata. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 694–715. Springer, Heidelberg (1994)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, Sackler Faculty of Exact Sciences, Tel Aviv University, Tel Aviv, 69978, Israel

    Yoram Hirshfeld & Alexander Rabinovich

Authors
  1. Yoram Hirshfeld
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexander Rabinovich
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Comenius University, Mlynská dolina, 84248, Bratislava, Slovakia

    Rastislav Královič

  2. Institute of Informatics, University of Warsaw, Poland

    Paweł Urzyczyn

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hirshfeld, Y., Rabinovich, A. (2006). An Expressive Temporal Logic for Real Time. In: Královič, R., Urzyczyn, P. (eds) Mathematical Foundations of Computer Science 2006. MFCS 2006. Lecture Notes in Computer Science, vol 4162. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11821069_43

Download citation

  • DOI: https://doi.org/10.1007/11821069_43

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-37791-7

  • Online ISBN: 978-3-540-37793-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation