A Survey on Satisfiability Checking for the $\mu$-Calculus through Tree Automata

TL;DR

This survey reviews methods for satisfiability checking of the modal μ-calculus via tree automata, focusing on non-emptiness algorithms and their complexity, with implications for model checking and logic fragments.

Contribution

It provides a comprehensive overview of non-emptiness checking of alternating tree automata for μ-calculus satisfiability, including structural and determinization techniques.

Findings

Non-emptiness checking reduces to parity game solving.

Construction of emptiness games combines structural and determinization methods.

Complexity is exponential in automaton size, with special cases allowing simpler approaches.

Abstract

Algorithms for model checking and satisfiability of the modal $\mu$-calculus start by converting formulas to alternating parity tree automata. Thus, model checking is reduced to checking acceptance by tree automata and satisfiability to checking their emptiness. The first reduces directly to the solution of parity games but the second is more complicated. We review the non-emptiness checking of alternating tree automata by a reduction to solving parity games of a certain structure, so-called emptiness games. Since the emptiness problem for alternating tree automata is EXPTIME-complete, the size of these games is exponential in the number of states of the input automaton. We show how the construction of the emptiness games combines a (fixed) structural part with (history-)determinization of parity word automata. For tree automata with certain syntactic structures, simpler methods may be used to handle the treatment of the word automata, which then may be asymptotically smaller than in the general case. These results have direct consequences in satisfiability and validity checking for (various fragments of) the modal $\mu$-calculus.