一句话：提出双人可达性博弈的顽固集偏序约简理论，正确剪枝双方交错，并在TAPAAL中实现加权Petri网博弈约简。
偏序约简已成功用于并发系统模型检测，但此前缺乏在双人博弈中的通用理论。本文在双人可达性博弈的博弈论框架下提出基于顽固集的偏序约简，允许同时剪枝双方玩家的交错行为，并在一般标记迁移系统上的博弈中形式证明其正确性。作者进一步将框架实例化到带抑制弧的加权Petri网博弈，在模型检测器TAPAAL中给出高效实现，并在多个案例研究中评估。结果表明该约简能显著缩小需探索的状态空间，验证了其实用效率。
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.
@article{paperbot1329,
title = {Stubborn Set Reduction for Two-Player Reachability Games},
author = {Frederik Meyer Bønneland and Peter Gjøl Jensen and Kim Guldstrand Larsen and Marco Muñiz and Jiří Srba},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 1},
year = {2021},
doi = {10.23638/lmcs-17(1:21)2021}
}