Counting, Quantifiers and Algorithms

Logic (first order or temporal) can be easily extended to describe counts, parity and other numerical phenomena. The satisfiability problem of the extended logic is easily seen to be undecidable, even on models which are finite words. We examine situations in which the satisfiability problem on such models remains decidable (joint work with A V Sreejith).

Temporal logic with modulo counting is Pspace-complete (the lower bound holds without modulo counting, by Sistla and Clarke). Two-variable first order logic with modulo counting quantifiers is Expspace-complete (the upper bound is by an exponential translation to temporal logic, following Etessami, Vardi and Wilke). If positions can be checked for modulo congruence, but parity is kept out of the picture, temporal logic is complete for the third level of the polynomial hierarchy Sigma3P, while two-variable first order logic is Nexptime-complete (the lower bound holds without the congruence checking, by Weis and Immerman). Finally, in the special case of a one-letter alphabet, full first order logic with any number of variables, counting quantifiers and addition built-in is decidable (by Schweikardt); in the case of modulo counting quantifiers we give a double exponential space upper bound. Without the modulo counting quantifiers this is called Presburger arithmetic and is known to be complete for alternating doubly exponential time with a linear number of alternations, shown by Berman. So a small gap remains.

The talk will concentrate on the algorithms rather than on details of complexity classes.