摘要：Partial order reductions have been successfully applied to model checking ofconcurrent systems and practical applications of the technique show nontrivialreduction in the size of the explored state space. We present a theory ofpartial order reduction based on stubborn sets in the game-theoretical settingof 2-player games with reachability objectives. Our stubborn reduction allowsus to prune the interleaving behaviour of both players in the game, and weformally prove its correctness on the class of games played on general labelledtransition systems. We then instantiate the framework to the class of weightedPetri net games with inhibitor arcs and provide its efficient implementation inthe model checker TAPAAL. Finally, we evaluate our stubborn reduction onseveral case studies and demonstrate its efficiency.
