Fifteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 2000)

Paper: Virtual Symmetry Reduction (at LICS 2000)

Authors: E. Allen Emerson John W. Havlicek Richard J. Trefler


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 direction 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 that virtual symmetry reduction applies to a significantly broader class of asymmetric systems than could be handled before.


    author = 	 {E. Allen Emerson and John W. Havlicek and Richard J. Trefler},
    title = 	 {Virtual Symmetry Reduction},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2000},
    year =	 2000,
    editor =	 {Martin Abadi},
    month =	 {June}, 
    pages =      {121--131},
    location =   {Santa Barbara, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}