Please use this identifier to cite or link to this item: doi:10.22028/D291-29300
Volltext verfügbar? / Dokumentlieferung
Title: Star-Topology Decoupling in SPIN
Author(s): Gnad, Daniel
Dubbert, Patrick
Lluch, Alberto
Hoffmann, Jörg
Editor(s): del Mar Gallardo, Maria
Merino, Pedro
Language: English
Title: Model Checking Software : 25th International Symposium, SPIN 2018
Startpage: 103
Endpage: 114
Publisher/Platform: Springer International Publishing
Year of Publication: 2018
Place of publication: Cham
Title of the Conference: International Symposium on Model Checking Software
Place of the conference: Malaga, Spain
Publikation type: Conference Paper
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.
URL of the first publication: https://link.springer.com/chapter/10.1007/978-3-319-94111-0_6
Link to this record: hdl:20.500.11880/28411
http://dx.doi.org/10.22028/D291-29300
ISBN: 978-3-319-94111-0
Date of registration: 3-Dec-2019
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Professorship: MI - Prof. Dr. Jörg Hoffmann
Collections:UniBib – Die Universitätsbibliographie

Files for this record:
There are no files associated with this item.


Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.