The Power of the Weak

DOI10.1145/3372392MaRDI QIDQ5121266zbMATH OpenOpenAlexWikidataFDO

Authors Facundo Carreiro, Alessandro Facchini, Fabio Zanasi, Yde Venema

Publication date 11 September 2020

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

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

zbMATH Keywords

bisimulationmodal \(\mu\)-calculustree automataweak monadic second-order logic

Mathematics Subject Classification ID

Higher-order logic (03B16) Modal logic (including the logic of norms) (03B45) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: A landmark result in the study of logics for formal verification is Janin & Walukiewicz's theorem, stating that the modal $mu$-calculus ($mumathrmML$) is equivalent modulo bisimilarity to standard monadic second-order logic (here abbreviated as $mathrmsmso$), over the class of labelled transition systems (LTSs for short). Our work proves two results of the same kind, one for the alternation-free fragment of $mumathrmML$ ($m{u}_{D}mathrmML$) and one for weak $mathrmmso$ ($mathrmwmso$). Whereas it was known that $m{u}_{D}mathrmML$ and $mathrmwmso$ are equivalent modulo bisimilarity on binary trees, our analysis shows that the picture radically changes once we reason over arbitrary LTSs. The first theorem that we prove is that, over LTSs, $m{u}_{D}mathrmML$ is equivalent modulo bisimilarity to noetherian $mathrmmso$ ($mathrmnmso$), a newly introduced variant of $mathrmsmso$ where second-order quantification ranges over "well-founded" subsets only. Our second theorem starts from $mathrmwmso$, and proves it equivalent modulo bisimilarity to a fragment of $m{u}_{D}mathrmML$ defined by a notion of continuity. Analogously to Janin & Walukiewicz's result, our proofs are automata-theoretic in nature: as another contribution, we introduce classes of parity automata characterising the expressiveness of $mathrmwmso$ and $mathrmnmso$ (on tree models) and of $m{u}_{C}mathrmML$ and $m{u}_{D}mathrmML$ (for all transition systems).

Recommendations

• Powerless in face of the powers
• The Powers That Be
• The Power of the Half Power
• The power of unentanglement
• The full power of the half-power
• The strength of weak proximity
• The power of chaos
• The curse of wealth and power

Cited in

(14)

• A focus system for the alternation-free \(\mu \)-calculus
• Model theory of monadic predicate logic with the infinity quantifier
• Relating paths in transition systems: the fall of the modal mu-calculus
• scientific article; zbMATH DE number 1304332 (Why is no real title available?)
• Expressive Power of Monadic Second-Order Logic and Modal μ-Calculus
• Weak MSO: automata and expressiveness modulo bisimilarity
• Relating paths in transition systems: the fall of the modal mu-calculus
• scientific article; zbMATH DE number 7533315 (Why is no real title available?)
• Sharp congruences adequate with temporal logics combining weak and strong modalities
• scientific article; zbMATH DE number 7172369 (Why is no real title available?)
• A characterization theorem for the alternation-free fragment of the modal -calculus
• Automata-theoretic characterisations of branching-time temporal logics
• A characterisation theorem for two-way bisimulation-invariant monadic least fixpoint logic over finite structures
• Modal automata: analysing modal fixpoint logics, one step at a time (invited talk)

This page was built for publication: The Power of the Weak

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