能量 μ-演算：ω-正则能量博弈的符号不动点算法

$\omega$-正则能量博弈是带权两名玩家轮流博弈，其量化目标为保持能量水平非负，已被用于验证与综合。模态 $\mu$-演算逻辑在带有 $\omega$-正则获胜条件的博弈图上应用时，允许以不动点公式的形式定义符号算法来计算获胜状态集合。本文引入能量 $\mu$-演算，它是 $\mu$-演算的多值扩展，作为求解 $\omega$-正则能量博弈的符号框架。能量 $\mu$-演算使得现有的、众所周知的用于 $\omega$-正则博弈的符号 $\mu$-演算算法能够被无缝复用来求解其对应的能量增强变体。我们定义了能量 $\mu$-演算在博弈图符号表示上的语法与语义，并展示如何用它求解 $\omega$-正则能量博弈在能量水平有界与无界累积下的判定问题与最小信用问题。