2004/05/26 by Hubie Chen, Riccardo Pucella · 1 citation
Computer Science · #cs.LO #cs.PL
published as Theoretical Computer Science, 327 (1-2), 23-44 (2004) · 21 pages, 1 figure; preliminary version appeared in Proc. Workshop on Coalgebraic Methods in Computer Science (CMCS'03)
arxiv created 2004/05/26 · arxiv updated 2009/12/01
Kleene algebra with tests is an extension of Kleene algebra, the algebra of regular expressions, which can be used to reason about programs. We develop a coalgebraic theory of Kleene algebra with tests, along the lines of the coalgebraic theory of regular expressions based on deterministic automata. Since the known automata-theoretic presentation of Kleene algebra with tests does not lend itself to a coalgebraic theory, we define a new interpretation of Kleene algebra with tests expressions and a corresponding automata-theoretic presentation. One outcome of the theory is a coinductive proof principle, that can be used to establish equivalence of our Kleene algebra with tests expressions.