Virtual Symmetry Reduction

We provide a general method for ameliorating state explosion via symmetry reduction in certain asymmetric systems, such as systems with many similar, but not identical, processes. The method applies to systems whose structures (i.e., state transition graphs) have more state symmetries than arc symmetries. We introduce a new notion of \virtual symmetry" that strictly subsumes earlier notions of \rough symmetry" and \near symmetry" ET99]. Virtual symmetry is the most general condition under which the structure of a system is naturally bisimilar to its quotient by a group of state symmetries. We give several example systems exhibiting virtual symmetry that are not amenable to symmetry reduction by earlier techniques: a one-lane bridge system, where the n with priority for crossing changes dynamically; an abstract system with asymmetric communication network; and a system with asymmetric resource sharing motivated from the drinking philosophers problem. These examples show ...

• Type: Conference
• Year: 2000
• Where: LICS
• Authors: E. Allen Emerson, John Havlicek, Richard J. Trefler
• Keywords: Asymmetric Systems, Automated Reasoning, LICS 2000, Symmetry Reduction, Virtual Symmetry