Receptive process theory

In essence, this paper reworks Hoare's theory of Communicating Sequential Processes under the above assumption about communication and verifies algebraically the design of a Muller C-element from a majority-element.

Abstract

An algebraic theory of receptive processes is presented. A receptive process models the interaction by input events and output events between a system and its environment. Input from the environment and output to the environment are never blocked; but if a system is not ready to receive a particular input, its subsequent behaviour is undefined. In essence, this paper reworks Hoare's theory of Communicating Sequential Processes under the above assumption about communication. The resulting model is more attractive than the failures-divergences model of CSP because the refusal sets of the latter are simplified out of existence. Like CSP, receptive process theory is equipped with a sound and complete set of algebraic laws. Applications of the theory include the design of asynchronous circuits and the study of data flow networks. As an example, this paper verifies algebraically the design of a Muller C-element from a majority-element.