双主体零和博弈逻辑形式系统建构及模型检测研究

博弈逻辑是博弈论和逻辑学相交叉的一个崭新研究领域,属应用逻辑范畴。双主体零和博弈逻辑是目前国际上博弈逻辑研究的重心。在命题动态逻辑原有程序算子(;∪*)的基础上增加对偶(dual)算子d建构双主体零和博弈逻辑的形式系统;把双主体零和博弈逻辑嵌入μ-演算中,分析双主体零和博弈逻辑的语言表达力;并在对双主体零和博弈逻辑形式系统建构的基础上,研究其模型检测的复杂性,可以为双主体非零和博弈逻辑及多主体博弈逻辑的研究奠定基础。双主体零和博弈逻辑已成为拓展博弈逻辑研究的一个重要方向。

Research on Two-agent Zero-sum Game Logic Formal System and Model checking

Game logic is a new field of research on the intersection between game theory and logic.Its international research focuses on two-agent zero-sum game logic.This paper studies syntax,semantics and axiomatization on two-agent zero-sum game logic.The paper also explores how to embed the game logic into the μ-calculus.The author demonstrates complexity of model checking on two-agent zero-sum game logic.