J.I. Zucker (1993):
Propositional temporal logics and their use in model checking,
in Functional Programming, Concurrency, Simulation and
Automated Reasoning,
ed. P.E. Lauer,
Lecture Notes in Computer Science 693 (Springer-Verlag), 108-116.
[text.ps]
Abstract.
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 mu-calculus,
which is considered in the next paper.
The emphasis is on a broad understanding rather than on
technical details.