Author: Damien Pous.## Symbolic Algorithms for Language Equivalence and Kleene Algebra with TestsThis page is a web-appendix to the following paper, in Proc. POPL'15. (.pdf) |

*
We propose algorithms for checking language equivalence of
finite automata over a large alphabet. We use symbolic automata,
where the transition function is compactly represented using
(multi-terminal) binary decision diagrams (BDD). The key idea
consists in computing a bisimulation by exploring reachable pairs
symbolically, so as to avoid redundancies. This idea can be combined
with already existing optimisations, and we show in particular a
nice integration with the disjoint sets forest data-structure from
Hopcroft and Karp's standard algorithm.
Then we consider Kleene algebra with tests (KAT), an algebraic
theory that can be used for verification in various domains ranging
from compiler optimisation to network programming analysis. This
theory is decidable by reduction to language equivalence of automata
on guarded strings, a particular kind of automata that have
exponentially large alphabets. We propose several methods allowing
to construct symbolic automata out of KAT expressions, based either
on Brzozowski's derivatives or on standard automata constructions.
All in all, this results in efficient algorithms for deciding
equivalence of KAT expressions.
*

- 2016 February 1st (latest version, 1.4):
- safa 1.4, generic algorithms for symbolic automata (online documentation),
- symkat 1.4, specific KAT automata constructions and decision procedure (online documentation).

- 2014 November 25: safa 1.3, symkat 1.3.
- 2014 October 21: symbolic_kat 1.2.
- 2014 October 7: symbolic_kat 1.1.
- 2014 July 11: symbolic_kat 1.0.

The various algorithms can be tested online, using the following applet. It suffices to write your favourite KAT expressions in the two text fields below. See below for syntax. Guarded strings appearing below the textboxes are typical counter-examples, when one or the other inclusion does not hold. The corresponding automata are depicted, with a trace of the execution of the algorithm represented with violet lines (for the naive algorithm) or arrows (for the Hopcroft and Karp variant). Note that when only one inclusion holds, the depicted trace is that corresponding to the proof of that inclusion (i.e., a trace of x+y=y when x<y holds).

Blue lines (or arrows) represent pairs of states whose outputs have been checked, and whose successors have been pushed to the todo list. Violet lines represent pairs of internal BDD nodes that the algorithm did visit. Dashed blue lines represent pairs of states that could be skipped thanks to the up-to-congruence technique. A red line represent a counter-example: a pair of states with distinct ouputs, that could be reached from the initial states

Hypotheses to eliminate | First expression | Second expression | |||

## Options## ExamplesClick the following examples to load them. ## Syntax- atomic tests are characters from a to j
- atomic Kleene elements are characters from k to z
- multiplication or Boolean conjunction is implicit, by juxtaposition
- addition or Boolean disjunction is +
- Kleene star is postfix *
- Boolean negation is prefix !
- zero and one are 0 and 1
## Elimination of hypothesesYou can enter KAT hypotheses to exploit in the first textbox. They are pairs of KAT expressions related either by inclusion or by equality. Use semicolon (;) to separate pairs; only some kinds of equations can be eliminated: |