A model-theoretic characterization of monadic second order logic on infinite words

Journal of Symbolic Logic 82 (1):62-76 (2017)
  Copy   BIBTEX

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 can alternatively be described as a first-order logic interpreted in${\cal P}\left$, 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 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.

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 103,401

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2017-03-26

Downloads
27 (#864,536)

6 months
2 (#1,294,541)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Varieties of complex algebras.Robert Goldblatt - 1989 - Annals of Pure and Applied Logic 44 (3):173-242.

Add more references