A coalgebraic approach to Kleene algebra with tests

DOI10.1016/J.TCS.2004.07.020zbMATH Open1071.68073arXivcs/0405097OpenAlexW2102823559MaRDI QIDQ703519FDOQ703519

Riccardo Pucella, Hubie Chen

Publication date: 11 January 2005

Published in: Theoretical Computer Science (Search for Journal in Brave)

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/cs/0405097

zbMATH Keywords

Kleene algebra with testsAutomataBisimulationCoinduction

Mathematics Subject Classification ID

Algebraic theory of languages and automata (68Q70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Derivatives of Regular Expressions
• Universal coalgebra: A theory of systems
• A note on Coinduction and Weak Bisimilarity for While Programs
• Two Complete Axiom Systems for the Algebra of Regular Events
• A completeness theorem for Kleene algebras and the algebra of regular events
• On the Forms of the Predicates in the Theory of Constructive Ordinals
• Regular expressions and the equivalence of programs

Cited In (5)

• Quantitative Kleene coalgebras
• Canonical finite models of Kleene algebra with tests
• On Hoare logic and Kleene algebra with tests
• A complete inference system for skip-free guarded Kleene algebra with tests
• Position Automata for Kleene Algebra with Tests

This page was built for publication: A coalgebraic approach to Kleene algebra with tests

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q703519)