  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.
