3 papers
cs.LO2023
Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity
Wojciech Różowski, Tobias Kappé, Dexter Kozen +2
We introduce Probabilistic Guarded Kleene Algebra with Tests (ProbGKAT), an extension of GKAT that allows reasoning about uninterpreted imperative programs with probabilistic branc…
cs.LO2023
A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
Tobias Kappé, Todd Schmid, Alexandra Silva
Guarded Kleene Algebra with Tests (GKAT) is a fragment of Kleene Algebra with Tests (KAT) that was recently introduced to reason efficiently about imperative programs. In contrast…
cs.FL2022
An Elementary Proof of the FMP for Kleene Algebra
Tobias Kappé
Kleene Algebra (KA) is a useful tool for proving that two programs are equivalent. Because KA's equational theory is decidable, it integrates well with interactive theorem provers.…