Complexity of Reasoning in Kleene and Action Algebras

ESSLLI 2022 course by Stepan Kuznetsov

Abstract

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.

Slides

• Lecture 1, Monday August 15
• Lecture 2, Tuesday August 16
• Lecture 3, Wednesday August 17
• Lecture 4, Thursday August 18
• Lecture 5, Friday August 19

Reading

• For Lectures 1-3:
  • A. Das, D. Pous. A cut-free cyclic proof system for Kleene algebra, in: Proc. Tableaux ‘17, LNCS vol. 10501, Springer, 2017, pp. 261-277.
  • A. Das, D. Pous. Non-well-founded proof theory for (Kleene+action) (algebras+lattices), in: Proc. CSL 2018, LIPIcs vol. 119, Dagstuhl, 2018, pp. 19:1-19:18.
• For Lecture 3:
  • D. Kozen. On the complexity of reasoning in Kleene algebra. Inform. Comput., 179:152-162, 2002.
• For Lecture 4:
  • S.L. Kuznetsov. Commutative action logic. J. Logic Comput., exac008, 2022. doi arXiv
• For Lecture 5:
  • W. Buszkowski. On action logic: equational theories of action algebras, J. Logic Comput., 17(1):199-217, 2007.
  • W. Buszkowski, E. Palka. Infinitary action logic: complexity, models, grammars, Stud. Logica, 89(1):1-18, 2008.
  • S. Kuznetsov. Action logic is undecidable. ACM Trans. Comput. Logic, 22:2,10, 2021. doi arXiv
  • S.L. Kuznetsov, S.O. Speranski. Infinitary action logic with exponentiation, Ann. Pure Appl. Logic, 173(2):103057, 2022. doi arXiv