Finite memory devices in CSP

Abstract

It is often said that a state based approach to CSP is inadequate, however we present here some (theoretical) hints against this assertion. A new class of processes modelled by finite memory devices are considered. These devices (called here CSP automata) allow both: deal with the different kinds of nondeterminism at a state level and model misbehaviours due to divergences. They are well adapted to the semantics of failures plus divergences. As CSP is independent of branching time CSP-automata can be determinized. Furthermore we show that an extension of the classical automata's morphism is equivalent to refinement between processes. That allow us to define canonical forms through minimization. These processes can also be characterized by a set of recursive equations so called linear systems. These processes are stable under nondeterminism, change of symbol, prefixing and interleaving.