Spot issueshttps://gitlab.lre.epita.fr/spot/spot/-/issues2021-05-03T09:57:34+02:00https://gitlab.lre.epita.fr/spot/spot/-/issues/460missed LTL simplification2021-05-03T09:57:34+02:00Alexandre Duret-Lutzmissed LTL simplificationFor 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.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.lre.epita.fr/spot/spot/-/issues/385ltl2tgba -G cases that can be improved2020-07-22T21:33:58+02:00Alexandre Duret-Lutzltl2tgba -G cases that can be improvedOn 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
> `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.lre.epita.fr/spot/spot/-/issues/12even more LTL simplification for GF formulas2017-11-15T14:34:27+01:00Alexandre Duret-Lutzeven more LTL simplification for GF formulaswe could implement those rules:
```
GF(a & Fb) = G(Fa & Fb)
GF(a & XXXXXFb) = G(Fa & Fb)
GF(a & eventual) = G(Fa & 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.lre.epita.fr/spot/spot/-/issues/11more LTL simplifications for GF formulas2017-11-15T14:34:27+01:00Alexandre Duret-Lutzmore LTL simplifications for GF formulas`(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` 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.lre.epita.fr/spot/spot/-/issues/2find a way to reduce {b*;r} = (b W r) when r is satisfiable2017-11-15T14:34:27+01:00Alexandre Duret-Lutzfind a way to reduce {b*;r} = (b W r) when r is satisfiableCommit 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.