关于模态$\mu$-演算中的守卫变换

守卫范式要求 $\mu$-演算公式中不动点变量的出现位于模态算子的辖域内。文献中包含能有效将 $\mu$-演算公式转化为守卫范式的守卫变换。我们表明，已知的守卫变换会导致公式规模呈指数级膨胀，这与现有关于多项式行为的声称相反。我们还表明，对于更宽松的向量形式的 $\mu$-演算公式，任何多项式时间的守卫变换都将产生一个针对奇偶博弈的多项式时间求解算法，而该算法的存在性是一个开放问题。我们还研究了 $\mu$-演算、向量形式与分层方程系统之间的变换，后者是交替奇偶树自动机的一种替代语法。