Skip to main content

A Symbolic Decision Procedure for Symbolic Alternating Finite Automata

Author(s): D'Antoni, Loris; Kincaid, Zachary; Wang, Fang

To refer to this page use:
Abstract: We introduce Symbolic Alternating Finite Automata (s-AFA) as a succinct and decidable model for describing sets of finite sequences over arbitrary alphabets. Boolean operations over s-AFAs have linear complexity, which contrasts 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 exploits the power of SAT 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 formulae over finite traces, and 2) checking equivalence of Boolean combinations of regular expressions. Our experiments show that our technique can be beneficial in both applications.
Publication Date: 16-Apr-2018
Citation: D'Antoni, Loris, Zachary Kincaid, and Fang Wang. "A Symbolic Decision Procedure for Symbolic Alternating Finite Automata." Electronic Notes in Theoretical Computer Science 336 (2018): pp. 79-99. doi:10.1016/j.entcs.2018.03.017
DOI: 10.1016/j.entcs.2018.03.017
ISSN: 1571-0661
Pages: 79 - 99
Type of Material: Journal Article
Journal/Proceeding Title: Electronic Notes in Theoretical Computer Science
Version: Final published version. This is an open access article.
Notes: The Thirty-third Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII)

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.