WHERE: 4310
Loris D'Antoni
ABSTRACT:
We introduce Symbolic Alternating Finite Automata (SAFA) as an expressive, succinct, and decidable model for describing sets of finite sequences over arbitrary alphabets. Boolean operations over SAFAs have linear complexity, which is in sharp contrast with the
quadratic cost of intersection and union for non-alternating symbolic automata. Unfortunately, due to this succinctness, emptiness and equivalence checking are PSpaceHard. We introduce a novel algorithm for checking the equivalence of two SAFAs based on bisimulation
up to congruence. This algorithm allows us to exploit the power of SAT and SMT solvers to efficiently search the state space of the SAFAs.
We evaluate our decision procedure on two verification and security applications: 1) checking satisfiability of linear temporal logic formulas over finite traces, and 2) checking equivalence of Boolean combinations of regular expressions.Our experiments show
that our technique often outperforms existing techniques and it can be beneficial in both such applications.
![[Computer Systems Lab]](http://www.cs.wisc.edu/pics/csl_logo.gif){kind=logo}