Abstract
In this paper, we develop the basic theory of disimulations, a type of relation between two automata which witnesses equivalence. We show that many standard constructions in the theory of automata such as determinization, minimization, inaccessible state removal, et al., are instances of disimilar automata. Then, using disimulations, we define an “algebraic” proof system for the equational theory of Kleene algebra in which a proof essentially consists of a sequence of matrices encoding automata and disimulations between them. We show that this proof system is complete for the equational theory of Kleene algebra, and that proofs in this system can be constructed by a PSPACE transducer.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Cohen, E.: Hypotheses in Kleene Algebra. Technical Report TM-ARH-023814, Bellcore (1993), http://citeseer.ist.psu.edu/1688.html
Fitting, M.: Bisimulations and Boolean Vectors. Advances in Modal Logic 4, 97–125 (2003)
Kozen, D.: A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events. Infor. and Comput 110(2), 366–390 (1994)
Kozen, D., Smith, F.: Kleene Algebra with Tests: Completeness and Decidability. In: van Dalen, D., Bezem, M. (eds.) CSL 1996. LNCS, vol. 1258, pp. 224–259. Springer, Heidelberg (1997)
Kozen, D.: Automata and Computability. In: Undergraduate Texts in Computer Science. Springer, Heidelberg (1997)
Kozen, D.: Typed Kleene Algebra. Technical Report 98-1669, Computer Science Department, Cornell University (March 1998)
Kozen, D.: On Hoare Logic and Kleene Algebra with Tests. Trans. Computational Logic 1(1), 60–76 (2000)
Stockmeyer, L.J., Meyer, A.R.: Word Problems Requiring Exponential Time. In: Proc. 5th Symp. Theory of Computing, pp. 1–9 (1973)
Worthington, J.: Feasibly Reducing KAT Equations to KA Equations, http://arxiv.org/abs/0801.2368
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Worthington, J. (2008). Automatic Proof Generation in Kleene Algebra. In: Berghammer, R., Möller, B., Struth, G. (eds) Relations and Kleene Algebra in Computer Science. RelMiCS 2008. Lecture Notes in Computer Science, vol 4988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78913-0_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-78913-0_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78912-3
Online ISBN: 978-3-540-78913-0
eBook Packages: Computer ScienceComputer Science (R0)