Existential Second-Order Logic Over Strings
- Thomas Eiter ,
- Georg Gottlob ,
- Yuri Gurevich
Journal of the ACM, | , Vol 47(1): pp. 77-131
We study existential second-order logic over finite strings. For every prefix class C, we determine the complexity of the model checking problem restricted to C. In particular, we prove that, in the case of the Ackermann class, for every formula φ, there is a finite automaton A that solves the model checking problem for φ.
Permission to make digital / hard copy of part or all of this work for personal or classroom use is granted without fee provided that the copies are not made or distributed for profit or commercial advantage, the copyright notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery (ACM), Inc. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and /or a fee. © 2000 ACM 0004-5411/00/0100-0077.