Geodesic
Algorithmic complexity for theories of commutative Kleene algebras
Izvestiya. Mathematics , Tome 88 (2024) no. 2, pp. 236-269.

Voir la notice de l'article provenant de la source Math-Net.Ru

Kleene algebras are structures with addition, multiplication and constants $0$ and $1$, which form an idempotent semiring, and the Kleene iteration operation. In the particular case of $*$-continuous Kleene algebras, Kleene iteration is defined, in an infinitary way, as the supremum of powers of an element. We obtain results on algorithmic complexity for Horn theories (semantic entailment from finite sets of hypotheses) of commutative $*$-continuous Kleene algebras. Namely, $\Pi_1^1$-completeness for the Horn theory and $\Pi^0_2$-completeness for its fragment, where iteration cannot be used in hypotheses, is proved. These results are commutative counterparts of the corresponding theorems of D. Kozen (2002) for the general (non-commutative) case. Several accompanying results are also obtained.
Keywords: Kleene algebras, algorithmic complexity, infinitary logic. 
@article{IM2_2024_88_2_a3,
     author = {S. L. Kuznetsov},
     title = {Algorithmic complexity for theories of commutative {Kleene} algebras},
     journal = {Izvestiya. Mathematics },
     pages = {236--269},
     publisher = {mathdoc},
     volume = {88},
     number = {2},
     year = {2024},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/IM2_2024_88_2_a3/}
}
TY  - JOUR
AU  - S. L. Kuznetsov
TI  - Algorithmic complexity for theories of commutative Kleene algebras
JO  - Izvestiya. Mathematics 
PY  - 2024
SP  - 236
EP  - 269
VL  - 88
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/IM2_2024_88_2_a3/
LA  - en
ID  - IM2_2024_88_2_a3
ER  - 
%0 Journal Article
%A S. L. Kuznetsov
%T Algorithmic complexity for theories of commutative Kleene algebras
%J Izvestiya. Mathematics 
%D 2024
%P 236-269
%V 88
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/IM2_2024_88_2_a3/
%G en
%F IM2_2024_88_2_a3
S. L. Kuznetsov. Algorithmic complexity for theories of commutative Kleene algebras. Izvestiya. Mathematics , Tome 88 (2024) no. 2, pp. 236-269. http://geodesic.mathdoc.fr/item/IM2_2024_88_2_a3/

[1] S. C. Kleene, “Representation of events in nerve nets and finite automata”, Automata studies, Ann. of Math. Stud., 34, Princeton Univ. Press, Princeton, NJ, 1956, 3–41 | DOI | MR | Zbl

[2] D. Kozen, “On Kleene algebras and closed semirings”, Mathematical foundations of computer science (Banská Bystrica 1990), Lecture Notes in Comput. Sci., 452, Springer-Verlag, Berlin, 1990, 26–47 | DOI | MR | Zbl

[3] V. Pratt, “Action logic and pure induction”, Logics in AI (Amsterdam 1990), Lecture Notes in Comput. Sci., 478, Lecture Notes in Artificial Intelligence, Springer-Verlag, Berlin, 1991, 97–120 | DOI | MR | Zbl

[4] V. N. Red'ko, “On the algebra of commutative events”, Ukrain. Mat. Zh., 16:2 (1964), 185–195 (Russian) | MR | Zbl

[5] R. J. Parikh, “On context-free languages”, J. Assoc. Comput. Mach., 13:4 (1966), 570–581 | DOI | MR | Zbl

[6] D. Kozen, “On the complexity of reasoning in Kleene algebra”, Inform. and Comput., 179:2 (2002), 152–162 | DOI | MR | Zbl

[7] S. L. Kuznetsov, “On the complexity of reasoning in Kleene algebra with commutativity conditions”, Theoretical aspects of computing – ICTAC 2023 (Lima 2023), Lecture Notes in Comput. Sci., 14446, Springer, Cham, 2023, 83–99 | DOI

[8] S. L. Kuznetsov, “Reasoning in commutative Kleene algebras from $*$-free hypotheses”, The Logica yearbook 2021, College Publications, London, 2022, 99–113 | MR

[9] E. Palka, “An infinitary sequent system for the equational theory of $*$-continuous action lattices”, Fund. Inform., 78:2 (2007), 295–309 | MR | Zbl

[10] W. Buszkowski and E. Palka, “Infinitary action logic: complexity, models and grammars”, Studia Logica, 89:1 (2008), 1–18 | DOI | MR | Zbl

[11] J.-Y. Girard, “Linear logic”, Theoret. Comput. Sci., 50:1 (1987), 1–101 | DOI | MR | Zbl

[12] S. L. Kuznetsov and S. O. Speranski, “Infinitary action logic with exponentiation”, Ann. Pure Appl. Logic, 173:2 (2022), 103057 | DOI | MR | Zbl

[13] S. L. Kuznetsov and S. O. Speranski, “Infinitary action logic with multiplexing”, Studia Logica, 111:2 (2023), 251–280 | DOI | MR | Zbl

[14] P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar, “Decision problems for propositional linear logic”, Ann. Pure Appl. Logic, 56:1-3 (1992), 239–311 | DOI | MR | Zbl

[15] S. L. Kuznetsov, “Kleene star, subexponentials without contraction, and infinite computations”, Sib. Èlektron. Mat. Izv., 18:2 (2021), 905–922 | DOI | MR | Zbl

[16] V. Danos, J.-B. Joinet, and H. Schellinx, “The structure of exponentials: uncovering the dynamics of linear logic proofs”, Computational logic and proof theory (Brno 1993), Lecture Notes in Comput. Sci., 713, Springer-Verlag, Berlin, 1993, 159–171 | DOI | MR | Zbl

[17] M. L. Minsky, “Recursive unsolvability of Post's problem of “tag” and other topics in theory of Turing machines”, Ann. of Math. (2), 74:3 (1961), 437–455 | DOI | MR | Zbl

[18] S. L. Kuznetsov, “Commutative action logic”, J. Logic Comput., 33:6 (2023), 1437–1462 | DOI | MR

[19] L. Straßburger, “On the decision problem for MELL”, Theor. Comput. Sci., 768 (2019), 91–98 | DOI | MR | Zbl

[20] R. Schroeppel, A two counter machine cannot calculate $2^N$, Report no. AIM-257, MIT, Cambridge, MA, 1972 https://dspace.mit.edu/handle/1721.1/6202

[21] E. Börger, Computability, complexity, logic, Stud. Logic Found. Math., 128, North-Holland Publishing Co., Amsterdam, 1989 | MR | Zbl

[22] S. C. Kleene, “Arithmetical predicates and function quantifiers”, Trans. Amer. Math. Soc., 79 (1955), 312–340 | DOI | MR | Zbl

[23] C. Spector, “Recursive well-orderings”, J. Symb. Log., 20:2 (1955), 151–163 | DOI | MR | Zbl

[24] P. Odifreddi, Classical recursion theory. The theory of functions and sets of natural numbers, Stud. Logic Found. Math., 125, North-Holland Publishing Co., Amsterdam, 1989 | MR | Zbl