Deciding functionality of transducers over infinite words 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?
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.