Spot issues https://gitlab.lrde.epita.fr/spot/spot/-/issues 2021-05-03T09:57:34+02:00 https://gitlab.lrde.epita.fr/spot/spot/-/issues/460 missed LTL simplification 2021-05-03T09:57:34+02:00 Alexandre Duret-Lutz missed LTL simplification For any φ we have that `F(Fp0 &amp; (p0 | φ))` is equivalent to `F(p0)`. Can we generalize and recognize this pattern? This is based on a mail by @ythierry. For any φ we have that `F(Fp0 & (p0 | φ))` is equivalent to `F(p0)`. Can we generalize and recognize this pattern? This is based on a mail by @ythierry. https://gitlab.lrde.epita.fr/spot/spot/-/issues/385 ltl2tgba -G cases that can be improved 2020-07-22T21:33:58+02:00 Alexandre Duret-Lutz ltl2tgba -G cases that can be improved On Sun, Apr 21, 2019 at 9:46 PM Juraj Major &lt;major@fi.muni.cz&gt; wrote: &gt; &gt; Hi Alexandre, &gt; &gt; Jan asked me to send you some formulae from LTL(F,G,X) where Delag &gt; produces smaller automata than ltl2tgba. I use Spot 2.7.3 and call &gt; `ltl2tg... On Sun, Apr 21, 2019 at 9:46 PM Juraj Major <major@fi.muni.cz> wrote: > > Hi Alexandre, > > 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)<br/> > 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) <br/> > 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. https://gitlab.lrde.epita.fr/spot/spot/-/issues/12 even more LTL simplification for GF formulas 2017-11-15T14:34:27+01:00 Alexandre Duret-Lutz even more LTL simplification for GF formulas we could implement those rules: ``` GF(a &amp; Fb) = G(Fa &amp; Fb) GF(a &amp; XXXXXFb) = G(Fa &amp; Fb) GF(a &amp; eventual) = G(Fa &amp; eventual) ``` we could implement those rules: ``` GF(a & Fb) = G(Fa & Fb) GF(a & XXXXXFb) = G(Fa & Fb) GF(a & eventual) = G(Fa & eventual) ``` https://gitlab.lrde.epita.fr/spot/spot/-/issues/11 more LTL simplifications for GF formulas 2017-11-15T14:34:27+01:00 Alexandre Duret-Lutz more LTL simplifications for GF formulas `(GF(a)&amp;GF(b)) | (GF(c)&amp;GF(d))` is equivalent to `(GF(a|c) &amp; GF(a|d) &amp; GF(b|c) &amp; GF (b|d))`. It&#39;s a bigger formula, but it can be translated into a one-state automaton. &gt; Jan Strejcek: &gt;&gt; ADL: &gt;&gt; we like to simplify `GFa | GFb` a... `(GF(a)&GF(b)) | (GF(c)&GF(d))` is equivalent to `(GF(a|c) & GF(a|d) & GF(b|c) & GF (b|d))`. It's a bigger formula, but it can be translated into a one-state automaton. > Jan Strejcek: >> ADL: >> we like to simplify `GFa | GFb` as >> `GF(a|b)` because `GF(a|b)` is easily translated as a deterministic >> automaton. In the same way, `(GFa & GFb) | (GFc & GFd)`, which is >> currently translated as a non-deterministic automaton, could be >> rewritten as `GF(a|c) & GF(a|d) & GF(b|c) & GF(b|d)` which will be >> translated as a deterministic automaton. Can this kind of rewriting >> be generalized? > > I think I can provide a (partial) answer. The only > non-obvious rule we have to add is the following: > > for pure eventually formulae m1,m2 (roughly speaking, the formulae starting > with F), the following > equivalence holds: G m1 | G m2 <=> G (m1|m2) > > With this rule and the standard rules > > G f1 & G f2 <=> G (f1&f2) > distributivity: (A&B) | (C&D) <=> (A|C) & (A|D) & (B|C) & (B|D) > or simply A | (C&D) <=> (A|C) & (A|D) applied twice > F f1 | F f2 <=> F (f1|f2) > > one can transform `(GFa & GFb) | (GFc & GFd)` into `G( F(a|c) & F(a|d) & F(b|c) & F(b|d))`, > which is enough to get determinstic automaton. A more interesting > question may be "How to detect the situation when such rules should be > applied". This especially applies to the distributivity as all other rules > simply replace two modalities with one, which has usually positive effect on > the translation and therefore the rules should be applied by default. I can > imagine that distributivity will be applied only with `--deter` option and > only to propagate disjunction downwards the syntactic tree (as disjunction > is often a source of nondeterminism). > Jan: >> ADL: >> It isn't as straightforward as it seems. For instance >> adding only the `G(e1)|G(e2) = G(e1|e2)` without distribution >> can be a serious regression: >> >> `G(Fa & Fb) | G(Fc & Fd)`: 3 states >> `G((Fa & Fb) | (Fc & Fd))`: 15 states >> `G(F(a | c) & F(a | d) & F(b | c) & F(b | d))`: 1 state >> >> I think for this to work we have to guarantee that all pure >> eventualities will be rewritten as F(something). > > I guess that you want to say that each pure eventuality formula can be > rewritten into a conjunction of F(something) formulae. I'm afraid this > doesn't hold. For example, `GFa R Fb` is a pure eventuality formula > equivalent to `GFa | GFb`... Hmm, but there is no problem in this > particular case. I have to think about it with a fresh mind. https://gitlab.lrde.epita.fr/spot/spot/-/issues/2 find a way to reduce {b*;r} = (b W r) when r is satisfiable 2017-11-15T14:34:27+01:00 Alexandre Duret-Lutz find a way to reduce {b*;r} = (b W r) when r is satisfiable Commit 11568666 removed the following rules {b*;r} = b W r !{b*;r} = !b M !{r} because it is only true when `r` is satisifiable, but the code did not check that. Currently the only way we have to ensure that `r` is sa... Commit 11568666 removed the following rules {b*;r} = b W r !{b*;r} = !b M !{r} because it is only true when `r` is satisifiable, but the code did not check that. Currently the only way we have to ensure that `r` is satisifiable is to translate it into an automaton. Doing so seems unlikely to be efficient. But there are many formulas that we can tell as satisfiable without even translation: for instance any SERE that do not involve `&`, `&&`, and `false` is satisfiable. So maybe each formula could have a Boolean property that tells when it is trivially satisfiable.