Solving games via three-valued abstraction refinement
Solving games via three-valued abstraction refinement
复制标题
通过三值抽象细化解决博弈
DOI：
10.1016/j.ic.2009.05.007
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Pritam Roy
中科院分区：
文献类型：
--
作者：
L. D. Alfaro;Pritam Roy
模拟现实系统的游戏可能具有非常大的状态空间，这使得它们的直接解决方案变得困难。我们提出了一种符号抽象细化方法来解决具有可达性或安全目标的两人游戏。给定可达性或安全性属性、初始状态集和游戏表示，我们的方法首先构建游戏的简单抽象，并以属性和初始集中存在的谓词为指导。然后对抽象进行细化，直到可以证明或反驳初始状态的性质。具体来说，我们以三值方式评估抽象游戏的属性，计算满足该属性的状态的过近似（可能状态）和欠近似（必须状态）。如果此计算未能对初始状态上的属性有效性产生特定的是/否答案，我们的算法通过分割不确定的抽象状态（可能状态但不是必须状态的状态）来细化抽象。该方法有助于有效的符号实现。我们讨论抽象方案所需的属性，以实现我们的技术的收敛和终止。
Games that model realistic systems can have very large state-spaces, making their direct solution difficult. We present a symbolic abstraction-refinement approach to the solution of two-player games with reachability or safety goals. Given a reachability or safety property, an initial set of states, and a game representation, our approach starts by constructing a simple abstraction of the game, guided by the predicates present in the property and in the initial set. The abstraction is then refined, until it is possible to either prove, or disprove, the property over the initial states. Specifically, we evaluate the property on the abstract game in three-valued fashion, computing an over-approximation (the may states), and an under-approximation (the must states), of the states that satisfy the property. If this computation fails to yield a certain yes/no answer to the validity of the property on the initial states, our algorithm refines the abstraction by splitting uncertain abstract states (states that are may-states, but not must-states). The approach lends itself to an efficient symbolic implementation. We discuss the property required of the abstraction scheme in order to achieve convergence and termination of our technique.