Partial order based design of concurrent systems

Abstract

A partial order based graph model for concurrency is introduced, using hierarchical structured graphs with relations denoting concurrency, causal ordering, and temporal ordering. Both compositionally structured processes as well as partial order based structures describing the semantics of processes can be expressed in this unified framework. Thus we obtain a powerful calculus that allows to algebraically transform processes or to prove properties of them. Apart from algebraic properties we also study state based properties of the process language, by means of assertional techniques. We use the combination of the two to derive, in a number of transformation and refinement steps, a distributed minimum weight spanning tree algorithm, in the style of Gallagher, Humblet, and Spira.