Polarized process algebra and program equivalence

Abstract

The basic polarized process algebra is completed yielding as a projective limit a cpo which also comprises infinite processes. It is shown that this model serves in a natural way as a semantics for several program algebras. In particular, the fully abstract model of the program algebra axioms of [2] is considered which results by working modulo behavioral congruence. This algebra is extended with a new basic instruction, named `entry instruction' and denoted with `@'. Addition of l allows many more equations and conditional equations to be stated. It becomes possible to find an axiomatization of program inequality. Technically this axiomatization is an infinite final algebra specification using conditional equations and auxiliary objects.