Are there any LTL to _non_ deterministic Rabin automaton translators? I know of two translators LTL -> deterministic Rabin automaton:


Rabinizer3
ltl2dstar


They produce deterministic automata, which can be much larger than their possible non-deterministic variants. Is there a translator LTL -> non deterministic Rabin?

(my synthesis tool could handle small non-det Rabin automata but not large though det ones)
You can easily translate LTL to non-deterministic Buchi automata, which can be thought of as a simple fragment of Rabin automata (although they are equally expressive).
I don't think any tool would actually output the acceptance condition described as a Rabin condition, but this is very easy to deduce from the Buchi states.

An example of an online tool to do this conversion is:
http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/

But I'm sure there are many others, as the construction is relatively simple.