Regular Symmetry Patterns

3 years 14 days ago
Regular Symmetry Patterns
Symmetry reduction is a well-known approach for alleviating the state explosion problem in model checking. Automatically identifying symmetries in concurrent systems, however, is computationally expensive. We propose a symbolic framework for capturing symmetry patterns in parameterised systems (i.e. an infinite family of finite-state systems): two regular word transducers to represent, respectively, parameterised systems and symmetry patterns. The framework subsumes various types of “symmetry relations” ranging from weaker notions (e.g. simulation preorders) to the strongest notion (i.e. isomorphisms). Our framework enjoys two algorithmic properties: (1) symmetry verification: given a transducer, we can automatically check whether it is a symmetry pattern of a given system, and (2) symmetry synthesis: we can automatically generate a symmetry pattern for a given system in the form of a transducer. Furthermore, our symbolic language allows additional constraints that the symmetry ...
Anthony W. Lin, Truong Khanh Nguyen, Philipp R&uum
Added 11 Apr 2016
Updated 11 Apr 2016
Type Journal
Year 2016
Authors Anthony W. Lin, Truong Khanh Nguyen, Philipp Rümmer, Jun Sun 0001
Comments (0)