Take the 2-minute tour ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

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?

share|improve this question
    
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
3  
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
1  
@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
show 8 more comments

2 Answers

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

share|improve this answer
1  
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
add comment

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.

share|improve this answer
    
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
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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