Three-valued abstractions of games: uncertainty, but with precision
Three-valued abstractions of games: uncertainty, but with precision
复制标题
游戏的三值抽象：不确定性，但精确
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
R. Jagadeesan
中科院分区：
文献类型：
--
作者：
L. D. Alfaro;Patrice Godefroid;R. Jagadeesan
我们提出了一个用于抽象双人回合制游戏的框架，该框架保留了交替/spl mu/-演算（AMC）的任何公式。与传统的只能证明其中一个参与者获胜策略存在的保守抽象不同，我们的框架基于3值博弈，可以用来证明和证伪包含任意嵌套策略量词的AMC公式.我们的主要贡献如下。我们定义了抽象的3值游戏和交替细化关系，这些保留了双方球员的获胜策略。我们提供了一个逻辑表征的交替细化关系。我们表明，我们的抽象是精确的，可以通过完整性的结果。我们提出了AMC公式，解决3值游戏/spl欧米茄/-经常性的目标，我们表明，这样的游戏是确定在一个3值的意义上。我们还讨论了模型检查的复杂性的任意AMC公式的3值游戏和检查交替细化。
We present a framework for abstracting two-player turn-based games that preserves any formula of the alternating /spl mu/-calculus (AMC). Unlike traditional conservative abstractions which can only prove the existence of winning strategies for only one of the players, our framework is based on 3-valued games, and it can be used to prove and disprove formulas of AMC including arbitrarily nested strategy quantifiers. Our main contributions are as follows. We define abstract 3-valued games and an alternating refinement relation on these that preserves winning strategies for both players. We provide a logical characterization of the alternating refinement relation. We show that our abstractions are as precise as can be via completeness results. We present AMC formulas that solve 3-valued games with /spl omega/-regular objectives, and we show that such games are determined in a 3-valued sense. We also discuss the complexity of model checking arbitrary AMC formulas on 3-valued games and of checking alternating refinement.