An algebraic theory of fair asynchronous communicating processes.

*(English)*Zbl 0566.68022
Automata, languages and programming, 12th Colloq., Nafplion/Greece 1985, Lect. Notes Comput. Sci. 194, 260-269 (1985).

[For the entire collection see Zbl 0563.00018.]

A language for defining fair asynchronous communicating processes is presented. The main operator is a binary composition operator \(\|:p\| q\) represents processes p and q linked together asynchronously but ”fairly”. In addition the language has a mechanism for abstracting away from internal components of a process. A denotational semantics is given for the language. The domain used consists of certain kinds of finite-branching trees which may have limit points associated with their infinite paths. The semantics is algebraic in the sense that every operator in the language is interpreted as a function over the domain. Each of these functions are continuous, except that associated with \(\|\), which is monotonic. The model satisfies a large collection of equations which supports a transformational proof system for processes. The model is also fully-abstract with respect to a natural notion of testing equivalence. Moreover we show that no fully-abstract model can be continuous.

A language for defining fair asynchronous communicating processes is presented. The main operator is a binary composition operator \(\|:p\| q\) represents processes p and q linked together asynchronously but ”fairly”. In addition the language has a mechanism for abstracting away from internal components of a process. A denotational semantics is given for the language. The domain used consists of certain kinds of finite-branching trees which may have limit points associated with their infinite paths. The semantics is algebraic in the sense that every operator in the language is interpreted as a function over the domain. Each of these functions are continuous, except that associated with \(\|\), which is monotonic. The model satisfies a large collection of equations which supports a transformational proof system for processes. The model is also fully-abstract with respect to a natural notion of testing equivalence. Moreover we show that no fully-abstract model can be continuous.

##### MSC:

68N25 | Theory of operating systems |