ESSENTIAL TRANSITIONS TO BISIMULATION EQUIVALENCES

Minimization of a labelled transition system (lts) is useful e.g. whil e condensing the global state space of a concurrent system composition ally for verification. In this paper new minimality results for both w eak and branching bisimilarities are proven. It is well known that an equivalent Its with the minimal number of stares can be, in the case o f bisimilarities, found by identifying all equivalent states of an Its . However, the question has been partially open whether an equivalent lts with the minimal number of stales and transitions can be found. We give a proof that for every weak-image-finite Its there is a unique b isimilar Its that contains the minimal number of states and transition s. We study divergence preserving bisimilarities, since divergence - i .e. the possibility to use system resources infinitely without any out put - should not be ignored when liveness properties of systems have t o be checked. Our results are shown to be valid also for commonly used divergence ignoring bisimilarities, weak bisimilarity and branching b isimilarity.