Modal and Temporal Logics for Processes

Preface We examine modal and temporal logics for processes. In section 1 we introduce concurrent processes as terms of an algebraic language comprising a few basic operators, as developed by Milner, Hoare and others. Their behaviours are described using transitions. Families of transitions can be arranged as labelled graphs, concrete summaries of process behaviour. Various combinations of processes are reviewed. In section 2 modal logic is introduced for describing the capabilities of processes. An important discussion is when two processes may be deemed, for all practical purposes, to have the same behaviour. We discuss bisimulation equivalence as the discriminating power of modal logic is tied to it. This equivalence is initially presented in terms of games. More generally practitioners have found it useful to be able to express temporal properties (such as liveness and safety) of concurrent systems. A logic expressing temporal notions provides a framework for the precise formalization of such specifications. Formulas of the modal logic are not rich enough to express such temporal properties. So extra operators, extremal fixed points, are added in section 3. The result is a very expressive temporal logic