Graph Subsumption in Abstract State Space Exploration

TL;DR

This paper extends an abstract graph-based state space exploration method with a subsumption reduction technique, significantly reducing state space size and computational resources needed.

Contribution

It introduces a subsumption-based reduction for neighbourhood abstraction, improving efficiency in abstract state space exploration.

Findings

Subsumption drastically reduces state space size.

Resource consumption (time and memory) is significantly lowered.

The method is effective across various experiments.

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.