Graph Subsumption in Abstract State Space Exploration

Eduardo Zambon, Arend Rensink

Abstract

In this paper we present the extension of an existing method for abstract graph-based state space exploration, called neighbourhood abstraction, with a reduction technique based on subsumption. Basically, one abstract state subsumes another when it covers more concrete states; in such a case, the subsumed state need not be included in the state space, thus giving a reduction. We explain the theory and especially also report on a number of experiments, which show that subsumption indeed drastically reduces both the state space and the resources (time and memory) needed to compute it.
Original languageUndefined
Title of host publicationProceedings of First Workshop on Graph Inspection and Traversal Engineering (GRAPHite 2012)
EditorsA. Wijs, D. Bosnacki, S. Edelkamp
PublisherOpen Publishing Association
Pages35-49
Number of pages15
DOIs
StatePublished - Apr 2012

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
Volume99
ISSN (Print)2075-2180
ISSN (Electronic)2075-2180

Fingerprint

Experiments

Keywords

  • EWI-22467
  • Graph Transformation
  • GROOVE
  • METIS-289768
  • IR-82192
  • Abstract State Space Exploration
  • Symmetry Reduction

Cite this

Zambon, E., & Rensink, A. (2012). Graph Subsumption in Abstract State Space Exploration. In A. Wijs, D. Bosnacki, & S. Edelkamp (Eds.), Proceedings of First Workshop on Graph Inspection and Traversal Engineering (GRAPHite 2012) (pp. 35-49). (Electronic Proceedings in Theoretical Computer Science; Vol. 99). Open Publishing Association. DOI: 10.4204/EPTCS.99.6

Zambon, Eduardo; Rensink, Arend / Graph Subsumption in Abstract State Space Exploration.

Proceedings of First Workshop on Graph Inspection and Traversal Engineering (GRAPHite 2012). ed. / A. Wijs; D. Bosnacki; S. Edelkamp. Open Publishing Association, 2012. p. 35-49 (Electronic Proceedings in Theoretical Computer Science; Vol. 99).

Research output: Scientific - peer-reviewConference contribution

@inbook{cd35ce3293b349a9a7d854a4e374ab03,
title = "Graph Subsumption in Abstract State Space Exploration",
abstract = "In this paper we present the extension of an existing method for abstract graph-based state space exploration, called neighbourhood abstraction, with a reduction technique based on subsumption. Basically, one abstract state subsumes another when it covers more concrete states; in such a case, the subsumed state need not be included in the state space, thus giving a reduction. We explain the theory and especially also report on a number of experiments, which show that subsumption indeed drastically reduces both the state space and the resources (time and memory) needed to compute it.",
keywords = "EWI-22467, Graph Transformation, GROOVE, METIS-289768, IR-82192, Abstract State Space Exploration, Symmetry Reduction",
author = "Eduardo Zambon and Arend Rensink",
note = "Open Access",
year = "2012",
month = "4",
doi = "10.4204/EPTCS.99.6",
series = "Electronic Proceedings in Theoretical Computer Science",
publisher = "Open Publishing Association",
pages = "35--49",
editor = "A. Wijs and D. Bosnacki and S. Edelkamp",
booktitle = "Proceedings of First Workshop on Graph Inspection and Traversal Engineering (GRAPHite 2012)",

}

Zambon, E & Rensink, A 2012, Graph Subsumption in Abstract State Space Exploration. in A Wijs, D Bosnacki & S Edelkamp (eds), Proceedings of First Workshop on Graph Inspection and Traversal Engineering (GRAPHite 2012). Electronic Proceedings in Theoretical Computer Science, vol. 99, Open Publishing Association, pp. 35-49. DOI: 10.4204/EPTCS.99.6

Graph Subsumption in Abstract State Space Exploration. / Zambon, Eduardo; Rensink, Arend.

Proceedings of First Workshop on Graph Inspection and Traversal Engineering (GRAPHite 2012). ed. / A. Wijs; D. Bosnacki; S. Edelkamp. Open Publishing Association, 2012. p. 35-49 (Electronic Proceedings in Theoretical Computer Science; Vol. 99).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Graph Subsumption in Abstract State Space Exploration

AU - Zambon,Eduardo

AU - Rensink,Arend

N1 - Open Access

PY - 2012/4

Y1 - 2012/4

N2 - In this paper we present the extension of an existing method for abstract graph-based state space exploration, called neighbourhood abstraction, with a reduction technique based on subsumption. Basically, one abstract state subsumes another when it covers more concrete states; in such a case, the subsumed state need not be included in the state space, thus giving a reduction. We explain the theory and especially also report on a number of experiments, which show that subsumption indeed drastically reduces both the state space and the resources (time and memory) needed to compute it.

AB - In this paper we present the extension of an existing method for abstract graph-based state space exploration, called neighbourhood abstraction, with a reduction technique based on subsumption. Basically, one abstract state subsumes another when it covers more concrete states; in such a case, the subsumed state need not be included in the state space, thus giving a reduction. We explain the theory and especially also report on a number of experiments, which show that subsumption indeed drastically reduces both the state space and the resources (time and memory) needed to compute it.

KW - EWI-22467

KW - Graph Transformation

KW - GROOVE

KW - METIS-289768

KW - IR-82192

KW - Abstract State Space Exploration

KW - Symmetry Reduction

U2 - 10.4204/EPTCS.99.6

DO - 10.4204/EPTCS.99.6

M3 - Conference contribution

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 35

EP - 49

BT - Proceedings of First Workshop on Graph Inspection and Traversal Engineering (GRAPHite 2012)

PB - Open Publishing Association

ER -

Zambon E, Rensink A. Graph Subsumption in Abstract State Space Exploration. In Wijs A, Bosnacki D, Edelkamp S, editors, Proceedings of First Workshop on Graph Inspection and Traversal Engineering (GRAPHite 2012). Open Publishing Association. 2012. p. 35-49. (Electronic Proceedings in Theoretical Computer Science). Available from, DOI: 10.4204/EPTCS.99.6