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

TL;DR

This paper establishes a decomposition theorem for the modal μ-calculus, enabling fixed-parameter tractable model-checking on structures with bounded Kelly-width or DAG-width, advancing the understanding of efficient verification methods.

Contribution

It introduces a novel decomposition theorem for the modal μ-calculus and demonstrates fixed-parameter tractability for model-checking on specific graph classes, not relying on monadic second-order logic embedding.

Findings

Decomposition theorem for modal μ-calculus based on structure composition

Fixed-parameter tractability of model-checking on Kelly-width and DAG-width bounded structures

First fpt results for μ-calculus not derived from monadic second-order logic

Abstract

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.