倒计时$μ$ -微积分
Countdown $μ$-calculus
摘要：
我们介绍了倒计时$μ$ -演算，扩展的模态$μ$ -演算的顺序近似的不动点算子。除了经典微积分中可定义的性质外，它还可以表达（无）有界性，例如存在任意长的特定动作序列。与奇偶游戏和自动机的标准对应关系扩展到适当定义的倒计时游戏和自动机。然而，与经典的设置，标量片段是可证明的弱于完整的向量演算，并对应于自动机满足一个简单的语法条件。我们建立了一些事实，特别是可判定性的模型检验问题和严格的层次结构所引起的最大允许嵌套我们的新运营商。
英文摘要：
We introduce the countdown $μ$-calculus, an extension of the modal $μ$-calculus with ordinal approximations of fixpoint operators. In addition to properties definable in the classical calculus, it can express (un)boundedness properties such as the existence of arbitrarily long sequences of specific actions. The standard correspondence with parity games and automata extends to suitably defined countdown games and automata. However, unlike in the classical setting, the scalar fragment is provably weaker than the full vectorial calculus and corresponds to automata satisfying a simple syntactic condition. We establish some facts, in particular decidability of the model checking problem and strictness of the hierarchy induced by the maximal allowed nesting of our new operators.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
