I am trying to construct an equivalent Deterministic Rabin Automata (DRA) given a Linear Temporal Logic (LTL) Formula. One (expensive) way to do this would be to construct an equivalent Non-deterministic Buchi Automata and then determinize it using Safra's construction.

I am interested to know whether there exist efficient algorithms which can 1. Directly construct DRA from LTL without intermediate NBA construction. 2. Are there any existing tools to do this.

[This is my first question posted here. Kindly point in comment, if I missed any conventions of the forum. Thank you.]

  • $\begingroup$ Searching for "ltl to rabin automata" in Google gives me several results, including this: ltl2dstar.de $\endgroup$
    – xavierm02
    Dec 30 '16 at 0:36
  • $\begingroup$ @xavierm02 ltl2dstar takes the indirect way though NBAs, which the OP is trying to avoid. $\endgroup$
    – DCTLib
    Dec 30 '16 at 14:16

There is a very recent tool to translate from LTL directly to deterministic Rabin automata. It can be obtained here:


The page not only contains a link to the downloadable implementation, but also has link to a technical report that describes the construction for the translation. Apparently, a peer-reviewed paper about the construction has not appeared yet. Note that the construction is rather involved - the paper has 50 pages, and there is a reason why for many years, the detour though Büchi automata was (and somewhat still is) state-of-the-art.

Note that the computational complexity of the direct translation is not better than the one that one can obtain by translating LTL to non-det. Büchi automata and then applying Safra's method.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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