# 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).