Kleene Algebra with Tests and Program Schematology
| dc.contributor.author | Angus, Allegra | en_US |
| dc.contributor.author | Kozen, Dexter | en_US |
| dc.date.accessioned | 2007-04-09T19:56:22Z | |
| dc.date.available | 2007-04-09T19:56:22Z | |
| dc.date.issued | 2001-07-10 | en_US |
| dc.description.abstract | The theory of flowchart schemes has a rich history going back to Ianov (1960); see Manna (1974) for an elementary exposition. A central question in the theory of program schemes is scheme equivalence. Manna presents several examples of equivalence proofs that work by simplifying the schemes using various combinatorial transformation rules. In this paper we present a purely algebraic approach to this problem using Kleene algebra with tests (KAT). Instead of transforming schemes directly using combinatorial graph manipulation, we regard them as a certain kind of automaton on abstract traces. We prove a generalization of Kleene's theorem and use it to construct equivalent expressions in the language of KAT. We can then give a purely equational proof of the equivalence of the resulting expressions. We prove soundness of the method and give a detailed example of its use. | en_US |
| dc.format.extent | 312235 bytes | |
| dc.format.mimetype | application/postscript | |
| dc.identifier.citation | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR2001-1844 | en_US |
| dc.identifier.uri | https://hdl.handle.net/1813/5831 | |
| dc.language.iso | en_US | en_US |
| dc.publisher | Cornell University | en_US |
| dc.subject | computer science | en_US |
| dc.subject | technical report | en_US |
| dc.title | Kleene Algebra with Tests and Program Schematology | en_US |
| dc.type | technical report | en_US |
Files
Original bundle
1 - 1 of 1