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:
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.