Termination, deadlock, and divergence

Publisher Website
Google Scholar
Abstract
In this paper, a process algebra that incorporates explicit representations of successful termination, deadlock, and divergence is introduced and its semantic theory is analyzed. Both an operational and a denotational semantics for the language is given and it is shown that they agree. The operational theory is based upon a suitable adaptation of the notion of bisimulation preorder. The denotational semantics for the language is given in terms of the initial continuous algebra that satisfies a set of equations E, CIE. It is shown that CIE is fully abstract with respect to our choice of behavioral preorder. Several results of independent interest are obtained; namely, the finite approximability of the behavioral preorder and a partial completeness result for the set of equations E with respect to the preorder.

This publication has 19 references indexed in Scilit: