Complexity of Reasoning in Kleene and Action Algebras
ESSLLI 2022 course by Stepan Kuznetsov
Iteration, or Kleene star, is one of the most mysterious algebraic operation that appears in computer science. Even simple theories involving this operation happen to enjoy properties which are more usual for strong systems with induction (like first-order arithmetic), and thus, high algorithmic complexity. In the proposed course, we survey complexity results for theories of algebras with the Kleene star. We start with classical results by Kozen (1994, 2002) on complexity of equational and Horn theories for Kleene algebras (but with modern proofs, which utilize circular proof systems by Das and Pous), and then head to recent results on action algebras, that is, Kleene algebras with residuals, by Buszkowski and Palka (2007) and the author (2019-2020). A highlight of this course is the usage of Kleene algebra for modelling infinite computations, dual to subexponential modalities in linear logic.