ABSTRACT
The aim of this chapter is to present existing propositional temporal logics with branching and partially ordered time. These logics are used for specifying and proving properties of programs and systems. The branching time approach is useful e.g. for nondeterministic programs and can be applied also for concurrent programs. The partial order approach is especially useful for concurrent programs and facilitates the study of more subtle properties than those based on branching time.
A survey of branching time logics, computation tree logics, partial order temporal logics and logics based on event structures is given. The following issues are also discussed: the completeness of proof systems, the finite model property, decidability, model checking and expressiveness of the logics.
