Modal and Temporal Logics for Processes

Colin Stirling

Preface: In the following we examine modal and temporal logics for processes. First 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 the behaviour of processes. Various combinationsof processes and their resulting behaviour as determined by the transition rules are reviewed.

In section 2 a simple modal logic, a slight extension of Hennessy-Milner 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 beha viour. We discuss bisimulation equivalence as the discriminating power of the 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, a slight extension of mo dal mu-calculus.

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 this 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 examples.

LFCS report ECS-LFCS-92-221

Previous | Index | Next