A Symbolic Decision Procedure for Symbolic Alternating Finite Automata

TL;DR

This paper introduces Symbolic Alternating Finite Automata (s-AFA), a highly expressive and efficient model for finite sequences, with a novel equivalence checking algorithm leveraging SAT/SMT solvers, demonstrated in verification and security tasks.

Contribution

The paper presents s-AFA as a new automata model with linear Boolean operations and a bisimulation-based equivalence algorithm utilizing SAT/SMT solvers, improving efficiency in key applications.

Findings

s-AFA offers linear complexity for Boolean operations

The equivalence checking algorithm is efficient and scalable

Experiments outperform existing techniques in verification and security tasks

Abstract

We introduce Symbolic Alternating Finite Automata (s-AFA) as an expressive, succinct, and decidable model for describing sets of finite sequences over arbitrary alphabets. Boolean operations over s-AFAs have linear complexity, which is in sharp contrast with the quadratic cost of intersection and union for non-alternating symbolic automata. Due to this succinctness, emptiness and equivalence checking are PSpace-hard. We introduce an algorithm for checking the equivalence of two s-AFAs 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 s-AFAs. 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.