Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

1-2016

Abstract

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 patterns need to satisfy to be easily incorporated in the verification/synthesis. We show how these properties can help identify symmetry patterns in examples like dining philosopher protocols, self-stabilising protocols, and prioritised resource-allocator protocol. In some cases (e.g. Gries’s coffee can problem), our technique automatically synthesises a safety-preserving finite approximant, which can then be verified for safety solely using a finite-state model checker.

Keywords

Permutation Group, Concurrent System, Pushdown Automaton, Symmetry Pattern, Regular Relation

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2016, St. Petersburg, FL, USA, January 17–19

Volume

9583

First Page

455

Last Page

475

ISBN

9783662491218

Identifier

10.1007/978-3-662-49122-5_22

Publisher

Springer Link

City or Country

St. Petersburg, Florida

Additional URL

https://doi.org/10.1007/978-3-662-49122-5_22

Download

Share

COinS