Abstract
The universal Horn theory of relational Kleene algebra with tests is of practical interest, particularly for program semantics, where Horn formulas can be used to verify correctness of programs or compiler optimizations. Unfortunately, this theory is known to be Π\(_{\rm 1}^{\rm 1}\)-complete. However, many formulas arising in practice fall into fragments of the theory that are of lower complexity. In this paper, we see that the location of occurrences of the Kleene asterate operator * within a formula has a great impact on complexity. Using syntactic criteria based on the location of *, we give a fragment of the theory that is Σ\(_{\rm 1}^{\rm 0}\)-complete, and a slightly larger fragment that is Π\(_{\rm 2}^{\rm 0}\)-complete. We show that the same results hold over *-continuous Kleene algebras with tests. The techniques exhibit a relationship between first-order logic and the Horn theories of relational and *-continuous Kleene algebra, even though the theories are not first-order axiomatizable.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Burris, S., Sankappanavar, H.P.: A Course in Universal Algebra. Springer, New York (1981), Also available online: http://www.thoralf.uwaterloo.ca/htdocs/ualg.html
Cohen, E.: Hypotheses in Kleene Algebra (Unpublished)
Cohen, E., Kozen, D., Smith, F.: The complexity of Kleene algebra with tests. Technical Report 96-1598, Computer Science Department, Cornell University (July 1996)
Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall, London (1971)
Hardin, C., Kozen, D.: On the Complexity of the Horn Theory of REL. Technical Report 2003-1896, Computer Science Department, Cornell University (May 2003)
Hardin, C., Kozen, D.: On the Elimination of Hypotheses in Kleene Algebra with Tests. Technical Report 2002-1879, Computer Science Department, Cornell University (October 2002)
Kozen, D.: On Kleene algebras and closed semirings. In: Rovan, B. (ed.) MFCS 1990. LNCS, vol. 452, pp. 26–47. Springer, Heidelberg (1990)
Kozen, D.: On the Complexity of Reasoning in Kleene Algebra. Information and Computation 179, 152–162 (2002)
Kozen, D.: The Design and Analysis of Algorithms. Springer, New York (1991)
Kozen, D., Smith, F.: Kleene algebra with tests: completeness and decidability. In: van Dalen, D., Bezem, M. (eds.) CSL 1996. LNCS, vol. 1258, pp. 244–259. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hardin, C. (2005). How the Location of * Influences Complexity in Kleene Algebra with Tests. In: Baader, F., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2005. Lecture Notes in Computer Science(), vol 3452. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32275-7_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-32275-7_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25236-8
Online ISBN: 978-3-540-32275-7
eBook Packages: Computer ScienceComputer Science (R0)