  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 behaviors of GKAT expressions. 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.
