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 …