Speaker
Stepan Kuznetsov
(Steklov Institute RAS)
Description
We give a survey of algorithmic complexity results for theories of algebraic structures including Kleene star. Those include Kleene algebras, Kleene lattices, and their extensions with division operations, also called action algebras / lattices. We focus on equational and Horn theories, since already on this level of expressivity we get high levels of undecidability. The talk includes both well-known old results (following Kozen 2002 and Buszkowski 2007), as well as new ones recently obtained by the speaker. The latter include undecidability and complexity of the logic of action algebras, both non-commutative and commutative, and that of the logic of Kleene algebras with commutativity conditions.
