Deciding functionality of transducers over infinite words

Question

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?

Answer 1

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.

Answer 2

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.

https://www.react.uni-saarland.de/publications/CFKMRS14.html