Paper Info
Title
The Power of the Weak
Abstract
A landmark result in the study of logics for formal verification is Janin and Walukiewicz’s theorem, stating that the modal μ-calculus (μML) is equivalent modulo bisimilarity to standard monadic second-order logic (here abbreviated as SMSO) over the class of labelled transition systems (LTSs for short). Our work proves two results of the same kind, one for the alternation-free or noetherian fragment μNML of μML on the modal side and one for WMSO, weak monadic second-order logic, on the second-order side. In the setting of binary trees, with explicit functions accessing the left and right successor of a node, it was known that WMSO is equivalent to the appropriate version of alternation-free μ-calculus. Our analysis shows that the picture changes radically once we consider, as Janin and Walukiewicz did, the standard modal μ-calculus, interpreted over arbitrary LTSs. The first theorem that we prove is that, over LTSs, μNML is equivalent modulo bisimilarity to noetherian MSO (NMSO), a newly introduced variant of SMSO where second-order quantification ranges over “conversely well-founded” subsets only. Our second theorem starts from WMSO and proves it equivalent modulo bisimilarity to a fragment of μNML defined by a notion of continuity. Analogously to Janin and Walukiewicz’s result, our proofs are automata-theoretic in nature: As another contribution, we introduce classes of parity automata characterising the expressiveness of WMSO and NMSO (on tree models) and of μCML and μNML (for all transition systems).
Year
DOI
Venue
2020
10.1145/3372392
ACM Transactions on Computational Logic (TOCL)
Keywords
DocType
Volume
Modal -calculus,bisimulation,tree automata,weak monadic second-order logic
Journal
21
Issue
ISSN
Citations 
2
1529-3785
0
PageRank 
References 
Authors
0.34
0
4
Name
Order
Citations
PageRank
Facundo Carreiro1124.09
Alessandro Facchini2359.47
Yde Venema360965.12
Fabio Zanasi411013.89