Frederik Meyer Bønneland ; Peter Gjøl Jensen ; Kim Guldstrand Larsen ; Marco Muñiz ; Jiří Srba - Stubborn Set Reduction for Two-Player Reachability Games

lmcs:5997 - Logical Methods in Computer Science, March 18, 2021, Volume 17, Issue 1 - https://doi.org/10.23638/LMCS-17(1:21)2021
Stubborn Set Reduction for Two-Player Reachability Games

Authors: Frederik Meyer Bønneland ; Peter Gjøl Jensen ; Kim Guldstrand Larsen ; Marco Muñiz ; Jiří Srba

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 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.


Volume: Volume 17, Issue 1
Published on: March 18, 2021
Accepted on: October 16, 2020
Submitted on: December 23, 2019
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 107 times.
This article's PDF has been downloaded 89 times.