How to get $\omega$-regular expression from buchi automaton Is there an algorithm or a trick on how to get $\omega$-regular expressions from Buchi automatons? If yes, is there also some way to do create minimal such regular expressions?
It is extremely difficult for me to recognise the general struture of such automata and to formalize them in a synthetic way.
For example take this automata: 
Buchi automaton
The $\omega$-regular expression I came up with was: $b^*a(a^\omega+(a^*b^+a)^\omega)$.
The minimised solution someone else found, was this: $(b^*a)^\omega$.
PS: should I post this in the mathematics and/or theoretical computer science forum and/or computer science, too?
 A: A Büchi automaton is a finite automaton that one runs on
infinitely long strings (length $\omega$), with the proviso that
the string is accepted if infinitely often the machine had
visited an accepting state.
In your example, which I picture here, it is clear that the
accepted strings are exactly described by $(b^*a)^\omega$, because
a string will be accepted just in case any $b$ occurring in it is
eventually followed by an $a$.

In general, for a Büchi machine with just one accepting
state, then the way I think about it is this. In order for a string to be accepted, it must first get from the start state to the accepting state for the first time, and then it must get from that accepting state back again to that accepting state again, infinitely many times. This simple idea tells you how to find the $\omega$-regular expression for the accepted strings. Namely, let $\tau$ be a regular expression for
getting from the start state to that accepting state, and let $\sigma$ be a regular expression for getting from the accepting
state back to the accepting state with a nonempty string. Putting them together, the accepted strings for the Büchi machine will be
described by $\tau\sigma^\omega$. One follows $\tau$ to get to the accepting state, and then follows $\sigma$ infinitely many times in order to revisit it sufficiently. 
If there is more than one accepting state, then a similar idea
will work, simply by adding those expressions together, since for one of the accepting states (by pigeonhole), one must first get there and then revisit it $\omega$ many times.
