Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests

TL;DR

This paper introduces symbolic automata algorithms for efficient language equivalence checking, and applies these techniques to decide equivalence in Kleene algebra with tests, enhancing verification methods.

Contribution

It presents novel algorithms for language equivalence using symbolic automata with BDDs and extends these methods to Kleene algebra with tests for improved decision procedures.

Findings

Efficient algorithms for language equivalence of automata over large alphabets.

Symbolic automata construction methods for KAT expressions.

Decidability results for KAT expression equivalence.

Abstract

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 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 standard automata constructions. All in all, this results in efficient algorithms for deciding equivalence of KAT expressions.