Introducing symmetry to graph rewriting systems with process abstraction

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationGraph Transformation - 12th International Conference, ICGT 2019, Held as Part of STAF 2019, Proceedings
EditorsFernando Orejas, Esther Guerra
PublisherSpringer-Verlag
Pages3-20
Number of pages18
ISBN (Print)9783030236106
DOIs
Publication statusPublished - 2019 Jan 1
Event12th International Conference on Graph Transformation, ICGT 2019, Held as part of STAF 2019 - Eindhoven, Netherlands
Duration: 2019 Jul 152019 Jul 16

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11629 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference12th International Conference on Graph Transformation, ICGT 2019, Held as part of STAF 2019
CountryNetherlands
CityEindhoven
Period19/7/1519/7/16

Fingerprint

Graph Rewriting
Rewriting Systems
Symmetry
Symmetry Reduction
Model checking
Model Checking
Graph Isomorphism
Model
State Space
Formal Semantics
Abstraction
Combined Method
Soundness
Modeling Language
Concurrent
Subgraph
Express
Semantics

Keywords

  • Abstraction
  • Graph rewriting systems
  • LMNtal
  • Model checking
  • Symmetry reduction

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Tomioka, T., Tsunekawa, Y., & Ueda, K. (2019). Introducing symmetry to graph rewriting systems with process abstraction. In F. Orejas, & E. Guerra (Eds.), Graph Transformation - 12th International Conference, ICGT 2019, Held as Part of STAF 2019, Proceedings (pp. 3-20). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11629 LNCS). Springer-Verlag. https://doi.org/10.1007/978-3-030-23611-3_1

Introducing symmetry to graph rewriting systems with process abstraction. / Tomioka, Taichi; Tsunekawa, Yutaro; Ueda, Kazunori.

Graph Transformation - 12th International Conference, ICGT 2019, Held as Part of STAF 2019, Proceedings. ed. / Fernando Orejas; Esther Guerra. Springer-Verlag, 2019. p. 3-20 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11629 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Tomioka, T, Tsunekawa, Y & Ueda, K 2019, Introducing symmetry to graph rewriting systems with process abstraction. in F Orejas & E Guerra (eds), Graph Transformation - 12th International Conference, ICGT 2019, Held as Part of STAF 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11629 LNCS, Springer-Verlag, pp. 3-20, 12th International Conference on Graph Transformation, ICGT 2019, Held as part of STAF 2019, Eindhoven, Netherlands, 19/7/15. https://doi.org/10.1007/978-3-030-23611-3_1
Tomioka T, Tsunekawa Y, Ueda K. Introducing symmetry to graph rewriting systems with process abstraction. In Orejas F, Guerra E, editors, Graph Transformation - 12th International Conference, ICGT 2019, Held as Part of STAF 2019, Proceedings. Springer-Verlag. 2019. p. 3-20. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-23611-3_1
Tomioka, Taichi ; Tsunekawa, Yutaro ; Ueda, Kazunori. / Introducing symmetry to graph rewriting systems with process abstraction. Graph Transformation - 12th International Conference, ICGT 2019, Held as Part of STAF 2019, Proceedings. editor / Fernando Orejas ; Esther Guerra. Springer-Verlag, 2019. pp. 3-20 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{6ce00ffe4d5b4bf19c8777ecd8d0e102,
title = "Introducing symmetry to graph rewriting systems with process abstraction",
abstract = "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.",
keywords = "Abstraction, Graph rewriting systems, LMNtal, Model checking, Symmetry reduction",
author = "Taichi Tomioka and Yutaro Tsunekawa and Kazunori Ueda",
year = "2019",
month = "1",
day = "1",
doi = "10.1007/978-3-030-23611-3_1",
language = "English",
isbn = "9783030236106",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "3--20",
editor = "Fernando Orejas and Esther Guerra",
booktitle = "Graph Transformation - 12th International Conference, ICGT 2019, Held as Part of STAF 2019, Proceedings",

}

TY - GEN

T1 - Introducing symmetry to graph rewriting systems with process abstraction

AU - Tomioka, Taichi

AU - Tsunekawa, Yutaro

AU - Ueda, Kazunori

PY - 2019/1/1

Y1 - 2019/1/1

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

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 - Orejas, Fernando

A2 - Guerra, Esther

PB - Springer-Verlag

ER -