S.J. van Gool
- A model-theoretic characterization of monadic second-order logic on infinite words
- Journal of Symbolic Logic
- Volume | Issue number
- 82 | 1
- Pages (from-to)
- Number of pages
- Document type
- Interfacultary Research Institutes
- Institute for Logic, Language and Computation (ILLC)
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, non-trivial 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.
- go to publisher's site
- Accepted author manuscript
- © The Association for Symbolic Logic 2017
If you believe that digital publication of certain material infringes any of your rights or (privacy) interests, please let the Library know, stating your reasons. In case of a legitimate complaint, the Library will make the material inaccessible and/or remove it from the website. Please Ask the Library, or send a letter to: Library of the University of Amsterdam, Secretariat, Singel 425, 1012 WP Amsterdam, The Netherlands. You will be contacted as soon as possible.