Abstract
Kleene algebras with tests provide a rigorous framework for equational specification and verification. They have been used successfully in basic safety analysis, source-to-source program transformation, and concurrency control. We prove the completeness of the equational theory of Kleene algebra with tests and *-continuous Kleene algebra with tests over language-theoretic and relational models. We also show decidability. Cohen’s reduction of Kleene algebra with hypotheses of the form r = 0 to Kleene algebra without hypotheses is simplified and extended to handle Kleene algebras with tests.
Cite
CITATION STYLE
Kozen, D., & Smith, F. (1997). Kleene algebra with tests: Completeness and decidability. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1258, pp. 244–259). Springer Verlag. https://doi.org/10.1007/3-540-63172-0_43
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
