Highlights Conference 2021 Conference Abstract
Given the status of the modal mu-calculus as a universal specification language, the computational complexity of its model checking and satisfiability problems is of central importance. To determine the complexity of a proposed algorithm for one of these problems, one needs a sensible measure of the size of the formula that is (part of) the input to the algorithm. Different size measures have been used, depending on how precisely such a formula is represented in the input: (1) the length of the formula, corresponding to a representation of the formula as a string or syntax tree; (2) subformula size, corresponding to a representation of the formula as the directed acyclic graph of its subformulas; and (3) closure size, corresponding to a similar representation of a formula via its (Fischer-Ladner) closure. The choice between these representations is non-trivial because the subformula size of a formula may be exponentially smaller than its length, and, as was shown by Bruse, Friedmann & Lange, its closure size may be exponentially smaller than its subformula size. Consequently, complexity results about the mu-calculus may be suboptimal when expressed in terms of subformula size, in the sense that a stronger version of the result holds when formulated in terms of closure size. In other words, it is desirable to design algorithms that operate on a representation of a formula that is based on its closure. In the literature different frameworks have been used to represent mu-calculus formulas; examples include alternating tree automata and hierarchical equation system. In both cases the mathematically fundamental structure underlying the representation is essentially a graph, whose nodes are labelled with logical connectives and priorities. Likewise, the parity games that feature in model checking algorithms generally are based on an arena which is some kind of product of a graph representing the formula and the model where it is evaluated. In all of these settings the graph representing the formula can be based on its syntax tree, its subformula dag or its closure graph. We make this graph structure explicit and call the resulting concept a “parity formula”. One can view these parity formulas as a natural generalisation of mu-calculus formulas themselves, alternating tree automata, hierarchical equation systems; and of the formula component of model checking games. However, parity formulas have a very simple mathematical structure, which allows for a straightforward and unambiguous definition of its size and its index (alternation depth). We provide two new results about the representation of mu-calculus formulas as parity formulas: 1) A common assumption in the literature on the mu-calculus is that one may assume, without loss of generality, that formulas are clean, or well-named, in the sense that bound variables are disjoint from free variables, and each bound variable determines a unique subformula. We show that this assumption may lead to an exponential blow-up in terms of closure-size. This means that, if one is interested in optimal complexity results, it can not be assumed that the input formula is clean. 2) To the best of our knowledge, all representations of mu-calculus formulas known from the literature, are suboptimal in one way or another: they are based on the subformula dag, presuppose this cleanness assumption, or use a priority function yielding an unnecessarily big index. Our main result is a construction that provides, for every mu-calculus formula, an equivalent parity formula that is based on its closure of the given formula and has an index that exactly corresponds to its alternation depth. The proof of this result is non-trivial. (joint work with Clemens Kupke and Johannes Marti)