Decomposition Theorems and Model-Checking for the Modal $\mu$-calculus

ABSTRACT. The modal $\mu$-calculus, introduced by Dexter Kozen in 1981, is among the best known temporal logics studied in the theory of verification. Despite 30 years of continuous efforts, the exact complexity of its model checking problem remains elusive, and the question whether the problem can be solved in polynomial time is still unsolved.

Most work in the literature uses a game- or automata theoretic approach by reducing the model checking problem to the problem of solving parity games, a two-player game in which the formula and the transition system is combined into a single game arena.

In this paper we take a different route and study the model checking problem directly, keeping the formula and the transition system separate. This allows us to develop logical tools which manipulate the formula only and thereby studying the problem within the framework of parameterized complexity. This approach has been very successful for first- or monadic second-order logic, for instance in the work on algorithmic meta theorems.

As the main logical result of this paper we develop decomposition- or splitter-theorems for the modal $\mu$-calculus in the style of Feferman-Vaught theorems for FO and MSO. In particular, we show that if a transition system $M$ is composed of the union of two systems $M_1 \cup M_2$, then the truth of $L_\mu$-formulas at a node in $M$ essentially only depends on the truth of suitable formulas in the two systems $M_1$ and $M_2$. This result even applies to the much more general case where we allow additional edges in $M$ which start in $M_1$ and end in $M_2$.

As an algorithmic consequence we get that $L_\mu$ model-checking is fixed-parameter tractable on various classes of transition systems such as transition systems of bounded directed path width and bounded Kelly-width. To the best of our knowledge, these are among the first FPT-results for $L_\mu$ that do not follow immediately from tractability of monadic second-order logic.