UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

The Power of the Weak

Carreiro, F; Facchini, A; Venema, Y; Zanasi, F; (2020) The Power of the Weak. ACM Transactions on Computational Logic , 21 (2) , Article 15. Green open access

[img]
Preview
Text
tocl-version.pdf - Accepted version

Download (1MB) | Preview

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).

Type: Article
Title: The Power of the Weak
Open access status: An open access version is available from UCL Discovery
Publisher version: https://doi.org/10.1145/3372392
Language: English
Additional information: This version is the author accepted manuscript. For information on re-use, please refer to the publisher's terms and conditions.
Keywords: Modal μ-calculus, weak monadic second-order logic, tree automata, bisimulation
UCL classification: UCL
UCL > Provost and Vice Provost Offices
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/10094723
Downloads since deposit
9Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item