PostImage

For any transducer $$T = (Q_T, \Sigma, \delta_T, q_{0, T}, F_T)$$ and FA $$A = (Q_A, \Sigma, \delta_A, q_{0, A}, F_A)$$, we can construct a FA $$B = (Q_B, \Sigma, \delta_B, q_{0, B}, F_B)$$ which satisfies $$L (B) =\operatorname{Post}_T (A)$$ as follows:

$$Q_B = (Q_T \times Q_A) \cup S$$, where S contains all the fresh intermediate states which are introduced below.

The initial state $$q_{0, B}$$ is $$(q_{0, T}, q_{0, A})$$, and $$F_B$$ contains states of the form $$(q_T, q_A)$$ which satisfies $$q_T \in F_T \wedge q_A \in F_A$$.

For any tuple $$(q_T, a, w, q_T') \in \delta_T$$, and any $$(q_A, a, q_A') \in \delta_A$$:

Suppose $$w = \sigma_1 \ldots \sigma_n$$, then we add $$n - 1$$ fresh states to $$Q_B$$, which we label by $$q_1, \ldots, q_{n - 1}$$. Then we have:

• $$((q_T, q_A), \sigma_1, q_1) \in \delta_B$$

• $$(q_1, \sigma_2, q_2) \in \delta_B$$

• ...

• $$(q_{n - 1}, \sigma_n, (q_T', q_A')) \in \delta_B$$

Note that the input 'a' is not used in the construction, but it is crucial that the transitions in T and A have the same input character.