## 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