A BDD-like Implementation of an Automata
Jean‐Michel Couvreur · 2004
In this paper we propose a new data structure, called shared automata, for representing deterministic finite automata (DFA). Shared automata admit a strong canonical form for DFA similarly to Binary Decision Diagrams (BDDs). As a re- sult, checking whether two DFAs are equal is a constant-time comparison. A hash- based cache can be used to improve significantly the performance of automata op- erations. The key points of this structure are the decomposition of the DFA into its strongly connected components and an incremental algorithm based on this decom- position for transforming any DFA into a shared automaton. We experimentally compare PresTaf, a direct implementation of the Presburger arithmetic built on a shared automata package, and the Presburger package LASH based on standard au- tomata algorithms. Experimental results show the great benefit of the new canonical data structure applied to symbolic state space exploration of infinite systems.