CSP, partial automata, and coalgebras

The paper presents a first reconstruction of Hoare's theory of CSP in terms of partial automata and related coalgebras. We show that the concepts of processes in Hoare (Communicating Sequential Processes, Prentice-Hall, Englewood Cliffs, NJ, 1985) are strongly related to the concepts of states for special, namely, final partial automata. Moreover, we show how the deterministic and nondeterministic operations in Hoare (1985) can be interpreted in a compatible way by constructions on the semantical level of automata. Based on this, we are able to interpret finite process expressions as representing finite partial automata with designated initial states. In such a way we provide a new method for solving recursive process equations which is based on the concept of final automata. The coalgebraic reconstruction of CSP allows us to use coinduction as a new proof principle. To make evident the usefulness of this principle we prove some example laws from Hoare (1985). (C) 2002 Elsevier Science B.V. All rights reserved.