论文标题
能源MU-Calculus：欧米茄常规能量游戏的符号定点算法
Energy mu-Calculus: Symbolic Fixed-Point Algorithms for omega-Regular Energy Games
论文作者
论文摘要
$ω$ - 局限能量游戏是在验证和综合的背景下使用的，具有定量目标以保持能量水平的定量目标以保持能量水平的定量目标。 Modal $ $ $ -CALCULUS的逻辑，当在具有$ω$的获胜条件的游戏图上应用时，允许以定点公式的形式定义符号算法，以计算获胜状态的集合。 在本文中，我们引入了能源$ $ $ -CALCULUS，这是$μ$ -CALCULUS的多价扩展，它是解决$ω$ groumard Energy Games的象征框架。 Energy $μ$ -CALCULUS可以使现有的，众所周知的象征性$ $ $ $ $ $ $ $ $ $ $ $ - 级游戏的无缝重复使用，以解决其相应的能量增强变体。我们在游戏图的符号表示方面定义了能源$ $ $ calculus的语法和语义，并展示如何使用它来解决决策以及$ω$的能源游戏的最低信用问题，包括有限的能量水平和未结合的能量水平的积累。
$ω$-regular energy games, which are weighted two-player turn-based games with the quantitative objective to keep the energy levels non-negative, have been used in the context of verification and synthesis. The logic of modal $μ$-calculus, when applied over game graphs with $ω$-regular winning conditions, allows defining symbolic algorithms in the form of fixed-point formulas for computing the sets of winning states. In this paper, we introduce energy $μ$-calculus, a multi-valued extension of the $μ$-calculus that serves as a symbolic framework for solving $ω$-regular energy games. Energy $μ$-calculus enables the seamless reuse of existing, well-known symbolic $μ$-calculus algorithms for $ω$-regular games, to solve their corresponding energy augmented variants. We define the syntax and semantics of energy $μ$-calculus over symbolic representations of the game graphs, and show how to use it to solve the decision and the minimum credit problems for $ω$-regular energy games, for both bounded and unbounded energy level accumulations.
