Re: [Spot] Parameters for the "ltl2tgba" tool

Hi Ruediger, e> Dear all, e> included in the SPOT distribution is the tool "ltl2tgba" that converts LTL e> formulas to equivalent Büchi automata. For the research I am currently e> working on, I need to convert LTL formulas to as-small-as-possible Büchi e> automata (that are not transition-based, so I am using the tool with the e> "-N" parameter to obtain SPIN never-claims). So far, for all my e> benchmarks, I am calling the tool with the following parameter e> combinations: e> ltl2tgba -N -R3 -r4 e> ltl2tgba -N -R3 -r7 e> ltl2tgba -N -R3 -r4 e> ltl2tgba -N -R3 -r7 e> ltl2tgba -N -R3 -r4 e> ltl2tgba -N -R3 -r7 I presume you forgot to edit some of these lines? From the rest of your mail, you might be using -R2q and -R2t also. Have you seen cases where -r4 produces a smaller automaton than -r7 ? I would think that given that -r7 includes -r4 it should always be better. Of course these options only try to reduce the LTL formulae, not the resulting automata. However if you see cases where -r7 reduces the formula in a way that the translated automaton is bigger than one obtained after -r4, I would be interested to study them. e> After that, I take the smallest automata obtained. So far, I am only e> interested in the number of states. e> Now my question is: Given that I have enough time, which other parameter e> combinations might lead to automata that that are smaller than any e> automaton obtained when using the parameter combinations given above? As e> an example, can it be the case that "-R2q" is sometimes better than "-R3"? These switches are not exclusive. I would always use -R3, because removing dead states and useless acceptance conditions (-R3 does that) will improve the efficiency of other algorithms such as delayed simulations. You could try the following combinations ltl2tgba -f -N -R3 -R1q -R1t -r7 ltl2tgba -f -N -R3 -R2q -R2t -r7 ltl2tgba -f -N -R3 -R1q -R1t -R2q -R2t -r7 But I think the latter should always return the smaller automaton (when it is correct...). Unfortunately these -R1* and -R2* options are not always correct (this is the reason they are not available on the on-line translator script). They were implemented by a student during his master's thesis, but he struggled to adapt Etessami's paper to transition-based automata. I know of an easy case where the -R2* simplification is clearly wrong: ./ltl2tgba -f -R3 -R2t 'FG a' Apparently the structure of the automata generated by the "-f" translation is such that -R2* can be wrong only when it is mixed with -R3. But the bug really is in -R2*. I'm a bit more confident about -R1* for which I'm not aware of any problem (except that it does not work for generalized automata, but that should not be an issue for you). Still, personally I would only use -R3. Rewriting -R1* and -R2* has been on the TODO list for a while. I have seen some work, by Juvekar and Piterman, that generalizes the technique to generalized Büchi automata: it would probably be a better fit for Spot. So to summarize, I think you should be safe with ltl2tgba -f -N -R3 -R1q -R1t -r7 and I suggest you use -R2* only if you can check that the resulting automaton is correct. Although I think "-f" will create less states than the other translations, you can also try to replace it by one of -f -f -x -f -x -p -f -L -f -L -x -f -L -x -p -l -taa -c (If you encounter a case where -l or -taa is better than -f, please let me know!) -- Alexandre Duret-Lutz