Stubborn Set Reduction for Two-Player Reachability Games

TL;DR

This paper extends partial order reduction techniques to two-player reachability games, enabling more efficient state space exploration by pruning interleavings, with formal correctness proofs and practical implementation in TAPAAL.

Contribution

It introduces a stubborn set reduction method for two-player games, with formal correctness proofs and an implementation for weighted Petri net games.

Findings

Significant reduction in state space explored in case studies.

Efficient implementation in TAPAAL enhances practical applicability.

Proven correctness for general labelled transition systems.

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