Graph Subsumption in Abstract State Space Exploration

Eduardo Zambon
(University of Twente)
Arend Rensink
(University of Twente)

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.

In Anton Wijs, Dragan Bošnački and Stefan Edelkamp: Proceedings First Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2012), Tallinn, Estonia, 1st April 2012, Electronic Proceedings in Theoretical Computer Science 99, pp. 35–49.
Published: 23rd October 2012.

ArXived at: http://dx.doi.org/10.4204/EPTCS.99.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org