Thomas Eiter
Yuri Gurevich
Abstract
Existential second-order logic (ESO) and monadic second-order logic(MSO) have attracted much interest in logic and computer science. ESO is a much expressive logic over successor structures than MSO. However, little was known about the relationship between MSOand syntatic fragments of ESO. We shed light on this issue by completely characterizing this relationship for the prefix classes of ESO over strings, (i.e., finite successor structures). Moreover, we determine the complexity of model checking over strings, for all ESO-prefix classes. Let ESO( Q ) denote the prefix class containing all sentences of the shape ∃RQ4 , where R is a list of predicate variables, Q is a first-order predicate qualifier from the prefix set Q and 4 is quantifier-free. We show that ESO( ∃*∀∃∃∃*) and ESO( ∃*∀∀ ) are the maximal standard ESO-prefix classes contained in MSO, thus expressing only regular languages. We further prove the following dichotomy theorem: An ESO prefix-class either expresses only regular languages (and is thus in MSO), or it expresses some NP-complete languages. We also give a precise characterization of those ESO-prefix classes that are equivalent to MSO over strings, and of the ESO-prefix classes which are closed under complementation on strings.
- ABITEBOUL, S., HULL, R., AND VIANU, V. 1995. Foundations of Databases. Addison-Wesley, Reading, Mass. Google Scholar
- AJTAI, M. 1983. ~1 Formulae on Finite Structures. Ann. Pure Appl. Logic 24, 1-48.Google Scholar
- BASIN, D., AND KLARLUND, N. 1995. Hardware verification using monadic second-order logic. In Proceedings of the 7th International Conference on Computer Aided Verification (CAV'95). Lecture Notes in Computer Science, vol. 939. Springer-Verlag, New York, pp. 31-41. Google Scholar
- BERGER, R. 1966. The undecidability of the domino problem. Mem. AMS 66.Google Scholar
- BERSTEL, J. 1979. Transductions and Context-Free Languages. Teubner, Stuttgart. BC)RGER, E., GRADEL, E., AND GUREVICH, Y. 1997. The Classical Decision Problem. Springer, Berlin-Heidelberg, Germany.Google Scholar
- BUCHI, J.R. 1962. On a decision method in restricted second-order arithmetic. In Proceedings of the International Congress on Logic, Methodology and Philosophy of Science, E. Nagel et al., eds, Stanford University Press, Stanford, Calif., pp. 1-11.Google Scholar
- BUCHI, J. R. 1960. Weak second-order arithmetic and finite automata. Z. Math. Logik Grund. Math. 6, 66-92.Google Scholar
- DE ROUGEMONT, M. 1987. Second order and inductive definability on finite structures. Z. Math. Logik Grund. Math. 33, 47-63.Google Scholar
- DURAND, A., LAUTEMANN, C., AND SCHWENTICK, T. 1998. Subclasses of Binary NP. J. Logic Comput. 8, 2, 189-207.Google Scholar
- EBBINGHAUS, H.-D., AND FLUM, J. 1995. Finite Model Theory. In Perspectives in Mathematical Logic. Springer-Verlag, New York.Google Scholar
- EILENBERG, S. 1974. Automata, Languages, and Machines. Academic Press, New York. Google Scholar
- EITER, T., AND GOTTLOB, G. 1998. On the expressiveness of frame satisfiability and fragments of second order logic. J. Symb. Logic 63, 1, 73-82.Google Scholar
- EITER, T., GOTTLOB, G., AND GUREVICH, Y. 1996. Normal forms for second-order logic over finite structures, and classification of NP optimization problems. Ann. Pure Appl. Logic 78, 111-125.Google Scholar
- FAGIN, R. 1974. Generalized first-order spectra and polynomial-time recognizable sets. In Cornplexity of Computation, R. M. Karp, ed. American Mathematics Society, Providence, R.I., pp. 43-74.Google Scholar
- FAGIN, R. 1975. Generalized monadic spectra. Z. Math. Logik Grund. Math. 21, 89-96.Google Scholar
- FAGIN, R. 1993. Finite-model theory--A personal perspective. Theoret. Comput. Sci. 116, 1, 3-31. Google Scholar
- GRADEL, E. 1991. The expressive power of second-order Horn logic. In Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS '91). Lecture Notes in Computer Science, vol. 480, Springer-Verlag, New York, pp. 466-477. Google Scholar
- GRADEL, E. 1992. Capturing complexity classes with fragments of second order logic. Theoret. Comput. Sci. 101, 5-57. Google Scholar
- GRANDJEAN, E. 1985. Universal quantifiers and time complexity of random access machines. Math. Syst. Theory 13, 171-187.Google Scholar
- GUREVICH, Y. 1988. Logic and the challenge of computer science. In Trends in Theoretical Computer Science, E. B6rger, ed. chapter 1. Computer Science Press, Rockville, Md.Google Scholar
- HENRIKSEN, J. G., JENSEN, J., JORGENSEN, M., KLARLUND, N., PAIGE, B., RAUHE, T., AND SANDHOLM A. 1996. Mona: Monadic second-order logic in practice. In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS'95. Lecture Notes in Computer Science, vol. 1019. Springer-Verlag, New York, pp. 89-110. Google Scholar
- HOPCROFT, J., AND ULLMAN, J. 1979. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading, Mass. Google Scholar
- IMMERMAN, N. 1986. Relational queries computable in polynomial time. Inf. Cont. 68, 86-104. Google Scholar
- IMMERMAN, N. 1987. Languages that capture complexity classes. SIAM J. Comput. 16, 760-778. Google Scholar
- IMMERMAN, N. 1999. Descriptive Complexity. Springer-Verlag, New York.Google Scholar
- KLARLUND, N. 1998. Mona & Fido: The Logic-Automaton Connection in Practice. In Proceedings of the Conference on Computer Science Logic (CSL '97), Mogens Nielsen, Wolfgang Thomas, eds. Lecture Notes in Computer Science, vol. 1414. Springer-Verlag, New York, pp. 311-326. Google Scholar
- KOLAITIS, P., AND PAPADIMITRIOU, C. 1990. Some computational aspects of circumscription. J. ACM 37, 1 (Jan.), 1-15. Google Scholar
- KOLAITIS, P., AND PAPADIMITRIOU, C.H. 1991. Why not negation by fixpoint? J. Comput. Syst. Sci. 43, 125-144. Google Scholar
- KOLAITIS, P., AND THAKUR, M.N. 1995. Approximation properties of NP minimization classes. J. Comput. Syst. Sci. 50, 391-411. Google Scholar
- KOLAITIS, P., AND VARDI, M.Y. 1990. 0-1 Laws and decision problems for fragments of secondorder logic. Inf. Comput. 87, 302-338. Google Scholar
- LAUTEMANN, C., SCHWENTICK, T., AND THI~RIEN, D. 1995. Logics for context-free languages. In Proceedings of the Conference on Computer Science Logic (CSL '94). Leszek Pacholski, Jerzy Tiuryn, eds. Lecture Notes in Computer Science, vol. 933, Springer-Verlag, New York, pp. 205-216. Google Scholar
- LEIVANT, D. 1989. Descriptive characterizations of computational complexity. J. Comput. Syst. Sci. 39, 51-83. Google Scholar
- LYNCH, J.F. 1992. The quantifier structure of sentences that characterize nondeterministic time complexity. Comput. Complex. 2, 40-66. Google Scholar
- MCNAUGHTON, R., AND PAPERT, S. 1971. Counter-Free Automata. MIT Press, Cambridge, Mass. Google Scholar
- OLIVE, F. 1998. A conjunctive logical characterization of nondeterministic linear time. In Proceedings of the Conference on Computer Science Logic (CSL '97), Mogens Nielsen, Wolfgang Thomas, eds. Lecture Notes in Computer Science, vol. 1414, Springer-Verlag, New York, pp. 360-372. Google Scholar
- PACHOLSKI, L., AND SZWAST, W. 1991. On the 0-1 law for the existential second-order minimal G6del sentences with equality. In Proceedings of the 6th Annual Symposium on Logic in Computer Science (LICS '91). IEEE Computer Science Press, Los Alamitos, Calif., pp. 290-285.Google Scholar
- PANCONESI, A., AND RANJAN, D. 1993. Quantifiers and approximation. Theoret. Comput. Sci. 107, 145-163. Google Scholar
- PAPADIMITRIOU, C. H., AND YANNAKAKIS, M. 1991. Optimization, approximation, and complexity classes. J. Comput. Syst. Sci. 43, 425-440.Google Scholar
- PIN, J.-E. 1986. Varieties of Formal Languages. North Oxford, London and Plenum, New York. Google Scholar
- PIN, J.-E. 1994. Logic on words. Bull. EATCS 54, 145-165.Google Scholar
- PIN, J.-E. 1996. Semigroups and automata on words. Ann. Math. Artif. Int. 16, 343-384.Google Scholar
- ROSEN, E. 1999. An existential fragment of second order logic. Arch. Math. Logic 38, 217-234.Google Scholar
- SACCA, D. 1997. The expressive powers of stable models for bound and unbound DATALOG queries. J. Comput. Syst. Sci. 54, 3, 441-464. Google Scholar
- SCHAEFER, T.J. 1978. The complexity of satisfiability problems. In Proceedings of the lOth Annual ACM Symposium on the Theory of Computing (STOC '78) (San Diego, Calif., May 1-3). ACM, New York, pp. 216-226. Google Scholar
- SCHLIPF, J. 1995. The expressive powers of logic programming semantics. J. Comput. Syst. Sci. 51, 1, 64-86. Google Scholar
- SCHWENTICK, T. 1994. Graph connectivity and monadic NP. In Proceedings of the IEEE Symposium on Foundations of Computer Science (FOCS '94). IEEE Computer Science Press, Los Alamitos, Calif., pp. 614-622.Google Scholar
- SCHWENTICK, T. 1995. Graph connectivity, monadic NP and built-in relations of moderate degree. In Proceedings of the 22nd International Colloquium on Automata, Languages, and Programming (ICALP '95), Zoltfin Ftil6p and Ferene Gicseg, Eds. Lecture Notes in Computer Science, vol. 944. Springer-Verlag, New York, pp. 405-416. Google Scholar
- STOCKMEYER, L.J. 1977. The polynomial-time hierarchy. Theoret. Comput. Sci. 3, 1-22.Google Scholar
- STRAUBING, H. 1994. Finite Automata, Formal Logic, and Circuit Complexity. Birkhfiuser, Berlin, Boston, Basel. Google Scholar
- STRAUBING, H., THERIEN, D., AND THOMAS, W. 1995. Regular languages defined with generalized quantifiers. Inf. Computat. 118, 289-301. Google Scholar
- THOMAS, W. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science, volume B, chapter 4, J. van Leeuwen, ed. Elsevier Science Publishers B.V. (North-Holland). Google Scholar
- THOMAS, W. 1996. Languages, automata, and logic. In Handbook of Formal Language Theory, vol. III, G. Rozenberg and A. Salomaa, eds. Springer-Verlag, New York, pp. 389-455. Google Scholar
- TRAKHTENBROT, B.A. 1961. Finite automata and the logic of monadic predicates. Dokl. Akad. Nauk SSSR 140, 326-329.Google Scholar
- VARDI, M.Y. 1982. The complexity of relational query languages. In Proceedings of the 14th ACM Symposium on the Theory of Computing (STOC '82) (San Francisco, Calif., May 5-7). ACM, New York, pp. 137-146. Google Scholar
Index Terms
- Existential second-order logic over strings
Recommendations
Existential second-order logic over graphs: Charting the tractability frontier
Fagin's theorem, the first important result of descriptive complexity, asserts that a property of graphs is in NP if and only if it is definable by an existential second-order formula. In this article, we study the complexity of evaluating existential ...
The model checking problem for prefix classes of second-order logic: a survey
Fields of logic and computationIn this paper, we survey results related to the model checking problem for second-order logic over classes of finite structures, including word structures (strings), graphs, and trees, with a focus on prefix classes, that is, where all quantifiers (both ...
Existential second-order logic and modal logic with quantified accessibility relations
This article investigates the role of arity of second-order quantifiers in existential second-order logic, also known as Σ 1 1 . We identify fragments L of Σ 1 1 where second-order quantification of relations of arity k 1 is (nontrivially) vacuous in ...
Reviews
Jan Van den Bussche
Strings over a finite alphabet can be naturally represented as structures in the sense of mathematical logic. Indeed, for a string a 1 &ldots;a n , we have a finite structure with n points, 1,&ldots;,n , the order relation < on 1,&ldots;,n , and, for every letter b , a unary predicate P b true on exactly those i for which a i =b . This representation allows us to link classical complexity classes, such as NP or the regular languages, with logics, such as first-order logic or existential second-order logic. Indeed, for any sentence 4 in some logic, we can consider the set of all strings (represented as structures) that satisfy 4 , giving us a formal language, which then may, or may not, belong to some complexity class. For example, in first-order logic, the language defined by any sentence is always regular. If we move to existential monadic second-order logic (EMSO), where second-order quantifiers must be existential, in front of the formula, and over monadic (unary) predicates only, we still can define only regular languages, and any regular language is definable by some EMSO-sentence. This is Bu¨chi's theorem, and can be paraphrased by saying that EMSO “captures” the class of regular languages. If we move further to full existential second-order logic (ESO), where second-order quantifiers must still be existential and in front of the formula, but need not be monadic, we capture NP; this is Fagin's theorem. In this paper, the authors investigate what happens with fragments of ESO defined by restrictions on the quantifier prefix of the first-order part (assumed to be in prenex normal form) of the ESO-sentences. These restrictions are expressed by prefix classes (strings over ?,?,? *,? * ) already known from the investigation of the classical decision problem for first-order logic [1]. The results are remarkable. The authors show that such an ESO-prefix class fragment either can define only regular languages, or can already define NP-complete languages. More specifically, the “regular” fragments are all contained in ESO ? *?? * or ESO ? *? ? , and the “NP-complete” fragments all contain ESO ? ? ? , ESO ? ?? <__?__Pub Caret> , or ESO ??? . The mathematical proofs of these theorems involve new combinatorial results on hypergraphs. This well-written paper contains an extensive bibliography. It will interest researchers working in the field of logic and computational complexity.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments