Model Checking ω -Regular Properties with Decoupled Search

Daniel Gnad*, Jan Eisenhut, Alberto Lluch Lafuente, Jörg Hoffmann

*Corresponding author for this work

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

Abstract

Decoupled search is a state space search method originally introduced in AI Planning. Similar to partial-order reduction methods, decoupled search exploits the independence of components to tackle the state explosion problem. Similar to symbolic representations, it does not construct the explicit state space, but sets of states are represented in a compact manner, exploiting component independence. Given the success of both partial-order reduction and symbolic representations when model checking liveness properties, our goal is to add decoupled search to the toolset of liveness checking methods. Specifically, we show how decoupled search can be applied to liveness verification for composed Büchi automata by adapting, and showing correct, a standard algorithm for detecting lassos (i.e., infinite accepting runs), namely nested depth-first search. We evaluate our approach using a prototype implementation.

Original languageEnglish
Title of host publicationComputer Aided Verification
EditorsAlexandra Silva, K. Rustan Leino
PublisherSpringer
Publication date2021
Pages411-434
ISBN (Print)9783030816872
DOIs
Publication statusPublished - 2021
Event33rd International Conference on Computer-Aided Verification - Online event, Los Angeles, United States
Duration: 18 Jul 202124 Jul 2021
Conference number: 33

Conference

Conference33rd International Conference on Computer-Aided Verification
Number33
LocationOnline event
Country/TerritoryUnited States
CityLos Angeles
Period18/07/202124/07/2021
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12760 LNCS
ISSN0302-9743

Bibliographical note

Funding Information:
Acknowledgment. We thank Álvaro Torralba for helpful discussions about the state-splitting approach. Daniel Gnad was supported by the German Research Foundation (DFG), as part of project grant HO 2169/6-2, “Star-Topology Decoupled State Space Search”. Jörg Hoffmann’s research group has received support by DFG grant 389792660 as part of TRR 248 (see perspicuous-computing.science).

Publisher Copyright:
© 2021, The Author(s).

Fingerprint

Dive into the research topics of 'Model Checking ω -Regular Properties with Decoupled Search'. Together they form a unique fingerprint.

Cite this