[pl-seminar] This monday - A symbolic decision procedure for symbolic alternating automata

["Loris D'Antoni" <loris@xxxxxxxxxxx>]

Since no-one signed up, this Monday I'll give an impromptu talk about one of the papers I submitted to POPL. The talk will be accessible to everyone.

Heping: please post the event on the dept announcements

TITLE: A symbolic decision procedure for symbolic alternating automata
WHEN: 09/26 12-1

WHERE: 4310

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.