Modal and Temporal Logics for Processes
Colin Stirling · 1993
We examine modal and temporal logics for processes. In section 1 we intro-duce 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 la-belled graphs, concrete summaries of process behaviour. Various combinations of processes are reviewed. In section 2 modal logic is introduced for describing the capabilities of pro-cesses. An important discussion is when two processes may be deemed, for all practical purposes, to have the same behaviour. We discuss bisimulation equi-valence 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 tem-poral properties (such as liveness and safety) of concurrent systems. A logic expressing temporal notions provides a framework for the precise formalization of such specications. Formulas of the modal logic are not rich enough to express such temporal properties. So extra operators, extremal xed points, are added in section 3. The result is a very expressive temporal logic. The modal and temporal logics provide a repository of useful properties. However it is also very important to be able to verify that an agent has or lacks a particular property. This is the topic of section 4. First we show that property checking can be understood in terms of game playing.We then present sound and complete tableau proof systems for proving temporal properties of processes. The proof method is illustrated on several examples. Finally, concluding comments