一句话：将 Shapley 值引入模型检测，度量系统组件对满足时序规约的重要性，并给出线性与分支时序逻辑下的复杂度上下界。
本文关注如何度量系统某一部分的非确定性选择对其满足给定规约的能力的影响。为此，作者将 Shapley 值的思想应用于验证：把某个组件的控制权单独或与其他组件一起交给对手，再检验系统是否仍能满足规约，从而定义该组件的重要性。论文在模型检测框架下研究这一概念，覆盖多种经典线性时序规约，并提出若干将其推广到分支时序规约的方式。针对这些定义，作者在几乎所有情形下给出了紧的复杂度界，刻画了计算组件重要性值的理论代价。
We aim at measuring the influence of the nondeterministic choices of a part of a system on its ability to satisfy a specification. For this purpose, we apply the concept of Shapley values to verification as a means to evaluate how important a part of a system is. The importance of a component is measured by giving its control to an adversary, alone or along with other components, and testing whether the system can still fulfill the specification. We study this idea in the framework of model-checking with various classical types of linear-time specification, and propose several ways to transpose it to branching ones. We also provide tight complexity bounds in almost every case.
@inproceedings{paperbot6182,
title = {Responsibility and verification: Importance value in temporal logics},
author = {Corto Mascle and Christel Baier and Florian Funke and Simon Jantsch and Stefan Kiefer},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470597}
}