Process Algebra with Action Dependencies

Process algebras are a frequently used tool for the specification and verification of distributed reactive systems. In process algebras, actions are used to denote the basic entities of systems. In general, actions are just abstract names with no particular interpretation. The semantics of a system description, given in form of a process algebra term, is not in uenced by the choice of names. In this paper, we equip a process algebra with a simple semantics for the actions, given in the form of dependencies. The action dependencies are to be 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 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 present 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 exibility of this process algebra in the design of distributed reactive systems.