Partial order reduction for reachability games

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

6 Citations (Scopus)
38 Downloads (Pure)

Abstract

Partial order reductions have been successfully applied to model checking of concurrent systems and practical applications of the technique show nontrivial reduction in the size of the explored state space. We present a theory of partial order reduction based on stubborn sets in the game-theoretical setting of 2-player games with reachability/safety objectives. Our stubborn reduction allows us to prune the interleaving behaviour of both players in the game, and we formally prove its correctness on the class of games played on general labelled transition systems. We then instantiate the framework to the class of weighted Petri net games with inhibitor arcs and provide its efficient implementation in the model checker TAPAAL. Finally, we evaluate our stubborn reduction on several case studies and demonstrate its efficiency.

Original languageEnglish
Title of host publication30th International Conference on Concurrency Theory, CONCUR 2019
EditorsWan Fokkink, Rob van Glabbeek
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Publication dateAug 2019
Article number23
ISBN (Electronic)9783959771214
DOIs
Publication statusPublished - Aug 2019
Event30th International Conference on Concurrency Theory, CONCUR 2019 - Amsterdam, Netherlands
Duration: 27 Aug 201930 Aug 2019

Conference

Conference30th International Conference on Concurrency Theory, CONCUR 2019
Country/TerritoryNetherlands
CityAmsterdam
Period27/08/201930/08/2019
SeriesLeibniz International Proceedings in Informatics, LIPIcs
Volume140
ISSN1868-8969

Keywords

  • Games
  • Partial order reduction
  • Petri nets
  • Stubborn sets
  • Synthesis

Fingerprint

Dive into the research topics of 'Partial order reduction for reachability games'. Together they form a unique fingerprint.

Cite this