We are now ready to define predicate-augmented finite state
transducers with a bounded queue. A predicate-augmented finite state
transducer with queue (qpfst) *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
.

In a transition, each predicate is associated with a queue marker, which is one of {0,1}. On the input side, 1 will imply an enqueue operation of the symbol matching the predicate; on the output side 1 will imply a dequeue operation of the symbol matching the predicate. In the input part of the transition, can be used as well, in which case the queue marker must be 0 (input epsilons will be employed to represent outputs associated with initial and final states). In the output part of a transition we can have instead of a predicate, in order to represent the explicit dequeue operations motivated earlier. We require that every must have a corresponding queue marker which is 1.

The relation determines the effect of the output part of a transition. Its arguments represent respectively the output sequence of a transition, the (incoming and outgoing) queues, and the resulting output string. Note that queues are written from left to right in such a way that an element is enqueued to the left and dequeued from the right.

- for all we have
- if
then for all
we have
- if
then for all
and such that we have
- if then for all and such that we have

The relation is a relation between source states, sequences of input symbols, sequences of output symbols, target states, and source- and target queues. It is defined inductively.

- for all , .
- for each transition such that ,
- for each transition such that and , .
- for each transition such that and , .
- if
(
*q*_{0},*x*_{1},*y*_{1},*q*_{1},*x*_{0},*x*_{1}) and (*q*_{1},*x*_{2},*y*_{2},*q*,*x*_{1},*x*) are both in then

The relation *R*(*M*) accepted by a qpfst *M* is defined to be
.

Such qpfst are generally very powerful. However, the qpfst which result from the generalized transducer determinization algorithm are all limited. Not only are these transducers deterministic by construction, but they are also limited in the way the queue is actually used: in each case the maximum size of the queue is some constant. And of course, since the input was a finite-state transducer, the resulting equivalent qpfst describes a finite-state transduction too. Another way to characterize this limited use of qpfst is to observe that in such cases every cyclic path through such a transducer will have identical input and output queue: the queue is only used in a strictly local sense.

The ordinary transducer determinization algorithm is guaranteed to terminate
only if the input transducer can be determined, i.e., the transducer
must be * sub-sequential*. A separate algorithm exists to check a
given transducer for subsequentiality (section 5.2).
The same termination property
holds for the generalized transducer determinization algorithm. If
the generalized transducer determinization algorithm terminates for a
given pfst, then the result is an equivalent deterministic qpfst. The
application of a determinized (potentially non-functional) qpfst *T*
to a given string *w* is linear in the size of *w*, and independent of
the size of *T*.