zbMATH — the first resource for mathematics

Kleene algebra with hypotheses. (English) Zbl 07158699
Bojańczyk, Mikołaj (ed.) et al., Foundations of software science and computation structures. 22nd international conference, FOSSACS 2019, held as part of the European joint conferences on theory and practice of software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019. Proceedings. Cham: Springer (ISBN 978-3-030-17126-1/pbk; 978-3-030-17127-8/ebook). Lecture Notes in Computer Science 11425, 207-223 (2019).
Summary: We study the Horn theories of Kleene algebras and star continuous Kleene algebras, from the complexity point of view. While their equational theories coincide and are PSPACE-complete, their Horn theories differ and are undecidable. We characterise the Horn theory of star continuous Kleene algebras in terms of downward closed languages and we show that when restricting the shape of allowed hypotheses, the problems lie in various levels of the arithmetical or analytical hierarchy. We also answer a question posed by Cohen about hypotheses of the form \(1=S\) where \(S\) is a sum of letters: we show that it is decidable.
For the entire collection see [Zbl 1408.68009].
68Nxx Theory of software
68Qxx Theory of computing
Full Text: DOI