Existential second-order logic over strings

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.

REFERENCES

• 1: Serge Abiteboul , Richard Hull , Victor Vianu, Foundations of Databases: The Logical Level, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
• 2: AJTAI, M. 1983. ~1 Formulae on Finite Structures. Ann. Pure Appl. Logic 24, 1-48.
• 3: David A. Basin , Nils Klarlund, Hardware Verification using Monadic Second-Order Logic, Proceedings of the 7th International Conference on Computer Aided Verification, p.31-41, July 03-05, 1995
• 4: BERGER, R. 1966. The undecidability of the domino problem. Mem. AMS 66.
• 5: 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.
• 6: 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.
• 7: BUCHI, J. R. 1960. Weak second-order arithmetic and finite automata. Z. Math. Logik Grund. Math. 6, 66-92.
• 8: DE ROUGEMONT, M. 1987. Second order and inductive definability on finite structures. Z. Math. Logik Grund. Math. 33, 47-63.
• 9: DURAND, A., LAUTEMANN, C., AND SCHWENTICK, T. 1998. Subclasses of Binary NP. J. Logic Comput. 8, 2, 189-207.
• 10: EBBINGHAUS, H.-D., AND FLUM, J. 1995. Finite Model Theory. In Perspectives in Mathematical Logic. Springer-Verlag, New York.
• 11: Samuel Eilenberg, Automata, Languages, and Machines, Academic Press, Inc., Orlando, FL, 1974
• 12: 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.
• 13: 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.
• 14: 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.
• 15: FAGIN, R. 1975. Generalized monadic spectra. Z. Math. Logik Grund. Math. 21, 89-96.
• 16: Ronald Fagin, Finite-model theory—a personal perspective, Theoretical Computer Science, v.116 n.1, p.3-31, Aug. 2, 1993
• 17: Erich Grädel, The expressive power of second order Horn logic, Proceedings of the 8th annual symposium on Theoretical aspects of computer science, p.466-477, February 1991, Hamburg, Germany
• 18: Erich Grädel, Capturing complexity classes by fragments of second-order logic, Theoretical Computer Science, v.101 n.1, p.35-57, July 13, 1992 [doi>10.1016/0304-3975(92)90149-A]
• 19: GRANDJEAN, E. 1985. Universal quantifiers and time complexity of random access machines. Math. Syst. Theory 13, 171-187.
• 20: 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.
• 21: Jesper G. Henriksen , Jakob L. Jensen , Michael E. Jørgensen , Nils Klarlund , Robert Paige , Theis Rauhe , Anders Sandholm, Mona: Monadic Second-Order Logic in Practice, Proceedings of the First International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.89-110, May 19-20, 1995
• 22: John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 23: Neil Immerman, Relational queries computable in polynomial time, Information and Control, v.68 n.1-3, p.86-104, Jan/Feb/March 1986 [doi>10.1016/S0019-9958(86)80029-8]
• 24: Neil Immerman, Languages that capture complexity classes, SIAM Journal on Computing, v.16 n.4, p.760-778, Aug. 1987 [doi>10.1137/0216051]
• 25: IMMERMAN, N. 1999. Descriptive Complexity. Springer-Verlag, New York.
• 26: Nils Klarlund, Mona & Fido: The Logic-Automaton Connection in Practice, Selected Papers from the11th International Workshop on Computer Science Logic, p.311-326, August 23-29, 1997
• 27: Phokion G. Kolaitis , Christos H. Papadimitriou, Some computational aspects of circumscription, Journal of the ACM (JACM), v.37 n.1, p.1-14, Jan. 1990 [doi>10.1145/78935.78936]
• 28: Phokion G. Kolaitis , Christos H. Papadimitriou, Why not negation by fixpoint?, Journal of Computer and System Sciences, v.43 n.1, p.125-144, Aug. 1991 [doi>10.1016/0022-0000(91)90033-2]
• 29: Phokion G. Kolaitis , Madhukar N. Thakur, Approximation properties of NP minimization classes, Journal of Computer and System Sciences, v.50 n.3, p.391-411, June 1995 [doi>10.1006/jcss.1995.1031]
• 30: Phokion G. Kolaitis , Moshe Y. Vardi, 0-1 laws and decision problems for fragments of second-order logic, Information and Computation, v.87 n.1-2, p.302-338, July/August 1990 [doi>10.1016/0890-5401(90)90065-P]
• 31: Clemens Lautemann , Thomas Schwentick , Denis Thérien, Logics For Context-Free Languages, Selected Papers from the 8th International Workshop on Computer Science Logic, p.205-216, September 25-30, 1994
• 32: D. Leivant, Descriptive characterizations of computational complexity, Journal of Computer and System Sciences, v.39 n.1, p.51-83, Aug. 1989 [doi>10.1016/0022-0000(89)90019-6]
• 33: James F. Lynch, The quantifier structure of sentences that characterize nondeterministic time complexity, Computational Complexity, v.2 n.1, p.40-66, 1992 [doi>10.1007/BF01276438]
• 34: Robert McNaughton , Seymour A. Papert, Counter-Free Automata (M.I.T. research monograph no. 65), The MIT Press, 1971
• 35: Frédéric Olive, A Conjunctive Logical Characterization of Nondeterministic Linear Time, Selected Papers from the11th International Workshop on Computer Science Logic, p.360-372, August 23-29, 1997
• 36: 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.
• 37: Alessandro Panconesi , Desh Ranjan, Quantifiers and approximation, Theoretical Computer Science, v.107 n.1, p.145-163, Jan. 4, 1993 [doi>10.1016/0304-3975(93)90259-V]
• 38: PAPADIMITRIOU, C. H., AND YANNAKAKIS, M. 1991. Optimization, approximation, and complexity classes. J. Comput. Syst. Sci. 43, 425-440.
• 39: Jean Eric Pin , Raymond E. Miller, Varieties Of Formal Languages, Plenum Publishing Co., 1986
• 40: PIN, J.-E. 1994. Logic on words. Bull. EATCS 54, 145-165.
• 41: PIN, J.-E. 1996. Semigroups and automata on words. Ann. Math. Artif. Int. 16, 343-384.
• 42: ROSEN, E. 1999. An existential fragment of second order logic. Arch. Math. Logic 38, 217-234.
• 43: Domenico Saccà, The expressive powers of stable models for bound and unbound DATALOG queries, Journal of Computer and System Sciences, v.54 n.3, p.441-464, June 1997 [doi>10.1006/jcss.1997.1446]
• 44: Thomas J. Schaefer, The complexity of satisfiability problems, Proceedings of the tenth annual ACM symposium on Theory of computing, p.216-226, May 01-03, 1978, San Diego, California, United States [doi>10.1145/800133.804350]
• 45: John S. Schlipf, The expressive powers of the logic programming semantics, Journal of Computer and System Sciences, v.51 n.1, p.64-86, Aug. 1995
• 46: 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.
• 47: Thomas Schwentick, Graph Connectivity, Monadic NP and Built-in Relations of Moderate Degree, Proceedings of the 22nd International Colloquium on Automata, Languages and Programming, p.405-416, July 10-14, 1995
• 48: STOCKMEYER, L.J. 1977. The polynomial-time hierarchy. Theoret. Comput. Sci. 3, 1-22.
• 49: Howard Straubing, Finite automata, formal logic, and circuit complexity, Birkhauser Verlag, Basel, Switzerland, 1994
• 50: Howard Straubing , Denis Thérien , Wolfgang Thomas, Regular languages defined with generalized quantifiers, Information and Computation, v.118 n.2, p.289-301, May 1, 1995 [doi>10.1006/inco.1995.1067]
• 51: Wolfgang Thomas, Automata on infinite objects, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 52: Wolfgang Thomas, Languages, automata, and logic, Handbook of formal languages, vol. 3: beyond words, Springer-Verlag New York, Inc., New York, NY, 1997
• 53: TRAKHTENBROT, B.A. 1961. Finite automata and the logic of monadic predicates. Dokl. Akad. Nauk SSSR 140, 326-329.
• 54: Moshe Y. Vardi, The complexity of relational query languages (Extended Abstract), Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.137-146, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802186]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Model theory

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Relations between models; Automata (e.g., finite, push-down, resource-bounded)
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computational logic
      F.4.3 Formal Languages
          Subjects: Classes defined by grammars or automata (e.g., context-free languages, regular sets, recursive sets)

General Terms:
Languages, Theory

Keywords:
NP, S1S, decision problem, descriptive complexity, existential fragment, finite model theory, finite satisfiability, finite words, model checking, prefix classes, regular languages, second-order logic, strings