2
$\begingroup$

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)

Improve this question
$\endgroup$

1 Answer 1

Reset to default
0
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • $\begingroup$ yes, we can.. But do you mean that there is no "size" benefit in using non-det Rabin automata over non-det Buchi automata for LTL formulas? (i.e., for any LTL formula, the size of minimal non-det Rabin automaton equals to the size of minimal non-det Buchi?) (where size is the number of states) $\endgroup$
    – Ayrat
    Jan 12, 2017 at 19:30
  • 1
    $\begingroup$ It is true that Rabin automata may be more succinct than Buchi automata, even for nondeterministic ones. However, the lower bound in the blowup is the same. In addition, I don't think there is a translation from LTL to non-det Rabin that will give you significantly smaller automata (no more than a polynomial factor, I think). $\endgroup$
    – Shaull
    Jan 12, 2017 at 22:42
  • $\begingroup$ @Ayrat I am not sure whether the tool called GOAL satisfies the OP's requirement. (Personally, I think it is a very wonderful tool with a long-term goal "to handle all the common variants of omega-automata and the logics that are expressively equivalent to these automata". ) $\endgroup$
    – hengxin
    Apr 12, 2017 at 3:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.