Size matters in the modal $\mu$-calculus

TL;DR

This paper compares size measures for the modal μ-calculus, analyzing how different representations and alpha-equivalence impact formula complexity and automata-based transformations.

Contribution

It introduces size notions invariant under alpha-equivalence and compares subformula and closure sizes, highlighting their exponential differences and implications for complexity.

Findings

Closure-size can be exponentially smaller than subformula-size.

Transformations to parity formulas are linear in closure-size.

Alpha-equivalence impacts formula size and complexity measures.

Abstract

We discuss and compare complexity measures for the modal $\mu$-calculus, focusing on size and alternation depth. As a yardstick we take Wilke's alternating tree automata, which we shall call parity formulas in the text. Building on work by Bruse, Friedmann & Lange, we compare two size measures for $\mu$-calculus formulas: subformula-size,i.e. , the number of subformulas of the given formula, and closure-size. These notions correspond to the representation of a formula as a parity formula based on, respectively, its subformula dag, and its closure graph. What distinguishes our approach is that we are explicit about the role of alpha-equivalence, as naively renaming bound variables can lead to an exponential blow-up. In addition, we match the formula's alternation depth with the index of the parity formula. We start in a setting without alpha-equivalence. We define subformula-size and closure-size and recall that a $\mu$-calculus formula can be transformed into a parity formula of size linear wrt subformula size, and give a construction that transforms a $\mu$-calculus formula into an equivalent parity formula linear wrt closure-size. Conversely, there is a standard transformation producing a $\mu$-calculus formula of exponential subformula -- but linear closure-size in terms of the size of the original parity formula. We identify so-called untwisted parity formulas for which a transformation linear in subformula-size exists. We then introduce size notions that are completely invariant under alpha equivalence. We transfer the result of Bruse et alii, showing that also in our setting closure-size can be exponentially smaller than subformula-size. We also show how to rename bound variables so that alpha-equivalence becomes syntactic identity on the closure set. Finally, we review the complexity of guarded transformations.