Hi Ruijie, Meng Ruijie <ruijie_meng@u.nus.edu> writes:
During constructing Buchi automata for LTL, Spot always shows non-determinism automata although I select the "deterministic" item.
"deterministic" only expresses a *preference*: in case the translator can make a choice between a smaller non-deterministic or a larger automata, it will honor your preference. But for Büchi/Generalized Büchi output this option does ensure that a deterministic automaton will be output when one exists.
Would you mind telling me how to construct deterministic automata with Spot? Here is one LTL: !(false R (iusr2_ai3_re13 & (! X (true U iusr2_ai3_re14) | X (true U (iusr2_ai3_re14 & (true U ousr2_ai3_ce8)))))). The following is its automata but non-determinism.
If you use the "study" tab of the online application, you can see that this formula belongs to the "Persistence" class, which means that no deterministic Büchi automaton exist for this particular formula. See https://spot.lrde.epita.fr/hierarchy.html for more documentation about the classes. In particular, the section about the Recurrence class (where deterministic Büchi automata always exist) shows a case where the translator produce a non-deterministic Büchi automaton even with -D, and how to work around that.