SFA

Symbolic Finite Automata (SFAs) [3, 9, 19] are finite state automata in which the alphabet is given by a Boolean algebra that may have an infinite domain, and transitions are labeled with predicates over such algebra. In order for SFAs to be closed under Boolean operations and preserve decidability of equivalence, it should be decidable to check whether predicates in the algebra are satisfiable. SFAs accept languages of strings over a potentially infinite domain. Although strictly more expressive than finite-state automata, Symbolic Finite Automata are closed under Boolean operations and admit decidable equivalence.

— Symbolic Visibly Pushdown Automata

SFA (s-FA) - symbolic finite automata. Recognizes Regular languages, specifically RE with lookahead.

Other variation: SAFA (s-AFA) - Symbolic Alternating Finite Automata.

Read more here:

• A Symbolic Decision Procedure for Symbolic Alternating Finite Automata