Given a Büchi automaton what is the procedure to build an equivalent LTL formula? And what is its size?
I'm looking for references but I haven't found them so far.
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
2
Since Büchi automata are strictly more expressive than LTL, such a translation is not possible in the general case.
For instance, the language $L = \{w_0 w_1 w_2 \ldots \in (2^{\{a\}})^\omega \mid \exists^\infty i \in \mathbb{N}. w_{2i} = \{a\} \}$ is representable by a Büchi automaton with 3 states, but is not expressible in LTL as it is a counting language.
-
$\begingroup$ Do you know how to translate a counter-free Buchi automaton in LTL ? I am moslty interested in it. $\endgroup$– kafkaCommented Oct 2, 2019 at 5:22
-
1$\begingroup$ @kafka There is an answer for that case on mathoverflow: mathoverflow.net/questions/96963/… $\endgroup$– DCTLibCommented Oct 2, 2019 at 6:37