Star-Topology Decoupling in SPIN

Daniel Gnad, Patrick Dubbert, Alberto Lluch Lafuente, Jorg Hoffmann

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

287 Downloads (Pure)

Abstract

Star-topology decoupling is a state space search method recently introduced in AI Planning. It decomposes the input model into components whose interaction structure has a star shape. The decoupled search algorithm enumerates transition paths only for the center component, maintaining the leaf-component state space separately for each leaf. This is a form of partial-order reduction, avoiding interleavings across leaf components. It can, and often does, have exponential advantages over stubborn set pruning and unfolding. AI Planning relates closely to model checking of safety properties, so the question arises whether decoupled search can be successful in model checking as well. We introduce a first implementation of star-topology decoupling in SPIN, where the center maintains global variables while the leaves maintain local ones. Preliminary results on several case studies attest to the potential of the approach.

Original languageEnglish
Title of host publicationSPIN 2018: Model Checking Software
PublisherSpringer
Publication date2018
Pages103-114
ISBN (Print)978-3-319-94110-3
DOIs
Publication statusPublished - 2018
Event2018 International Symposium on Model Checking Software - University of Malaga, Málaga, Spain
Duration: 20 Jun 201822 Jun 2018

Conference

Conference2018 International Symposium on Model Checking Software
LocationUniversity of Malaga
Country/TerritorySpain
CityMálaga
Period20/06/201822/06/2018

Fingerprint

Dive into the research topics of 'Star-Topology Decoupling in SPIN'. Together they form a unique fingerprint.

Cite this