
Derivative Based Methods for Deciding SKA and SKAT
Sabine Broda, Sílvia Cavadas, Nelma Moreira
Centro de Matemática da Universidade do Porto
R. Campo Alegre 687, 4169007 Porto, Portugal
email: sbb@dcc.fc.up.pt,silviacavadas@gmail.com, nam@dcc.fc.up.pt
May 2014
Abstract
Synchronous Kleene algebra (SKA) is a decidable framework that
combines Kleene algebra (KA) with a synchrony model of concurrency.
Elements of SKA can be seen as processes taking place within a
fixed discrete
time frame and that, at each time step, may execute one or more
basic actions or then come to a halt. The extension synchronous
Kleene algebra with tests (SKAT) combines SKA with a boolean
algebra. Both algebras were introduced by C. Prisicariu, who proved the
completeness of SKA axioms, and thus decidability,
through a Kleene theorem based on the classical Thompson
epsilonNFA construction. Using the notion of
partial derivatives, we present a new decision
procedure for SKA terms equivalence. The results are extended for SKAT
considering automata with transitions labeled by boolean expressions instead of
atoms. This work extends previous one done for KA and KAT,
where derivative based methods have been used in feasible algorithms
for testing terms equivalence.
