The decision problem for the probabilities of higher-order properties

ABSTRACT

The probability of a property on the class of all finite relational structures is the limit as n → ∞ of the fraction of structures with n elements satisfying the property, provided the limit exists. It is known that 0-1 laws hold for any property expressible in first-order logic or in fixpoint logic, i.e. the probability of any such property exists and is either 0 or 1. It is also known that the associated decision problem for the probabilities is PSPACE-complete and EXPTIME-complete for first-order logic and fixpoint logic respectively. The 0-1 law fails, however, in general for second-order properties and the decision problem becomes unsolvable. We investigate here logics which on the one hand go beyond fixpoint in terms of expressive power and on the other possess the 0-1 law. We consider first iterative logic which is obtained from first order logic by adding while looping as a construct. We show that the 0-1 law holds for this logic and determine the complexity of the associated decision problem. After this we study a fragment of second order logic called strict &Sgr;11. This class of properties is obtained by restricting appropriately the first-order part of existential second-order sentences. Every strict &Sgr;11 property is NP-computable and there are strict &Sgr;11 properties that are NP-complete, such as 3-colorability. We show that the 0-1 law holds for strict &Sgr;11 properties and establish that the associated decision problem is NEXPTIME-complete. The proofs of the decidability and complexity results require certain combinatorial machinery, namely generalizations of Ramsey's Theorem.

REFERENCES

• AH78: Abramson,F.D., Harrington, L.A.: Models without indiscernibles. Y. Symbolic Logic 4silgn),rp. 572 600.
• Aj83: Ajtai, M.' I~{-formu/as on finite structures. Ann. of Po, re and Applied Logic 2443{1983),pp. I 48.
• AU79: Alfred V. Aho , Jeffrey D. Ullman, Universality of data retrieval languages, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.110-119, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567763]
• Ba75: Barwise, J.: Admissible Sets and Str~et,~ret. Springer-Verlag, 1975.
• Be80: Ber:man, L.: The complexity oflogical theories. Theoret. Comp. Sci. 11{1980), pp. 71- 77.
• BGK85: Andreas Blass , Yuri Gurevich , Dexter Kozen, A zero-one law for logic with a fixed-point operator, Information and Control, v.67 n.1-3, p.70-90, Oct./Nov./Dec. 1986 [doi>10.1016/S0019-9958(85)80027-9]
• BH79: Blass, A., Harary, F.: Properties of almost all graphs and complexes. J. Graph The. ory 3(1979),pp. 225 240.
• Bo79: Bollobas, B.: Gr~rh Theory. Springer- Verlag, 1979.
• CH82: Chandra, A., Harel, D.: Structure and Complexity of Relational Queries. J. Computer and Syttem~ Sciences 25(1982), pp. 99-- 128.
• CKS81: Ashok K. Chandra , Dexter C. Kozen , Larry J. Stockmeyer, Alternation, Journal of the ACM (JACM), v.28 n.1, p.114-133, Jan. 1981 [doi>10.1145/322234.322243]
• DG79: Dreben, D., and Goldfarb, W.D.: The Decision Problem: Solvable Ctatset of Q~antificational Formulas. Addison-Wesley, i979.
• Fa74: Fagin, R.: Generalized first order spectra and polynomia! time recognizable sets. Complezity of Computations {R. Karp, ed.), SIAM- AMS Proc. 7(1974), pp.43 73.
• Fa76: Fagin, R.: Probabilities on finite models. J. Symbolic Logic 41(1976). pp. 50 58.
• Ga64: Gaifman, H.: Concerning measures in first order calculi, ltraei J. Math. 2{1964). pp. 1 18.
• GKLT69: Glebskii, Y.V., Kogan, D.I., Liogonkii. M.I., Talanov, V.A.: RanKe and degree of realizability of formulas in the restricted predicate calculus. Cybernetieo S(1969 ), pp. 142 154.
• Go84: Goldfarb, W.D.: The GSdel class with equality is unsolvable. B~li. Amer. Mctk. So~. (N~w s~,i~,) t0(los4), pp. lts-tis.
• Gr83: Grandjean, E.: Complexity of the first order theory of almost all structures, information and Control 52(1983), pp. 180 204.
• Gu84: Gurev{ch, Y' Toward logic tailored for computational complexity. Coml~utatior~ and Proof Theory (M.M. Ricther et al., eds.), Springer Verlag, Lecture Notes in ~fath. 1104, 1984, pp. t75 216.
• Im83: Neil Immerman, Languages which capture complexity classes, Proceedings of the fifteenth annual ACM symposium on Theory of computing, p.347-354, December 1983 [doi>10.1145/800061.808765]
• Im86: 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]
• KS85: Kauffman, M., 5helah, S: On random models of finite power and monaclic logic. Dit. crete J~fat~ematics $4(1985), pp, 285 293.
• Le79: Lewis, H.R.: Unsolvable Classes of Quantificational Formulas.Addison- Wesley, 191'9.
• Le80: Lewis, H.R.: Complexity results for classes of quanti~cational formulas. J. Computer and Syttem Sciencet 21(1980), pp. 317 353.
• Mo74: Moschovakis, Y.N.: ~iementary lndsction on Abstract Struetaret. North Holland, 1974.
• NR77: NegetFil, J., RSdl, V.- Partitions of finite relational and set systems. J. Combinatorial Theory A 22(1977), pp. 289-312.
• NR83: Ne~et~iI, J., RSdl, V.: Ramsey classes of set systems. J. Combinatorial Theory A 34(t983), pp. tS3-20t.
• Po76: P6sa, L.- Hamiltonian circuits in random graphs. Ditcrete Math. 14(t976), pp. 359 364.
• Ra28: Ramsey, F.P.: On a problem in formal logic. Proe. London Math. Soe. 30(1928). pp. 264 286.
• Ra69: Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Trant. AM'S 141(t969). pp. I 35.
• Ry59: Ryll Nardzewski,C.: On the categoricit-y in power Ro. Bull. Aead. Poion. Sei. Sdr. Sci. Math. Attron. Phys. 7(1959), pp. 239 263.
• St76: Stockmeyer, L.J.: The polynomial time hierarchy. Tkeoret. Comp. $ei. 3(1976), pp. I 22.
• Tr50: Trakhtenbrot, B.A.: The impossibilty of an algorithm for the decision problem for finite models. Doklady Akademii Na~k SSR ?0(t0s0), PP. ,$69 5;2.
• Va82: 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]
• Va61: Vaught, R.: Denumerable models of complete theories, lnfinitfstie Metkod~, Pergamon {to61), pp. sos s2t.

INDEX TERMS

Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Probabilistic computation

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

General Terms:
Theory, Verification