Fixpoint Approximation of Strategic Abilities under Imperfect Information
Fixpoint Approximation of Strategic Abilities under Imperfect Information
复制标题
不完全信息下战略能力的不动点逼近
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Damian Kurpiewski
中科院分区：
文献类型：
--
作者：
W. Jamroga;M. Knapik;Damian Kurpiewski
众所周知，在不完全信息下对战略能力进行模型检查是很困难的。复杂性结果的范围从 NP 完整性到不可判定性，具体取决于问题的精确设置。同样重要的是，不动点等价通常不适用于不完美的信息策略，这严重阻碍了获胜策略的增量综合。在本文中，我们提出了 ATLir 公式的翻译，为其真值提供了下限和上限，并且验证成本比原始规范更便宜。也就是说，如果表达式被验证为真，那么 ATLir 的相应公式也应该在给定模型中成立。我们首先展示直接方法在哪些地方不起作用。然后，我们提出如何修改它以获得有保证的下限。为此，我们改变下一步运算符，使得遍历不可区分关系被视为原子活动。最有趣的是，较低的近似值是由使用下一步能力运算符的非标准变体的定点表达式提供的。我们展示了翻译的正确性，确定了其计算复杂性，并通过桥牌游戏的可扩展场景进行实验来验证该方法。
Model checking of strategic ability under imperfect information is known to be hard. The complexity results range from NP-completeness to undecidability, depending on the precise setup of the problem. No less importantly, fixpoint equivalences do not generally hold for imperfect information strategies, which seriously hampers incremental synthesis of winning strategies. In this paper, we propose translations of ATLir formulae that provide lower and upper bounds for their truth values, and are cheaper to verify than the original specifications. That is, if the expression is verified as true then the corresponding formula of ATLir should also hold in the given model. We begin by showing where the straightforward approach does not work. Then, we propose how it can be modified to obtain guaranteed lower bounds. To this end, we alter the next-step operator in such a way that traversing one's indistinguishability relation is seen as atomic activity. Most interestingly, the lower approximation is provided by a fixpoint expression that uses a nonstandard variant of the next-step ability operator. We show the correctness of the translations, establish their computational complexity, and validate the approach by experiments with a scalable scenario of Bridge play.
DOI：
10.1016/j.ic.2015.03.014
发表时间：
2015-06
期刊：
Inf. Comput.
影响因子：
--
作者：
Simon Busard;C. Pecheur;Hongyang Qu;F. Raimondi
通讯作者：
Simon Busard;C. Pecheur;Hongyang Qu;F. Raimondi
DOI：
10.1007/s10009-015-0378-x
发表时间：
2017-02-01
影响因子：
1.5
作者：
Lomuscio, Alessio;Qu, Hongyang;Raimondi, Franco
通讯作者：
Raimondi, Franco