能量μ演算：ω-正则能量博弈的符号不动点算法
Energy mu-Calculus: Symbolic Fixed-Point Algorithms for omega-Regular Energy Games
摘要：
$ω$-常规能量游戏，这是加权的两个玩家回合制游戏的定量目标，以保持能量水平非负，已被用于验证和合成的上下文中。模态$μ$-演算的逻辑，当应用于具有$ω$-正则获胜条件的博弈图时，允许以定点公式的形式定义用于计算获胜状态集的符号算法。在本文中，我们介绍了能量$μ$-演算，多值扩展的$μ$-演算，作为一个符号框架解决$ω$-经常能源游戏。能量$μ$-演算使现有的，众所周知的符号$μ$-演算算法的无缝重用$ω$-常规游戏，以解决其相应的能量增强的变种。我们定义的语法和语义的能量$μ$-演算的符号表示的游戏图，并展示了如何使用它来解决决策和最小信用问题的$ω$-定期能源游戏，有界和无界的能量水平的积累。
英文摘要：
$ω$-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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
