论文标题
模态MU-Calculus和一些变体的有界游戏理论语义
Bounded Game-Theoretic Semantics for Modal Mu-Calculus and Some Variants
论文作者
论文摘要
我们为模态MU-Calculus介绍了一种新的游戏理论语义（GTS）。我们所谓的有限GTS用仅出现有限路径的替代评估游戏代替了平等游戏。即使被考虑的过渡系统是无限的，也不需要无限的路径。新型游戏为MU-Calculus框架中的各种结构提供了替代方法。例如，它们已经成功地用作方法的基础，从而为逻辑提供了自然公式大小游戏。尽管我们的主要重点是引入新的GTS，但我们还考虑了一些应用程序来证明其用途。例如，我们考虑一个自然模型转换过程，该过程将模型检查游戏减少到构造模型中的单个固定公式，并且还使用GTS来识别使用PTIME模型检查的MU-Calculus的新替代变体。
We introduce a new game-theoretic semantics (GTS) for the modal mu-calculus. Our so-called bounded GTS replaces parity games with alternative evaluation games where only finite paths arise; infinite paths are not needed even when the considered transition system is infinite. The novel games offer alternative approaches to various constructions in the framework of the mu-calculus. For example, they have already been successfully used as a basis for an approach leading to a natural formula size game for the logic. While our main focus is introducing the new GTS, we also consider some applications to demonstrate its uses. For example, we consider a natural model transformation procedure that reduces model checking games to checking a single, fixed formula in the constructed models, and we also use the GTS to identify new alternative variants of the mu-calculus with PTime model checking.
