Decomposition theorems and model-checking for the modal -calculus

DOI10.1145/2603088.2603144zbMATH Open1394.68222arXiv1405.2234OpenAlexW3105868061MaRDI 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)

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.

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

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

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)

Cited In (8)

• Universal guards, relativization of quantifiers, and failure models in model checking modulo theories
• \(\aleph_1\) and the modal \(\mu\)-calculus
• Enriched MU-Calculi Module Checking
• A note on model checking the modal \(\nu\)-calculus
• Title not available (Why is that?)
• The mu-calculus and Model Checking
• Parameterized Algorithms for Parity Games
• Structural Refinement for the Modal nu-Calculus

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)