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.]
Efficient Algorithm Linear Temporal Logic to Deterministic Rabin Automata
formal languages;formal methods;buchi automata
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 Bchi 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. Bchi automata and then applying Safra's method.