Dipartimento di Ingegneria informatica, automatica e gestionale

The central open question in Descriptive Complexity is whether there is a logic that characterizes deterministic polynomial-time computations (PTIME) on relational structures. In this talk, I introduce my work on this question. I define an algebra of binary relations that is obtained from first-order logic with fixed points, FO(FP), by a series of transformations that include restricting logical connectives and adding a dynamic version of Hilbert’s Choice operator Epsilon. The formalism can also be viewed as a linear-time modal Dynamic logic, where algebraic expressions describing “proofs” or “programs” appear inside the modalities. Many typical polynomial-time properties such as cardinality, reachability and those requiring “mixed” propagations (that include linear equations modulo two) can be specified in the logic, and an arbitrary PTIME Turing machine can be encoded. For each fixed Choice function, the data complexity of model checking is in PTIME. However, there can be exponentially many such functions. ``Naive evaluations'' refer to a version of this model checking procedure where the Choice function variable Epsilon is simply treated as a constant. A crucial question is under what syntactic conditions on the algebraic terms such a naive evaluation works, that is, provides a certain answer to the original model checking problem. These conditions, applied to the formalism, would give us a logic for PTIME. The two views of the formalism, as an algebra and as a Dynamic logic, support application of both automata-theoretic and algebraic techniques to the study of this question.