Library

eCommons

 

On the Coalgebraic Theory of Kleene Algebra with Tests

Simple item page
dc.contributor.authorKozen, Dexter
dc.date.accessioned2008-03-14T18:49:38Z
dc.date.available2008-03-14T18:49:38Z
dc.date.issued2008-03-14T18:49:38Z
dc.description.abstractWe 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.en_US
dc.identifier.urihttps://hdl.handle.net/1813/10173
dc.subjectKleene algebraen_US
dc.subjectKleene algebra with testsen_US
dc.subjectBrzozowski derivativeen_US
dc.subjectcoalgebraen_US
dc.subjectcoinductionen_US
dc.titleOn the Coalgebraic Theory of Kleene Algebra with Testsen_US

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
ChenPucella.pdf
Size:
213.33 KB
Format:
Adobe Portable Document Format
Download

Collections

Computing and Information Science Technical Reports