Symmetry in labeled transition systems

Symmetry is defined for labeled transition systems, and it is shown how symmetrical systems can be symmetrically decomposed into components. The central question is under what conditions one such component may represent the whole system, in the sense that one symmetrical system is bisimilar to a second if and only if a component of the first is equivalent to a component of the second. The theory developed is illustrated by three case studies, i.e. the alternating bit protocol, Peterson's algorithm and the Dining Philosophers.