Abstraction Refinement for Games with Incomplete Information
Abstraction Refinement for Games with Incomplete Information
复制标题
不完整信息博弈的抽象细化
DOI：
10.4230/lipics.fsttcs.2008.1751
复制
发表时间：
2008
影响因子：
5.2
通讯作者：
B. Finkbeiner
中科院分区：
文献类型：
--
作者：
Rayna Dimitrova;B. Finkbeiner
反例引导的抽象精致（CEGAR）用于
自动化软件分析以找到合适的有限国家抽象
无限国家系统。在本文中，我们将Cegar扩展到游戏
有了不完整的信息，因为它们通常在控制器中发生
合成和模块化验证。挑战是，在
不完整的信息，必须仔细说明知识
玩家可用：策略不得依赖信息
玩家看不到。我们提出了一个游戏的抽象机制
不完整的信息包含玩家的近似\'移动
进入抽象状态的基于知识的子集结构
空间。这种抽象会导致一个完美的信息游戏
有限图。抽象策略的具体性可以编码为
战略 - 树公式的满意度。基于此编码
我们提出了一种基于插值的方法，用于选择新的谓词
并提供足够的条件来终止结果
改进循环。
Counterexample-guided abstraction refinement (CEGAR) is used in
automated software analysis to find suitable finite-state abstractions
of infinite-state systems. In this paper, we extend CEGAR to games
with incomplete information, as they commonly occur in controller
synthesis and modular verification. The challenge is that, under
incomplete information, one must carefully account for the knowledge
available to the player: the strategy must not depend on information
the player cannot see. We propose an abstraction mechanism for games under
incomplete information that incorporates the approximation of the players\' moves
into a knowledge-based subset construction on the abstract state
space. This abstraction results in a perfect-information game over a
finite graph. The concretizability of abstract strategies can be encoded as
the satisfiability of strategy-tree formulas. Based on this encoding,
we present an interpolation-based approach for selecting new predicates
and provide sufficient conditions for the termination of the resulting
refinement loop.