Mario Benevides (Universidade Federal Fluminense, Instituto de Computação)
Guarded Kleene Algebra with Tests (GKAT) was presented as a fragment of KAT to abstract imperative programming languages, where only if-then-else and while-do statements are allowed in the language. The loss of expressiveness is, nevertheless, compensated by a clear advantage over KAT: it allows almost linear decidability of program equivalence. In this work, we give the first step to optimizing the complexity of dynamic logic equivalence, which is EXPTIME-complete in PDL. First, and based on Strict Deterministic PDL, we present Guarded Propositional Dynamic Logic (GPDL), a fragment of PDL where programs correspond to GKAT terms. It comes embedded, as expected, with a semantics over relational models and a sound and complete axiomatisation. The main result of this work, the equivalence of GPDL programs can be established in almost linear time.
Poster