5
$\begingroup$

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.]

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

1 Answer 1

Reset to default
3
$\begingroup$

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

https://www7.in.tum.de/~sickert/projects/ltl2dra/

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Another tool is www7.in.tum.de/~kretinsk/rabinizer3.html It is by the same authors. The page also contains many links to the papers on which the tool is based. $\endgroup$
    – Ayrat
    Commented Dec 30, 2016 at 16:11

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.