<p>Françoise Gire actually gives two proofs of her result. </p>

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

<p>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].</p>

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

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

CC BY-SA 3.0
2015-09-02T17:31:08.683Z
2015-09-02T17:31:08.683Z
J.-E. Pin
<p>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. </p>

<p>$\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) \,\,,$</p>

<p>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.</p>

<p><a href="https://www.react.uni-saarland.de/publications/CFKMRS14.html" rel="nofollow">https://www.react.uni-saarland.de/publications/CFKMRS14.html</a></p>

CC BY-SA 3.0
2015-09-05T19:34:58.003Z
2015-09-05T19:41:15.853Z
2015-09-05T19:41:15.853Z
Markus
<p>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: <a href="http://www.sciencedirect.com/science/article/pii/002001908690058X">Two Decidability Problems for Infinite Words</a>. 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.</p>

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

CC BY-SA 3.0
2015-09-02T16:14:00.877Z
Hi can you send me and email zitterbewegung@gmail.com
Joshua Herman
<ds.algorithms><reference-request><automata-theory>
Deciding functionality of transducers over infinite words
aer0dynamic
# Deciding functionality of transducers over infinite words

(Asked by: username_0 on 2015-09-02)

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](http://www.sciencedirect.com/science/article/pii/002001908690058X). 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?

**Tags:** ds.algorithms, reference-request, automata-theory
> **Comments:**
> **username_1**: Hi can you send me and email zitterbewegung@gmail.com  

---

## 2 answers

### Answer by username_2 on 2015-09-02. Score: 7 | Accepted answer

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 by username_3 on 2015-09-05. Score: 0

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>


---

