Advertisement

Temporal Logic

  • V. S. Alagar
  • K. Periyasamy
Part of the Texts in Computer Science book series (TCS)

Abstract

In classical logic, the predicate P in “if P∧(PQ) 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.

Keywords

Model Check Temporal Logic Classical Logic Safety Property Program Graph 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Baier C, Katoen JP (2007) Principles of model checking. MIT Press, Cambridge Google Scholar
  2. 2.
    Ben-Ari M, Pnueli A, Manna Z (1983) The temporal logic of branching time. Acta Inform 20:207–226 MathSciNetMATHCrossRefGoogle Scholar
  3. 3.
    Büchi JR (1960) On a decision method in restricted second order arithmetic. Z Math Log Grundl Math 6:66–92 MATHCrossRefGoogle Scholar
  4. 4.
    Carnap R (1947) Meaning and necessity. Chicago University Press, Chicago. Enlarged Edition 1956 MATHGoogle Scholar
  5. 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 MATHCrossRefGoogle Scholar
  6. 6.
    Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge Google Scholar
  7. 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 CrossRefGoogle Scholar
  8. 8.
    Dijkstra E (1965) Solutions of a problem in concurrent programming control. Commun ACM 8(9):569 CrossRefGoogle Scholar
  9. 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 CrossRefGoogle Scholar
  10. 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. 11.
    Gabbay D, Hodkinson I, Reynolds M (1994) Temporal logic: mathematical foundations and computational aspects. Oxford logic guides, vol 1. Clarendon, Oxford MATHCrossRefGoogle Scholar
  12. 12.
    Holzmann G (2003) The SPIN model checker: primer and reference manual. Addison-Wesley, Reading Google Scholar
  13. 13.
    Kripke SA (1963) Semantic considerations on modal logic. Acta Philos Fenn 16:83–94 MathSciNetMATHGoogle Scholar
  14. 14.
    Gröger F (1986) Temporal logic of programs. EATCS monographs on theoretical computer science. Springer, Berlin Google Scholar
  15. 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. 16.
    Lamport L (1994) The temporal logic of actions. ACM Trans Program Lang Syst 16(3):872–923 CrossRefGoogle Scholar
  17. 17.
    Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems—specifications. Springer, New York CrossRefGoogle Scholar
  18. 18.
    Melham TF (1989) Formalizing abstraction mechanisms for hardware verification in higher order logic. PhD thesis, University of Cambridge, August 1989 Google Scholar
  19. 19.
    Moszkowski B (1986) Executing temporal logic programs. Cambridge University Press, Cambridge Google Scholar
  20. 20.
    Owiciki S, Lamport L (1982) Proving liveness properties of concurrent programs. ACM Trans Program Lang Syst 4(3):455–495 CrossRefGoogle Scholar
  21. 21.
    Peterson GL (1981) Myths about the mutual exclusion problem. Inf Process Lett 12(3):115–116 MATHCrossRefGoogle Scholar
  22. 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. 23.
    Pnueli A (1981) The temporal semantics of concurrent programs. Theor Comput Sci 13:45–60 MathSciNetMATHCrossRefGoogle Scholar
  24. 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. 25.
    Prior A (1957) Time and modality. Oxford University Press, London MATHGoogle Scholar
  26. 26.
    Rescher N, Urquhart A (1971) Temporal logic. Springer, Berlin MATHCrossRefGoogle Scholar
  27. 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. 28.
    Sistala AP, Clarke EM (1985) The complexity of linear propositional temporal logic. J ACM 32(3):733–749 CrossRefGoogle Scholar
  29. 29.
    Stirling C (1992) Modal and temporal logics. In: Handbook of logic in computer science. Oxford University Press, London Google Scholar
  30. 30.
    Wan K (2006) Lucx: Lucid Enriched with context. PhD thesis, Concordia University, Montreal, Canada Google Scholar

Copyright information

© Springer-Verlag London Limited 2011

Authors and Affiliations

  1. 1.Dept. Computer Science and Software Eng.Concordia UniversityMontrealCanada
  2. 2.Computer Science DepartmentUniversity of Wisconsin-La CrosseLa CrosseUSA

Personalised recommendations