TY - GEN
T1 - Introducing symmetry to graph rewriting systems with process abstraction
AU - Tomioka, Taichi
AU - Tsunekawa, Yutaro
AU - Ueda, Kazunori
N1 - Funding Information:
Acknowledgments. The authors would like to thank anonymous reviewers for their useful comments. This work was partially supported by Grant-in-Aid for Scientific Research (B) JP18H03223, JSPS, Japan.
PY - 2019
Y1 - 2019
N2 - Symmetry reduction in model checking is a technique for reducing state spaces by exploiting the inherent symmetry of models, i.e., the interchangeability of their subcomponents. Model abstraction, which abstracts away the details of models, often strengthens the symmetry of the models. Graph rewriting systems allow us to express models in such a way that inherent symmetry manifests itself with graph isomorphism of states. In graph rewriting, the synergistic effect of symmetry reduction and model abstraction is obtained under graph isomorphism. This paper proposes a method for abstracting programs described in a hierarchical graph rewriting language LMNtal. The method automatically finds and abstracts away subgraphs of a graph rewriting system that are irrelevant to the results of model checking. The whole framework is developed within the syntax and the formal semantics of the modeling language LMNtal without introducing new domains or languages. We show that the proposed abstraction method combined with symmetry reduction reduces state spaces while preserving the soundness of model checking. We implemented the method on SLIM, an implementation of LMNtal with an LTL model checker, tested it with various concurrent algorithms, and confirmed that it automatically reduces the number of states by successfully extracting the symmetry of models.
AB - Symmetry reduction in model checking is a technique for reducing state spaces by exploiting the inherent symmetry of models, i.e., the interchangeability of their subcomponents. Model abstraction, which abstracts away the details of models, often strengthens the symmetry of the models. Graph rewriting systems allow us to express models in such a way that inherent symmetry manifests itself with graph isomorphism of states. In graph rewriting, the synergistic effect of symmetry reduction and model abstraction is obtained under graph isomorphism. This paper proposes a method for abstracting programs described in a hierarchical graph rewriting language LMNtal. The method automatically finds and abstracts away subgraphs of a graph rewriting system that are irrelevant to the results of model checking. The whole framework is developed within the syntax and the formal semantics of the modeling language LMNtal without introducing new domains or languages. We show that the proposed abstraction method combined with symmetry reduction reduces state spaces while preserving the soundness of model checking. We implemented the method on SLIM, an implementation of LMNtal with an LTL model checker, tested it with various concurrent algorithms, and confirmed that it automatically reduces the number of states by successfully extracting the symmetry of models.
KW - Abstraction
KW - Graph rewriting systems
KW - LMNtal
KW - Model checking
KW - Symmetry reduction
UR - http://www.scopus.com/inward/record.url?scp=85069168015&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85069168015&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-23611-3_1
DO - 10.1007/978-3-030-23611-3_1
M3 - Conference contribution
AN - SCOPUS:85069168015
SN - 9783030236106
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 3
EP - 20
BT - Graph Transformation - 12th International Conference, ICGT 2019, Held as Part of STAF 2019, Proceedings
A2 - Guerra, Esther
A2 - Orejas, Fernando
PB - Springer Verlag
T2 - 12th International Conference on Graph Transformation, ICGT 2019, Held as part of STAF 2019
Y2 - 15 July 2019 through 16 July 2019
ER -