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 μ-calculus. Moreover, we also show that MSO on binary trees is the model companion of binary deterministic fair CTL.
Monadic second order logic as the model companion of temporal logic / S. Ghilardi, S. van Gool (PROCEEDINGS - SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE). - In: Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS 2016)[s.l] : Association for Computing Machinery, 2016 Jul. - ISBN 978-1-4503-4391-6. - pp. 417-426 (( Intervento presentato al 31. convegno Logic in Computer Science tenutosi a New York nel 2016.
|Titolo:||Monadic second order logic as the model companion of temporal logic|
GHILARDI, SILVIO (Primo)
|Parole Chiave:||monadic second order logic; model completeness|
|Settore Scientifico Disciplinare:||Settore MAT/01 - Logica Matematica|
Settore INF/01 - Informatica
|Data di pubblicazione:||lug-2016|
|Digital Object Identifier (DOI):||http://dx.doi.org/10.1145/2933575.2933609|
|Tipologia:||Book Part (author)|
|Appare nelle tipologie:||03 - Contributo in volume|