Complete axiomatization of the Stutter-invariant fragment of the linear time $\mu$-calculus

The logic $\mu\mathsf{TL}(\mathsf{U})$ is the fixpoint extension of the “Until”-only fragment of linear-time temporal logic. It also happens to be the stutterinvariant fragment of linear-time $\mu$-calculus $\mu\mathsf{TL}$. We provide complete axiomatizations of $\mu\mathsf{TL}(\mathsf{U})$ on the class of finite words and on the class of $\omega$-words. We introduce for this end another logic, which we call $\mu\mathsf{TL}(\diamondsuit_\Gamma)$, and which is a variation of $\mu\mathsf{TL}$ where the Next time operator is replaced by the family of its stutter-invariant counterparts. This logic has exactly the same expressive power as $\mu\mathsf{TL}(\mathsf{U})$. Using already known results for $\mu\mathsf{TL}$, we first prove completeness for $\mu\mathsf{TL}(\diamondsuit_\Gamma)$, which finally allows us to obtain completeness for $\mu\mathsf{TL}(\mathsf{U})$.