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