33
$\begingroup$

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?

Improve this question
$\endgroup$
13
  • $\begingroup$ 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? $\endgroup$
    – Raphael
    Mar 7, 2012 at 22:11
  • $\begingroup$ @Raphael unfortunately, I don't know much about MSO $\endgroup$
    – Daniil
    Mar 8, 2012 at 7:12
  • 3
    $\begingroup$ 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. $\endgroup$
    – Janoma
    Mar 8, 2012 at 13:14
  • $\begingroup$ REG, DFA and NFA correspond to WMSO, not MSO. $\endgroup$
    – Raphael
    Mar 8, 2012 at 18:06
  • 1
    $\begingroup$ @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. $\endgroup$
    – Daniil
    Mar 18, 2012 at 20:55

2 Answers 2

Reset to default
18
$\begingroup$

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

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ Is there a result for the OP's question in these references, or is it open? $\endgroup$
    – Raphael
    Apr 7, 2012 at 12:20
  • $\begingroup$ I have clarified my answer. $\endgroup$
    – Vijay D
    Apr 7, 2012 at 19:23
3
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Your answer doesn't seem to be complete. $\endgroup$
    – Dave Clarke
    Apr 1, 2012 at 7:06
  • $\begingroup$ @Dave, yes, it isn't. $\endgroup$
    – Kaveh
    Apr 1, 2012 at 7:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.