# 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, 2012 at 22:11
• @Raphael unfortunately, I don't know much about MSO Mar 8, 2012 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. Mar 8, 2012 at 13:14
• REG, DFA and NFA correspond to WMSO, not MSO.
– Raphael
Mar 8, 2012 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. Mar 18, 2012 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, 2012 at 12:20
• I have clarified my answer. Apr 7, 2012 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. Apr 1, 2012 at 7:06
• @Dave, yes, it isn't. Apr 1, 2012 at 7:56