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.

Software/Program Verification (acm D.2.4), Specifying and Verifying and Reasoning about Programs (acm F.3.1)
Finite automorphism groups of algebraic, geometric, or combinatorial structures (msc 20B25), Specification and verification (program logics, model checking, etc.) (msc 68Q60)
Software Engineering [SEN]

van Langevelde, I.A. (2003). Symmetry in labeled transition systems. Software Engineering [SEN]. CWI.