Skip to main content
SpringerLink
Log in

Nesting Until and Since in Linear Temporal Logic

  • Conference paper
  • First Online:
STACS 2002 (STACS 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2285))

Included in the following conference series:

Abstract

We provide an effective characterization of the “until-since hierarchy” of linear temporal logic, that is, we show how to compute for a given temporal property the minimal nesting depth in “until” and “since” required to express it. This settles the most prominent classi- fication problem for linear temporal logic. Our characterization of the individual levels of the “until-since hierarchy” is algebraic: for each n, we present a decidable class of finite semigroups and show that a temporal property is expressible with nesting depth at most n if and only if the syntactic semigroup of the formal language associated with the property belongs to the class provided. The core of our algebraic characterization is a new description of substitution in linear temporal logic in terms of block products of finite semigroups.

Supported by FCAR, NSERC and Alexander von Humboldt Foundation

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. Jorge Almeida. Finite Semigroups and Universal Algebra, volume 3 of Series in Algebra. World Scientific, Singapore, 1995.

    Google Scholar 

  2. Jorge Almeida. A syntactical proof of locality of DA. Internat. J. Algebra and Comput., 6(2):165–177, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  3. Joëlle Cohen-Chesnot. Etude algébrique de la logique temporelle. Doctoral thesis, Université Paris 6, Paris, France, April 1989.

    Google Scholar 

  4. Joëlle Cohen, Dominique Perrin, and Jean-Eric Pin. On the expressive power of temporal logic. J. Comput. System Sci., 46(3):271–294, June 1993.

    Article  MATH  MathSciNet  Google Scholar 

  5. Samuel Eilenberg. Automata, Languages, and Machines, volume 59-B of Pure and Applied Mathematics. Academic Press, New York, 1976.

    Google Scholar 

  6. Allen E. Emerson. Temporal and modal logic. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, pages 995–1072. Elsevier Science Publishers B. V., Amsterdam, 1990.

    Google Scholar 

  7. Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-order logic with two variables and unary temporal logic. In Proceedings 12th Annual IEEE Symposium on Logic in Computer Science, pages 228–235, Warsaw, Poland, 1997.

    Google Scholar 

  8. Kousha Etessami and Thomas Wilke. An until hierarchy for temporal logic. In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, pages 108–117, New Brunswick, N. J., 1996.

    Google Scholar 

  9. Johan Anthony Willem Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, Calif., 1968.

    Google Scholar 

  10. Fred Kröger. Temporal Logic of Programs. Springer, 1987.

    Google Scholar 

  11. Leslie Lamport. Specifying concurrent program modules. ACMT rans. Programming Lang. Sys., 5(2):190–222, 1983.

    Article  MATH  Google Scholar 

  12. Zohar Manna, Anuchit Anuchitanukul, Nikolaj Bjørner, Anca Browne, Edward Chang, Michael Colón, Luca de Alfaro, Harish Devarajan, Henny Sipma, and Tomas Uribe. STeP: the Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Dept. of Computer Science, Stanford University, Stanford, Calif., 1994.

    Google Scholar 

  13. Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, pages 46–57, Rhode Island, Providence, 1977.

    Google Scholar 

  14. Ben Steinberg. Semidirect products of categories and applications. Journal of Pure and Applied Algebra, 142:153–182, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  15. Howard Straubing. Finite semigroup varieties of the form V.D. J. Pure Appl. Algebra, 36:53–94, 1985.

    Article  MATH  MathSciNet  Google Scholar 

  16. A. Prasad Sistla and Lenore D. Zuck. On the eventuality operator in temporal logic. In Proceedings, Symposium on Logic in Computer Science, pages 153–166, Ithaca, New York, June 1987.

    Google Scholar 

  17. A. Prasad Sistla and Lenore D. Zuck. Reasoning in a restricted temporal logic. Inform. and Computation, 102(2):167–195, February 1993.

    Article  MATH  MathSciNet  Google Scholar 

  18. Denis Thérien. Two-sided wreath product of categories. Journal of Pure and Applied Algebra, 74:307–315, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  19. Denis Thérien and Thomas Wilke. Temporal logic and semidirect products: An effective characterization of the until hierarchy. In Proceedings of the 37th Annual Symposium on Foundations of Computer Science, pages 256–263, Burlington, Vermont, 1996.

    Google Scholar 

  20. Denis Thérien and Thomas Wilke. Over words, two variables are as powerful as one quantifier alternation: FO2 = ∑2∩∏2. In Proceedings of the Thirtieth Annual ACMSymp osium on Theory of Computing, pages 41–47, Dallas, Texas, May 1998.

    Google Scholar 

  21. Brat Tilson. Categories as algebra. J. Pure Appl. Algebra, 48:83–198, 1987.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, McGill University, Montréal, Canada

    Denis Thérien

  2. Computer Science Department, CAU, Kiel, Germany

    Thomas Wilke

Authors
  1. Denis Thérien
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas Wilke
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute for Computer Science, Free University of Berlin, Takustraße 9, 14195, Berlin, Germany

    Helmut Alt

  2. CNRS - I3S - INRIA Sophia Antipolis, 2004 Route des Lucioles, 06902, Sophia Antipolis, France

    Afonso Ferreira

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Thérien, D., Wilke, T. (2002). Nesting Until and Since in Linear Temporal Logic. In: Alt, H., Ferreira, A. (eds) STACS 2002. STACS 2002. Lecture Notes in Computer Science, vol 2285. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45841-7_37

Download citation

  • DOI: https://doi.org/10.1007/3-540-45841-7_37

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43283-8

  • Online ISBN: 978-3-540-45841-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation