Two variants of Kleene Algebra and their applications
OA Version
Citation
Abstract
Kleene Algebra (KA) is an equational system celebrated for its decidability andcompleteness with respect to regular language equalities. Because of the desirable
properties of Kleene Algebra, numerous extensions were developed to reason about
network system [45, 48, 60], concurrent programs [38, 61, 57], probabilistic sys-
tems [32, 44], relational verification [76], and program schematology [24]. In this
thesis, we focus on two variants of Kleene Algebra with real-world applications.
The first system, Kleene Algebra with tests and top (TopKAT), was developed
to perform domain and reachablity reasoning. We showed the conventional extension
of Kleene Algebra with tests, despite able to encode Hoare logic, is inadequate for
domain reasoning. This leads to our development of TopKAT, which is complete for
domain reasoning. TopKAT was able to soundly encode both propositional incor-
rectness and Hoare logic [65, 7], offering better complexity bound than alternative
frameworks [69, 79]. Our completeness proof for TopKAT relies heavily on a tech-
nique called reduction, we showed that the reduction from TopKAT to KAT satisfy
nice properties that enable us to generate complete interpretations for TopKAT for
free, and also gives us a complete decision procedure with minimal effort.
The second system, control-flow Guarded Kleene Algebra with Tests (CF-GKAT)
verifies control-flow transformations. Guarded Kleene Algebra with Tests [67] pro-
vides a robust equational system that is not only sound and complete with respect to
trace equivalence, but also enjoys an efficient decision procedure. Yet, GKAT remains
insufficient as a system to verify several well-known control-flow algorithms [13, 52,
37], because it lacks important control-flow structures like indicator variable and non-
local control-flow structures like break, return, and goto. To obtain CF-GKAT, we
extended the syntax and semantics of GKAT to incorporate these essential features.
We have developed an efficient decision procedure for CF-GKAT program utilizing
CF-GKAT automata, an automata model that closely emulates CF-GKAT programs,
and can be efficiently lowered into GKAT automata. Furthermore, this decision pro-
cedure is sound and complete: the algorithm will output true if and only if the two
input programs are trace equivalent.
Description
2024
License
Attribution 4.0 International