Process Algebra with Action Dependencies

In this paper, we present a process algebra with a minimal form of semantics for actions given by dependencies. Action dependencies are interpreted in the Mazurkiewicz sense: independent actions should be able to commute, or (from a different perspective) should be unordered, whereas dependent actions are always ordered. In this approach, the process algebra operators are used to describe the conceptual behavioural structure of the system, and the action dependencies determine the minimal necessary orderings and thereby the additionally possible parallelism within this structure. In previous work on the semantics of specifications using Mazurkiewicz dependencies, the main interest has been on linear time. We present in this paper a branching time semantics, both operationally and denotationally. For this purpose, we introduce a process algebra that incorporates, besides some standard operators, also an operator for action refinement. For interpreting the operators in the presence of action dependencies, a new concept of partial termination has to be developed. We show consistency of the operational and denotational semantics; furthermore, we give a axiomatisation of bisimilarity, which is complete for finite terms. Some small examples demonstrate the flexibility of this process algebra in the design of distributed reactive systems.