Hi Ruediger,
>>> "e" == ehlers <ehlers(a)alan.cs.uni-sb.de> writes:
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
