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.
Monadic second order logic as the model companion of temporal logic
S. GhilardiPrimo
;
2016
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 μ-calculus. Moreover, we also show that MSO on binary trees is the model companion of binary deterministic fair CTL.File | Dimensione | Formato | |
---|---|---|---|
ghilardivangool2016.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
331.02 kB
Formato
Adobe PDF
|
331.02 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.