A Symbolic Decision Procedure for Symbolic Alternating Finite Automata

Loris D'Antoni, Zachary Kincaid, Fang Wang

Research output: Contribution to journalArticle

1 Scopus citations

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.

Original languageEnglish (US)
Pages (from-to)79-99
Number of pages21
JournalElectronic Notes in Theoretical Computer Science
Volume336
DOIs
StatePublished - Apr 16 2018

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Keywords

  • Automata
  • decision procedures

Fingerprint Dive into the research topics of 'A Symbolic Decision Procedure for Symbolic Alternating Finite Automata'. Together they form a unique fingerprint.

  • Cite this