A predicate-augmented finite state recognizer (pfsr) *M* is
specified by
where *Q* is a finite set of
states, a set of symbols, a set of
predicates over , *E* a finite set of transitions
.
Furthermore, is a set of start states
and is a set of final states.

The relation is defined inductively:

- for all , ,
- for all , ,
- for all and for all , if then
- if (
*q*_{0},*x*_{1},*q*_{1}) and (*q*_{1},*x*_{2},*q*) are both in then

A pfsr is called -free if there are no . For any given pfsr there is an equivalent -free pfsr. It is straightforward to extend the corresponding algorithm for classical automata. Without loss of generality we assume below that pfsr are -free.