Semantics of concurrent systems: A modular fixed-point trace approach

A method for finding the set of processes generated by a concurrent system (the behaviour of a system) in modular way is presented and the fixed point method of describing sets of processes is extensively applied, with processes regarded as traces rather than strings of actions.

Abstract

A method for finding the set of processes generated by a concurrent system (the behaviour of a system) in modular way is presented. A system is decomposed into modules with behaviours assumed to be known and then the behaviours are successively put together giving finally the initial system behaviour. It is shown that there is much of freedom in choice of modules; in extreme case atoms of a system, i.e. subsystems containing only one resource, can be taken as modules; each atom has its behaviour defined a proiri. The basic operation used for composing behaviours is the synchronization operation defined in the paper. The fixed point method of describing sets of processes is extensively applied, with processes regarded as traces rather than strings of actions.