A predicate-augmented finite state transducer (pfst) *M* is a tuple
with *Q* a finite set of states, a set
of symbols, a set of predicates over . As before, *S*
and *F* are sets of start states and final states respectively. *E* is
a finite set
. The final component
of a transition is used to indicate identities. For all transitions
(*p*,*d*,*r*,*q*,1) it must be the case that
.^{5}

We define the
function * str* from
to .

If and is a singleton set, then the transitions where are equivalent.

The relation is defined inductively.

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