Equivalence of Büchi automata and linear $\mu$-calculus

It's a known fact that every LTL formula can be expressed by a Büchi $\omega$-automaton. But, apparently, Büchi automata are a more powerful, expressive model. I've heard somewhere that Büchi automata are equivalent to linear-time $\mu$-calculus (that is, $\mu$-calculus with usual fixpoints and only one temporal operator: $\mathbf{X}$).

Is there an algorithm (constructive proof) of this equality?

• I do not know too much about logics. NBA are equivalent to MSO, afaik; do you know something about the relation of MSO and your logic? – Raphael Mar 7 '12 at 22:11
• @Raphael unfortunately, I don't know much about MSO – Daniil Mar 8 '12 at 7:12
• Note that regular languages, DFA, NFA and NBA are equivalent over MSO over strings, but not "equivalent" to MSO in a general sense (over arbitrary structures). Actually, second-order logic (SO), when considered over strings, is also equivalent to monadic second-order logic (MSO), but SO in general is much more expressive than LTL. – Janoma Mar 8 '12 at 13:14
• REG, DFA and NFA correspond to WMSO, not MSO. – Raphael Mar 8 '12 at 18:06
• @Raphael hal.archives-ouvertes.fr/docs/00/06/06/08/PDF/LogicOnWords.pdf - this article was a good starting point for me, although I myself is no expert and have yet to fully understand the algebraic and automata methods for $\omega$-languages. – Daniil Mar 18 '12 at 20:55

The constructive equivalence of linear-time fixed point formulae (the logic is called $\nu$TL by some) and Buechi automata is given in a paper by Mads Dam from 1992.

Fixed Points of Buchi Automata, FST&TCS 1992.

See page 4 for the construction of a $\nu$TL formula from a Buechi automaton. The construction of a Buechi automaton from a $\nu$TL formula is more complicated and takes the rest of the paper.

The rest of this reply is a brief argument that this result existed in the literature in far less direct form. Pierre Wolper showed that there were omega-regular properties that were not LTL-definable and gave an extension of LTL (called ETL) that could express omega-regular properties.

Temporal Logic can be more expressive, Pierre Wolper, Information and Computation, 1983.

It is also known that one can translate ETL formulae into $\nu$TL formulae, so by combining these results you can read off a translation of Buechi automata into $\nu$TL. In the other direction, it follows from the work of Buechi that S1S (the second order theory of one successor) formulae can be compiled into Buechi automata and by translating $\nu$TL formulae into S1S, we obtain a translation of $\nu$TL to Buechi automata. If you want a more in-depth introduction to these topics, I suggest Mads Dam's lecture notes, or the work of Roope Kaivola (sadly not as widely known as much related work).

Temporal Logics, Automata, and Classical Theories - An Introduction, Mads Dam, ESSLLI 1994.

Using Automata to Characterise Fixed Point Temporal Logics, Roope Kaivola

• Is there a result for the OP's question in these references, or is it open? – Raphael Apr 7 '12 at 12:20
• I have clarified my answer. – Vijay D Apr 7 '12 at 19:23

IIRC, there was a similar problem in Moshe Vardi's talk at the Fields Institute (it wasn't about $\mu$-calculus though).

You may want to check the slides or check Vardi's papers. There is definitely an algorithm but IIRC the negations cause a huge increase in the time required to perform the translation.

• Your answer doesn't seem to be complete. – Dave Clarke Apr 1 '12 at 7:06
• @Dave, yes, it isn't. – Kaveh Apr 1 '12 at 7:56