Model Checking and Artificial Intelligence
Model Checking and Artificial Intelligence
复制标题
模型检查和人工智能
DOI：
10.1007/978-3-642-00431-5_11
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Troquard N
中科院分区：
文献类型：
--
作者：
Troquard N
解决方案概念是分析类游戏系统的基本工具，因此，人们在使用逻辑来表征解决方案概念的问题上投入了大量精力。然而，一个问题是，为了描述诸如纳什均衡之类的解决方案概念，似乎有必要参考对象语言中的策略，这往往会使对象语言变得复杂。我们提出了一种逻辑，我们可以在其中制定游戏的重要属性（特别是纯策略解决方案概念），而无需借助对象语言中的命名策略。这个想法是，我们不使用声明特定策略集合形成解决方案的谓词，而是定义当且仅当该状态构成特定均衡结果时该状态为真的逻辑公式。我们通过模型检查策略博弈的均衡来演示逻辑。
Solutions concepts are a fundamental tool for the analysis of game-like systems, and as a consequence, much effort has been devoted to the problem of characterising solution concepts using logic. However, one problem is that, to characterise solution concepts such as Nash equilibrium, it seems necessary to refer to strategies in the object language, which tends to complicate the object language. We propose a logic in which we can formulate important properties of games (and in particular pure-strategy solution concepts) without recourse to naming strategies in the object language. The idea is that instead of using predicates which state that a particular collection of strategies forms a solution, we define formulae of the logic that are true at a state if and only if this state constitutes a particular equilibrium outcome. We demonstrate the logic by model checking equilibria of strategic games.