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.