On the relationship between process algebra and input/output automata

Abstract

The relationship between process algebra and input/output (I/O) automata models is investigated in a general setting of structured operational semantics. For a series of (approximations of) key properties of I/O automata, syntactic constraints on inference rules that guarantee these properties are proposed. A first result is that in a setting without assumptions about actions, trace and failure preorders are substitutive for any set of rules in a format due to R. de Simone (thesis, Univ. of Paris, 1984). Next, additional constraints that capture the notion of internal actions and guarantee substitutivity of the testing preorders of R. De Nicola and M. Hennessy (1984) and also of a preorder related to the failure semantics with fair abstraction of unstable divergence of J.A. Bergstra et al. (1988) are imposed. Subsequent constraints guarantee that input actions are always enabled and output actions cannot be blocked, two key features of I/O automata. The main result is that for any I/O calculus, i.e. a de Simone calculus that combines the constraints for internal, input and output actions, the quiescent trace preorder and the fair trace preorder are substitutive.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">&gt;</ETX>