Skip to main content
SpringerLink
Log in

Temporal Logic

  • Chapter
Specification of Software Systems

Part of the book series: Texts in Computer Science ((TCS))

Abstract

In classical logic, the predicate P in “if P∧(P⇒Q) then Q” retains its truth value even after Q has been derived. In other words, in classical logic the truth of a formula is static. However, real-life implications are causal and temporal. To handle these, it must be possible to specify that “an event happened when P was true, moments after that Q became true, and now “P is not true and Q is true”. This may also be stated using “states”. We associate predicates with states such that a predicate is true in some state S and false in some other states.

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 EPUB and 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
Hardcover Book
USD 54.99
Price excludes VAT (USA)
  • Durable hardcover 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

References

  1. Baier C, Katoen JP (2007) Principles of model checking. MIT Press, Cambridge

    Google Scholar 

  2. Ben-Ari M, Pnueli A, Manna Z (1983) The temporal logic of branching time. Acta Inform 20:207–226

    Article  MathSciNet  MATH  Google Scholar 

  3. Büchi JR (1960) On a decision method in restricted second order arithmetic. Z Math Log Grundl Math 6:66–92

    Article  MATH  Google Scholar 

  4. Carnap R (1947) Meaning and necessity. Chicago University Press, Chicago. Enlarged Edition 1956

    MATH  Google Scholar 

  5. Clarke EM, Emerson EA, Sistala AP (1986) Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244–263

    Article  MATH  Google Scholar 

  6. Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge

    Google Scholar 

  7. Courcoubetis C, Vardi M, Wolper P, Yannakakis M (1992) Memory efficient algorithms for the verification of temporal logic properties. Form Methods Syst Des 1:275–288

    Article  Google Scholar 

  8. Dijkstra E (1965) Solutions of a problem in concurrent programming control. Commun ACM 8(9):569

    Article  Google Scholar 

  9. Emerson EA, Clarke EM (1980) Characterizing correctness properties of parallel programs using fixpoints. In: Automata, languages, and programming. Lecture notes in computer science, vol 85, pp 169–181

    Chapter  Google Scholar 

  10. Gabbay D, Pnueli A, Stavi J (1980) The temporal analysis of fairness. In: Proceedings of the seventh ACM symposium on principles of programming languages, January 1980, pp 163–173

    Google Scholar 

  11. Gabbay D, Hodkinson I, Reynolds M (1994) Temporal logic: mathematical foundations and computational aspects. Oxford logic guides, vol 1. Clarendon, Oxford

    Book  MATH  Google Scholar 

  12. Holzmann G (2003) The SPIN model checker: primer and reference manual. Addison-Wesley, Reading

    Google Scholar 

  13. Kripke SA (1963) Semantic considerations on modal logic. Acta Philos Fenn 16:83–94

    MathSciNet  MATH  Google Scholar 

  14. Gröger F (1986) Temporal logic of programs. EATCS monographs on theoretical computer science. Springer, Berlin

    Google Scholar 

  15. Lamport L (1983) What good is temporal logic. In: Proceedings of IFIP’83 congress, information processing. North-Holland, Amsterdam, pp 657–668

    Google Scholar 

  16. Lamport L (1994) The temporal logic of actions. ACM Trans Program Lang Syst 16(3):872–923

    Article  Google Scholar 

  17. Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems—specifications. Springer, New York

    Book  Google Scholar 

  18. Melham TF (1989) Formalizing abstraction mechanisms for hardware verification in higher order logic. PhD thesis, University of Cambridge, August 1989

    Google Scholar 

  19. Moszkowski B (1986) Executing temporal logic programs. Cambridge University Press, Cambridge

    Google Scholar 

  20. Owiciki S, Lamport L (1982) Proving liveness properties of concurrent programs. ACM Trans Program Lang Syst 4(3):455–495

    Article  Google Scholar 

  21. Peterson GL (1981) Myths about the mutual exclusion problem. Inf Process Lett 12(3):115–116

    Article  MATH  Google Scholar 

  22. Pnueli A (1977) The temporal logic of programs. In: Proceedings of the eighteenth symposium on the foundations of computer science, Providence, USA

    Google Scholar 

  23. Pnueli A (1981) The temporal semantics of concurrent programs. Theor Comput Sci 13:45–60

    Article  MathSciNet  MATH  Google Scholar 

  24. Pnueli A (1986) Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends. Lecture notes in computer science, vol 224

    Google Scholar 

  25. Prior A (1957) Time and modality. Oxford University Press, London

    MATH  Google Scholar 

  26. Rescher N, Urquhart A (1971) Temporal logic. Springer, Berlin

    Book  MATH  Google Scholar 

  27. Sistala AP, Vardi M, Wolper P (1983) Reasoning about infinite computation paths. In: Proceedings of the 24th IEEE FOCS, pp 185–194

    Google Scholar 

  28. Sistala AP, Clarke EM (1985) The complexity of linear propositional temporal logic. J ACM 32(3):733–749

    Article  Google Scholar 

  29. Stirling C (1992) Modal and temporal logics. In: Handbook of logic in computer science. Oxford University Press, London

    Google Scholar 

  30. Wan K (2006) Lucx: Lucid Enriched with context. PhD thesis, Concordia University, Montreal, Canada

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. Computer Science and Software Eng., Concordia University, St. Catherine Street West 1515, H3G 1M8, Montreal, Québec, Canada

    Prof. V. S. Alagar

  2. Computer Science Department, University of Wisconsin-La Crosse, State Street 1725, 54601, La Crosse, WI, USA

    Prof. K. Periyasamy

Authors
  1. Prof. V. S. Alagar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Prof. K. Periyasamy
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to V. S. Alagar .

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag London Limited

About this chapter

Cite this chapter

Alagar, V.S., Periyasamy, K. (2011). Temporal Logic. In: Specification of Software Systems. Texts in Computer Science. Springer, London. https://doi.org/10.1007/978-0-85729-277-3_11

Download citation

  • DOI: https://doi.org/10.1007/978-0-85729-277-3_11

  • Publisher Name: Springer, London

  • Print ISBN: 978-0-85729-276-6

  • Online ISBN: 978-0-85729-277-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation