Propositional temporal logics and their use in model checking
For the sake of proving correctness of programs with respect to their specifications, a number of formalisms exist. A traditional one has been proof systems involving Floyd-Hoare correctness formulae. More recently, especially with regard to concurrent programs such as air traffic control systems or operating systems, which are nonterminating and concurrent, and in connection with the desire for automatic verification, other formalisms have been found to be more useful. This paper, and the following one, survey two such types of formalism which have proved to be particularly successful for efficient automatic verification, or “model checking”. In this paper we consider branching time propositional temporal logics, which serves as a good introduction for the more general formalism of the propositional μ-calculus, which is considered in the next paper. The emphasis is on a broad understanding rather than on technical details.
KeywordsModel Check Modal Logic Temporal Logic Future State Proof System
Unable to display preview. Download preview PDF.
- Clarke, E.M., Emerson, E.A. (1981): Design and synthesis of synchronization skeletons using branching time temporal logic. Proc. Workshop on Logics of Programs, Yorktown Heights, NY. Lecture Notes in Computer Science, 131, Springer-VerlagGoogle Scholar
- Clarke, E.M., Emerson, E.A., Sistla, A.P. (1983): Automatic verification of finite state concurrent systems using temporal specifications: A practical approach. Proc. 10th Annual ACM Symp. on Principles of Programming Languages, Austin, TX, 117–126.Google Scholar
- Clarke, E.M., Emerson, E.A., Sistla, A.P. (1986): Automatic verification of finite state concurrent programs using temporal logic. ACM TOPLAS 8, 244–263.Google Scholar
- Emerson, E.A. (1990): Temporal and modal logic. In: Handbook of Theoretical Computer Science, Vol. B: Formal Models and Semantics (ed. J. van Leeuwen), Elsevier, 995–1072.Google Scholar
- Emerson, E.A., Srinivasan, A.J. (1988): Branching time temporal logic. In: Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency: School/Workshop, Noorwijkerhout, The Netherlands, May/June 1988 (ed. J.W. de Bakker, W.P. de Roever, G. Rozenberg). Lecture Notes in Computer Science, 354, Springer-Verlag.Google Scholar
- Pnueli, A. (1977): The temporal logic of programs. 18th Annual Symp. on the Foundations of Computer Science, Providence, RI, 46–57.Google Scholar
- Stirling, C. (1992): modal and temporal logics. In: Handbook of Logic in Computer Science (ed. S. Abramsky, D. Gabbay, T. Maibaum), Oxford University Press, to appear.Google Scholar
- Zucker, J. (1992): The propositional μ-calculus and its use in model checking. In this volume.Google Scholar