Monadic second order logic as the model companion of temporal logic

DOI10.1145/2933575.2933609MaRDI QIDQ4635899zbMATH OpenOpenAlexWikidataFDO

Authors Silvio Ghilardi, Samuel J. van Gool

Publication date 23 April 2018

Published in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

monadic second-order logictree automatatemporal logicmodel companions

Mathematics Subject Classification ID

Other model constructions (03C30) Automata and formal grammars in connection with logical questions (03D05) Temporal logic (03B44)

Abstract: The main focus of this paper is on bisimulation-invariant MSO, and more particularly on giving a novel model-theoretic approach to it. In model theory, a model companion of a theory is a first-order description of the class of models in which all potentially solvable systems of equations and non-equations have solutions. We show that bisimulation-invariant MSO on trees gives the model companion for a new temporal logic, "fair CTL", an enrichment of CTL with local fairness constraints. To achieve this, we give a completeness proof for the logic fair CTL which combines tableaux and Stone duality, and a fair CTL encoding of the automata for the modal {mu}-calculus. Moreover, we also show that MSO on binary trees is the model companion of binary deterministic fair CTL.

Recommendations

• A model-theoretic characterization of monadic second order logic on infinite words
• scientific article; zbMATH DE number 4027441
• Bisimulation Invariant Monadic-Second Order Logic in the Finite
• Counting on CTL^*: On the expressive power of monadic path logic
• Expressive Power of Monadic Second-Order Logic and Modal μ-Calculus

Cited in

(6)

• SMT-based verification of data-aware processes: a model-theoretic approach
• A Cook's tour of duality in logic: from quantifiers, through Vietoris, to measures
• Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
• Model completeness, covers and superposition
• Existentially closed Brouwerian semilattices
• A model-theoretic characterization of monadic second order logic on infinite words

This page was built for publication: Monadic second order logic as the model companion of temporal logic

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