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 An error occured whilst processing this directive