9/29/97 - Dexter Kozen
Cornell University
On the Complexity of Reasoning in Kleene Algebra

In this talk I will discuss the complexity of reasoning in Kleene algebra and *-continuous Kleene algebra in the presence of extra equational assumptions E; that is, the complexity of deciding the validity of universal Horn formulas E --> s=t, where E is a finite set of equations. There is good practical motivation for understanding the complexity of this system; for example, it has been used successfully in the verification of caching protocols.

I will give a hierarchy of complexity results based on the form of the assumptions E: -- if E contains only commutativity assumptions pq=qp, the problem is Pi-1-0-complete; -- if E contains only monoid equations x=y, the problem is Pi-2-0-complete; -- for arbitrary equations E, the problem is Pi-1-1-complete.

The last problem is the universal Horn theory of the *-continuous Kleene algebras. This result resolves an open question of Kozen (1991).