Definition

A predicate-augmented finite state recognizer (pfsr) M is specified by $(Q,\Sigma,\Pi,E,S,F)$ where Q is a finite set of states, $\Sigma$ a set of symbols, $\Pi$ a set of predicates over $\Sigma$, E a finite set of transitions $Q \times (\Pi \cup \{\epsilon\}) \times Q$. Furthermore, $S\subseteq Q$ is a set of start states and $F\subseteq Q$ is a set of final states.

The relation $\widehat{E} \subseteq Q \times \Sigma^* \times Q$ is defined inductively:

1. for all $q\in Q$, $(q,\epsilon,q)\in\widehat{E}$,
2. for all $(p,\epsilon,q)\in E$, $(p,\epsilon,q)\in \widehat{E}$,
3. for all $(q_0,\pi,q)\in E$ and for all $\sigma\in\Sigma$, if $\pi(\sigma)$ then $(q_0,\sigma,q)\in\widehat{E}$
4. if (q₀,x₁,q₁) and (q₁,x₂,q) are both in $\widehat{E}$ then $(q_0,x_1x_2,q)\in\widehat{E}$

The language L(M) accepted by M is defined to be $\{w\in\Sigma^*\vert q_s\in S, q_f\in F, (q_s,w,q_f)\in\widehat{E}\}$.

A pfsr is called $\epsilon$-free if there are no $(p,\epsilon,q)\in E$. For any given pfsr there is an equivalent $\epsilon$-free pfsr. It is straightforward to extend the corresponding algorithm for classical automata. Without loss of generality we assume below that pfsr are $\epsilon$-free.