Carreiro, Facundo and Facchini, Alessandro and Venema, Yde and Zanasi, Fabio (2020) The power of the weak. ACM Transactions on Computational Logic (TOCL), 21 (2). pp. 1-47.
Full text not available from this repository.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).
| Item Type: | Scientific journal article, Newspaper article or Magazine article |
|---|---|
| Subjects: | Computer sciences > Computer science > Computational science foundations |
| Department/unit: | Dipartimento tecnologie innovative > Istituto Dalle Molle di studi sull’intelligenza artificiale USI-SUPSI |
| Depositing User: | Alessandro Facchini |
| Date Deposited: | 24 Aug 2023 13:27 |
| Last Modified: | 24 Aug 2023 13:30 |
| URI: | http://repository.supsi.ch/id/eprint/14560 |
Actions (login required)
 |
View Item |