ltl2tgba -G cases that can be improved
On Sun, Apr 21, 2019 at 9:46 PM Juraj Major email@example.com wrote:
Jan asked me to send you some formulae from LTL(F,G,X) where Delag produces smaller automata than ltl2tgba. I use Spot 2.7.3 and call
ltl2tgba -G 'formula'.
GFX((e & XXXa) -> (e & X!d)) (ltl2tgba 2 states vs. Delag 1 state)
G(Gc | Fa | F!G(c | Ge)) (6 vs. 3)
These looks like cases where Spot is simply not applying rewritings like GF(a | b) = GF(a)|GF(b). Those rules would make sense for -G, but they usually don't make sense when building other types of automata, so I haven't worked on those yet. It's unfortunate that the rewriting rules in Spot is not very modular.
Ge | XGF(Ge & X(c & Fd)) (5 vs. 2)
G!GXXe -> GF(b & c & Gc) - this one is interesting, because ltl2tgba -DG produces smaller automaton (2 states) then ltl2tgba -G (3 states). However, Delag still wins with 1 state
These are cases where Spot is missing the rule GF(a & Gb) = GFa & FGb
Because GF(b & c & Gc) is not a GF(guarantee), it's determinized via Safra if -D is given, and this is not tried without -D. The non-deterministic automaton output by -G for GF(b & c & Gc) is a 2-state incomplete automaton and deterministic automaton from -G -D is a 2-state complete automaton, so the incompleteness is what makes the difference during the product, as you need complete automata to make a disjunction.
G!(Gd & (c | Fb)) (4 vs. 2)
Running delag with "-f ltl2tgba" will output the same automaton as ltl2tgba, so this is a case where the fallback translator used by delag (I'm not sure what that is) does a better job. In their paper, they used Spot as fallback I think, but it seems they are now using something else.
The tool ltl2da, distributed with Owl, also produces a 2-state (but nicer IMHO) TELA for this.
XF(F(Gc & Xb) -> a) (6 vs. 3)
Again we are missing whatever rule needed to reduce this to:
GF(!c) | FG(!b) | XF(a)
(in which case its 3 states if deterministic or 2 if non-deterministic)
From the genltl's patterns, there's a --sejk-f pattern where Delag performs better than Spot but those are not LTL(F,G,X) formulae.
I'm not sure how that one works. Look like some kind of suspension would be useful.
So it seems a large part of these issues would be solved by LTL rewritings.