Countdown $\mu$-calculus

TL;DR

The paper introduces the countdown μ-calculus, extending modal μ-calculus with ordinal approximations, enabling the expression of unbounded properties, and explores its theoretical properties, decidability, and hierarchy structure.

Contribution

It presents the countdown μ-calculus, a novel extension with ordinal fixpoint approximations, and analyzes its expressiveness, automata correspondence, and decidability results.

Findings

Decidability of the model checking problem.

The scalar fragment is weaker than the full calculus.

Hierarchy based on nesting depth is strict.

Abstract

We introduce the countdown $\mu$-calculus, an extension of the modal $\mu$-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.