Technical Report: DCC-2014-10

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, 4169-007 Porto, Portugal
May 2014


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 epsilon-NFA 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.