Schmid, T;
Kappé, T;
Kozen, D;
Silva, A;
(2021)
Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness.
In: Bansal, N and Merelli, E and Worrell, J, (eds.)
ICALP 2021.
(pp. 142:1-142:14).
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Preview |
Text
LIPIcs-ICALP-2021-142.pdf - Published Version Download (948kB) | Preview |
Abstract
Guarded Kleene Algebra with Tests (GKAT) is an efficient fragment of KAT, as it allows for almost linear decidability of equivalence. In this paper, we study the (co)algebraic properties of GKAT. Our initial focus is on the fragment that can distinguish between unsuccessful programs performing different actions, by omitting the so-called early termination axiom. We develop an operational (coalgebraic) and denotational (algebraic) semantics and show that they coincide. We then characterize the behaviors of GKAT expressions in this semantics, leading to a coequation that captures the covariety of automata corresponding to these behaviors. Finally, we prove that the axioms of the reduced fragment are sound and complete w.r.t. the semantics, and then build on this result to recover a semantics that is sound and complete w.r.t. the full set of axioms.
| Type: | Proceedings paper |
|---|---|
| Title: | Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness |
| Event: | 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021) |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.4230/LIPIcs.ICALP.2021.142 |
| Publisher version: | https://drops.dagstuhl.de/opus/volltexte/2021/1421... |
| Language: | English |
| Additional information: | © Todd Schmid, Tobias Kappé, Dexter Kozen, and Alexandra Silva; licensed under Creative Commons License CC-BY 4.0 |
| Keywords: | Kleene algebra, program equivalence, completeness, coequations |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10131994 |
Archive Staff Only
 |
View Item |
