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
If and is a singleton set, then the transitions where are equivalent.
The relation is defined inductively.