Decomposability, Decidability and Axiomatisability for Bisimulation Equivalence on Basic Parallel Processes

S Christensen, Y Hirshfield and F Moller

Abstract: We prove the decidability of two subclasses of recursive processes involving a parallel composition operator with respect to bisimulation equivalence, namely the so-called normed and live processes. To accomplish this, we first prove a unique decomposition result for (a generalisation of) normed processes, in order to deduce a necessary cancellation law. The decidability proof permits us further to present a complete axiomatisation for these process classes.

LFCS report ECS-LFCS-92-244

Previous | Index | Next