Question

I know of two translators LTL -> deterministic Rabin automaton:

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)

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top