Decomposition theorems and model-checking for the modal -calculus

DOI10.1145/2603088.2603144zbMATH Open1394.68222OpenAlexW3105868061MaRDI QIDQ4635600FDOQ4635600

Authors Mikołaj Bojańczyk, Christoph Dittmann, Stephan Kreutzer 

Publication date 23 April 2018

Published in Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1405.2234

zbMATH Keywords

model checkingmodal logicmu-calculusfixed-parameter complexityparity gamesdecomposition theorems

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We prove a general decomposition theorem for the modal $mu$-calculus $L_{m}u$ 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_{m}u$ 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_{m}u$ which do not follow from embedding into monadic second-order logic.

Recommendations

• On model checking for the \(\mu\)-calculus and its fragments
• scientific article; zbMATH DE number 2186291
• On modal \(\mu \)-calculus over finite graphs with small components or small tree width
• Fast mu-calculus model checking when tree-width is bounded.
• Some model theory for the modal \(\mu\)-calculus: syntactic characterisations of semantic properties

Cited in

(8)

• Parameterized Algorithms for Parity Games
• Universal guards, relativization of quantifiers, and failure models in model checking modulo theories
• Structural Refinement for the Modal nu-Calculus
• scientific article; zbMATH DE number 7204561 (Why is no real title available?)
• \(\aleph_1\) and the modal \(\mu\)-calculus
• Enriched MU-Calculi Module Checking
• A note on model checking the modal \(\nu\)-calculus
• The mu-calculus and Model Checking

This page was built for publication: Decomposition theorems and model-checking for the modal \(\mu\)-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635600)