The power of the weak

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 μN ML of μML on the modal side and one forWMSO, 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 andWalukiewicz did, the standard modal μ-calculus, interpreted over arbitrary LTSs. The first theorem that we prove is that, over LTSs, μN ML 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 fromWMSO and proves it equivalent modulo bisimilarity to a fragment of μN ML defined by a notion of continuity. Analogously to Janin andWalukiewicz'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 μN ML (for all transition systems).