Skip to main content


eCommons@Cornell >
Faculty of Computing and Information Science >
Computing and Information Science >
Computing and Information Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: On the Coalgebraic Theory of Kleene Algebra with Tests
Authors: Kozen, Dexter
Keywords: Kleene algebra
Kleene algebra with tests
Brzozowski derivative
Issue Date: 14-Mar-2008
Abstract: We develop a coalgebraic theory of Kleene algebra with tests (KAT) along the lines of Rutten (1998) for Kleene algebra (KA) and Chen and Pucella (2003) for a limited version of KAT, resolving two open problems of Chen and Pucella. Our treatment includes a simple definition of the Brzozowski derivative for KAT expressions and an automata-theoretic interpretation involving automata on guarded strings. We also give a complexity analysis, showing that an efficient implementation of coinductive equivalence proofs in this setting is tantamount to a standard automata-theoretic construction. It follows that coinductive equivalence proofs can be generated automatically in PSPACE. This matches the bound of Worthington (2008) for the automatic generation of equational proofs in KAT.
Appears in Collections:Computing and Information Science Technical Reports

Files in This Item:

File Description SizeFormat
ChenPucella.pdf213.33 kBAdobe PDFView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us