Skip to main content
SpringerLink
Log in

Regular Linear Temporal Logic with Past

  • Conference paper
Verification, Model Checking, and Abstract Interpretation (VMCAI 2010)

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

Abstract

This paper upgrades Regular Linear Temporal Logic (RLTL) with past operators and complementation. RLTL is a temporal logic that extends the expressive power of linear temporal logic (LTL) to all ω-regular languages. The syntax of RLTL consists of an algebraic signature from which expressions are built. In particular, RLTL does not need or expose fix-point binders (like linear time μ-calculus), or automata to build and instantiate operators (like \({\textrm{ETL}_*}\)).

Past operators are easily introduced in RLTL via a single previous-step operator for basic state formulas. The satisfiability and model checking problems for RLTL are PSPACE-complete, which is optimal for extensions of LTL. This result is shown using a novel linear size translation of RLTL expressions into 2-way alternating parity automata on words. Unlike previous automata-theoretic approaches to LTL, this construction is compositional (bottom-up). As alternating parity automata can easily be complemented, the treatment of negation is simple and does not require an upfront transformation of formulas into any normal form.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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. Barringer, H., Kuiper, R., Pnueli, A.: A really abstract concurrent model and its temporal logic. In: POPL 1986 (1986)

    Google Scholar 

  2. Bauer, A., Leucker, M., Streit, J.: SALT—structured assertion language for temporal logic. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 757–775. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  3. Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 363. Springer, Heidelberg (2001)

    Google Scholar 

  4. Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.Y.: Regular vacuity. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 191–206. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  5. Dax, C., Klaedtke, F.: Alternation elimination by complementation. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 214–229. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  6. Emerson, A., Clarke, E.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85. Springer, Heidelberg (1980)

    Google Scholar 

  7. Fisman, D., Eisner, C., Havlicek, J.: Formal syntax and Semantics of PSL: Appendix B of Accellera Property Language Reference Manual, Version 1.1. (2004)

    Google Scholar 

  8. Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal basis of fairness. In: POPL 1980 (1980)

    Google Scholar 

  9. Harel, D., Peleg, D.: Process logic with regular formulas. TCS 38, 307–322 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  10. Henriksen, J., Thiagarajan, P.S.: Dynamic linear time temporal logic. Annals of Pure and Applied Logic 96(1-3), 187–207 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  11. Hopcroft, J., Ullman, J.: Introduction to automata theory, languages and computation. Addison-Wesley, Reading (1979)

    MATH  Google Scholar 

  12. Kamp, H.: Tense Logic and the Theory of Linear Order. PhD thesis, UCLA (1968)

    Google Scholar 

  13. Kozen, D.: Results on the propositional μ-calculus. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140. Springer, Heidelberg (1982)

    Chapter  Google Scholar 

  14. Kupferman, O., Piterman, N., Vardi, M.: Extended temporal logic revisited. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, p. 519. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  15. Lange, M.: Weak automata for the linear time μ-calculus. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 267–281. Springer, Heidelberg (2005)

    Google Scholar 

  16. Lange, M.: Linear time logics around PSL: Complexity, expressiveness, and a little bit of succinctness. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 90–104. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  17. Laroussinie, F., Markey, N., Schnoebelen, Ph.: Temporal logic with forgettable past. In: LICS 2002 (2002)

    Google Scholar 

  18. Leucker, M., Sánchez, C.: Regular linear temporal logic. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 291–305. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  19. Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193. Springer, Heidelberg (1985)

    Google Scholar 

  20. Manna, Z., Pnueli, A.: Temporal Verif. of Reactive Systems. Springer, Heidelberg (1995)

    Google Scholar 

  21. Muller, D., Schupp, P.: Altenating automata on infinite trees. TCS 54, 267–276 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  22. Müller-Olm, M.: A modal fixpoint logic with chop. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 510–520. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  23. Pnueli, A.: The temporal logic of programs. In: FOCS 1977 (1977)

    Google Scholar 

  24. Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Logics and models of concurrent systems, NATO ASI F-13. Springer, Heidelberg (1985)

    Google Scholar 

  25. Pnueli, A.: Applications of temporal logic to the specification and verification of reactive systems–a survey of current trends. In: Current Trends in Concurrency. LNCS, vol. 224. Springer, Heidelberg (1986)

    Chapter  Google Scholar 

  26. Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  27. Schnoebelen, Ph.: The complexity of temporal logic model checking. In: AiML 2002 (2002)

    Google Scholar 

  28. Sistla, A.P., Clarke, E.: The complexity of propositional linear termporal logics. JACM 32(3), 733–749 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  29. Stockmeyer, L.: The Computational Complexity of Word Problems. PhD thesis. MIT (1974)

    Google Scholar 

  30. Vardi, M.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043. Springer, Heidelberg (1996)

    Google Scholar 

  31. Vardi, M., Wolper, P.: Reasoning about infinite computations. Inf. Comp. 115, 1–37 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  32. Wolper, P.: Temporal logic can be more expressive. Info.& Control 56, 72–99 (1983)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Madrid Institute for Advanced Studies (IMDEA Software), Spain

    César Sánchez

  2. Spanish Council for Scientific Research (CSIC), Spain

    César Sánchez

  3. Technische Universität München, Germany

    Martin Leucker

Authors
  1. César Sánchez
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Leucker
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Facultad de Informatica (UPM), IMDEA Software, Campus Montegancedo, 28660 Boadilla del Monte, Madrid, Spain

    Gilles Barthe

  2. Facultad de Informatica (UPM), IMDEA Software and Technical University of Madrid, Campus Montegancedo, 28660 Boadilla del Monte, Madrid, Spain

    Manuel Hermenegildo

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sánchez, C., Leucker, M. (2010). Regular Linear Temporal Logic with Past. In: Barthe, G., Hermenegildo, M. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2010. Lecture Notes in Computer Science, vol 5944. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11319-2_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-11319-2_22

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-11318-5

  • Online ISBN: 978-3-642-11319-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation