Sciweavers

WIA
2004
Springer

A BDD-Like Implementation of an Automata Package

14 years 3 months ago
A BDD-Like Implementation of an Automata Package
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 result, checking whether two DFAs are equal is a constant-time comparison. A hashbased cache can be used to improve significantly the performance of automata operations. The key points of this structure are the decomposition of the DFA into its strongly connected components and an incremental algorithm based on this decomposition 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 automata algorithms. Experimental results show the great benefit of the new canonical data structure applied to symbolic state space exploration of infinite systems. Keywords. shared automaton, Presburger arith...
Jean-Michel Couvreur
Added 03 Jul 2010
Updated 03 Jul 2010
Type Conference
Year 2004
Where WIA
Authors Jean-Michel Couvreur
Comments (0)