Algorithmic complexity of theories with Kleene iteration

Kleene iteration (star operator) is one of the most interesting algebraic operations arising in computer science. The studies of structures with this operation, Kleene algebras and their extensions, begin with the classical notion of regular expression describing formal languages. Subsequently, so-called action algebras (Pratt 1991, Kozen 1994), or Kleene algebras with division, were introduced. In these structures the Kleene star operator is combined with divisions compatible with a partial order (such operations had previously been introduced by Krull in 1924). This article gives a survey of results on algorithmic complexity for the logical theories of structures with Kleene iteration. Although the simplest of these theories, the theory of equality of regular expressions, is algorithmically decidable, some of its generalizations, such as Horn theories and fragments of these, as well as theories with division, almost immediately become undecidable. Particularly interesting is the case of *-continuous Kleene algebras, where iteration is defined as the limit of powers of an element (in the general case iteration is defined as a fixed point). In the language of logic, *-continuity corresponds to the omega rule, and the complexity of such theories can attain the level of ¹₁-completeness. Bibliography: 83 titles.