Algorithms for solving computational problems related to the modal mu-calculus generally do not take the formulas themselves as input, but operate on some kind of representation of formulas. This representation is usually based on a graph structure that one may associate with a mu-calculus formula. Recent work by Kupke, Marti and Venema showed that the operation of renaming bound variables may incur an exponential blow-up of the size of such a graph representation. Their example revealed the undesirable situation that standard constructions, on which algorithms for model checking and satisfiability depend, are sensitive to the specific choice of bound variables used in a formula.

Our work discusses how the notion of alphabetic equivalence interacts with the construction of graph representations of mu-calculus formulas, and with the induced size measures of formulas. We introduce the condition of alpha-invariance on such constructions, requiring that alphabetically equivalent formulas are given the same (or isomorphic) graph representations.

Our main results are the following. First we show that if two mu-calculus formulas are alpha-equivalent, then their respective Fischer-Ladner closures have the same cardinality, up to alpha-equivalence. We then continue with the definition of an alpha-invariant construction which represents an arbitrary mu-calculus formula by a graph that has exactly the size of the quotient of the closure of the formula, up to alpha-equivalence. This definition, which is itself based on a renaming of variables, solves the above-mentioned problem discovered by Kupke et al.