Dear all, included in the SPOT distribution is the tool "ltl2tgba" that converts LTL formulas to equivalent Büchi automata. For the research I am currently working on, I need to convert LTL formulas to as-small-as-possible Büchi automata (that are not transition-based, so I am using the tool with the "-N" parameter to obtain SPIN never-claims). So far, for all my benchmarks, I am calling the tool with the following parameter combinations: ltl2tgba -N -R3 -r4 ltl2tgba -N -R3 -r7 ltl2tgba -N -R3 -r4 ltl2tgba -N -R3 -r7 ltl2tgba -N -R3 -r4 ltl2tgba -N -R3 -r7 After that, I take the smallest automata obtained. So far, I am only interested in the number of states. Now my question is: Given that I have enough time, which other parameter combinations might lead to automata that that are smaller than any automaton obtained when using the parameter combinations given above? As an example, can it be the case that "-R2q" is sometimes better than "-R3"? Phrased in other words, I'd like to know some set of parameter combinations "A" such that for all LTL formulas "f", I can simply run "ltl2tgba" on "f" trying all parameters combinations in "A" and take the minimal automaton found. For the resulting automaton, it should be assured that there's no smaller automaton obtainable with "ltl2tgba" from "f" for any possible parameter combination. At the same time, "A" should be as small as possible. I hope that someone finds some time to reply and apologies for using the SPOT framework in such a restricted way. Best regards, Ruediger Ehlers