Given a finite state transducer defining a rational relation over infinite words, it is known to be decidable whether or not the relation is a function, i.e. whether each infinite input word is related to at most one infinite output word. This is detailed in a paper by Gire: Two Decidability Problems for Infinite Words. Unfortunately, I cannot find the full text of the paper anywhere. The basic idea seems to be to form the composition of the transducer with its inverse $T \circ T^{-1}$ and check if the resulting transducer is a restriction of the identity function. Note that the inverse of a transducer $T$ is $T$ with input and output word swapped for each transition.

I am looking for details of the decision procedure. Do you have any references or a short description of the algorithm?


2 Answers 2


Françoise Gire actually gives two proofs of her result.

The first proof (I am quoting her paper now) uses a construction similar to the one used in [3] to prove the decidability of the $\omega$-equivalence of two functional finite transducers.

The second proof makes use of the technique you are describing in your question: $T$ is functional if and only if $T \circ T^{-1}$ is a restriction of the identity. The property for an infinitary rational relation of being a restriction of the identity is proved to be decidable in [3,4].

[3] K. Culik and J. Pachl, Equivalence problems for mappings on infinite strings, Inform. and Control 49 (1981) 52-63.

[4] K. Culik, Some decidable results about regular and pushdown translations, Inform. Process. Lett. 8 (1979) 5-8.


The works in the previous answer only seem to establish the decidability, but not the exact complexity. So I see a chance to blatantly advertise my own work here: You could formulate the property in HyperLTL: All pairs of words with the same input sequence must have the same output sequence.

$\forall\pi.\forall\pi'. \square\left(\bigwedge_{i} i_\pi\leftrightarrow i_{\pi'} \right)\implies \square\left(\bigwedge_o o_\pi \leftrightarrow o_{\pi'}\right) \,\,,$

where $i$ and $o$ are the input and output propositions, respectively. As the formula is in the alternation-free fragment you can check it in NLOGSPACE in the size of the transducer.



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.