Monadic second order logic and linear temporal logic are two logical formalisms that can be used to describe classes of infinite words, i.e., first-order models based on the natural numbers with order, successor, and finitely many unary predicate symbols. Monadic second order logic over infinite words (S1S) can alternatively be described as a first-order logic interpreted in P(ω), the power set Boolean algebra of the natural numbers, equipped with modal operators for ‘initial’, ʼnext’, and ‘future’ states. We prove that the first-order theory of this structure is the model companion of a class of algebras corresponding to a version of linear temporal logic (LTL) without until. The proof makes crucial use of two classical, nontrivial results from the literature, namely the completeness of LTL with respect to the natural numbers, and the correspondence between S1S-formulas and Büchi automata.
A model-theoretic characterization of monadic second order logic on infinite words / S. Ghilardi, S.J. VAN GOOL. - In: THE JOURNAL OF SYMBOLIC LOGIC. - ISSN 0022-4812. - 82:1(2017), pp. 62-76. [10.1017/jsl.2016.70]
A model-theoretic characterization of monadic second order logic on infinite words
S. GhilardiPrimo
;S.J. VAN GOOLUltimo
2017
Abstract
Monadic second order logic and linear temporal logic are two logical formalisms that can be used to describe classes of infinite words, i.e., first-order models based on the natural numbers with order, successor, and finitely many unary predicate symbols. Monadic second order logic over infinite words (S1S) can alternatively be described as a first-order logic interpreted in P(ω), the power set Boolean algebra of the natural numbers, equipped with modal operators for ‘initial’, ʼnext’, and ‘future’ states. We prove that the first-order theory of this structure is the model companion of a class of algebras corresponding to a version of linear temporal logic (LTL) without until. The proof makes crucial use of two classical, nontrivial results from the literature, namely the completeness of LTL with respect to the natural numbers, and the correspondence between S1S-formulas and Büchi automata.File | Dimensione | Formato | |
---|---|---|---|
ghilardivangool2015-revised.pdf
accesso aperto
Tipologia:
Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione
391.31 kB
Formato
Adobe PDF
|
391.31 kB | Adobe PDF | Visualizza/Apri |
modeltheoretic_characterization_of_monadic_second_order_logic_on_infinite_words.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
217.5 kB
Formato
Adobe PDF
|
217.5 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.