Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests

We first 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 a (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 com-bined with already existing optimisations, and we show in partic-ular 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 alge-braic theory that can be used for verification in various domains ranging from compiler optimisation to network programming anal-ysis. 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 standard automata con-structions. All in all, this results in efficient algorithms for deciding equiv-alence of KAT expressions