Decomposition Theorems and Model-Checking for the Modal μ-Calculus

We prove a general decomposition theorem for the modal mu-calculus L-mu in the spirit of Feferman and Vaught's theorem for disjoint unions. In particular, we show that if a structure (i.e., transition system) is composed of two substructures M-1 and M-2 plus edges from M-1 to M-2, then the formulas true at a node in M only depend on the formulas true in the respective substructures in a sense made precise below. As a consequence we show that the model-checking problem for L-mu is fixed-parameter tractable (fpt) on classes of structures of bounded Kelly-width or bounded DAG-width. As far as we are aware, these are the first fpt results for L-mu which do not follow from embedding into monadic second-order logic.