Hi Alexandre,
I've just tried to use the development version at https://spot-dev.lrde.epita.fr/app/ and fed it the following formula (which is ugly but simple, just {SERE} |-> bool), and it died of "500 Internal Server Error".
{(((((((!"a")##1(!"b"))##0("c" <-> "d"))##0("e" xor "f"))##0(((((("g" & "h") xor "i") <-> "j") | "k") & "l") | "m"))##0(("n" & "o") | (!"n" & "p")))##0("q" -> ("r" <-> "s")))##[0:1]"t"} |-> "u"
Regards,
Victor.
Hi Alexandre,
I've now worked out the proofs for the ## operator - there were a few (nice) surprises. To summarise, ##[i:j] is SI if both operands are SI, j is in {0,1,$}, and either:
* i=0, or
* i=1 and a is prefix-closed OR b is suffix-closed, or
* i=2 and a is prefix-closed AND b is suffix-closed.
Note that ##[0:1] does not need prefix/suffix-closedness as K:L catches some of the un-stuttered words from K;L, and similarly for ##[0:$]. These operators mix fusion with concatenation in a confusing way. Similarly, ##[2:$] was somewhat unexpected but nice :-) - I had expected only 0,1,$ to be allowed.
Concerning the |=>, I hope we can lift the prefix/suffix-closedness idea to omega-languages and handle it. I also hope this will handle some cases of X, which would be really nice. E.g.: {a[+]} |=> Fx is si, and for the same reason {a[+]}|->XFx is si.
Regards,
Victor.
Hi Alexandre,
I've reconsidered first_match, apparently my suggestion to eliminate the exit arcs of the accepting states in the NFA is wrong, e.g. for (a|a;a) the NFA has two accepting states with no exit arcs and the transformation does not have any effect, whereas first_match(a|a;a)=a. I guess the automaton has to be determinised before applying this transformation (unless you have a better idea).
Regards,
Victor.
> -----Original Message-----
> From: Alexandre Duret-Lutz <adl(a)lrde.epita.fr>
> Sent: Tuesday, May 7, 2019 3:15 PM
> To: Victor Khomenko <victor.khomenko(a)newcastle.ac.uk>
> Cc: spot <spot(a)lrde.epita.fr>
> Subject: Re: [Spot] syntactic stutter-invariance
>
> On Tue, May 7, 2019 at 10:41 AM Victor Khomenko
> <victor.khomenko(a)newcastle.ac.uk> wrote:
> > I have machine proofs for most of these, including the proof that K;L is si
> if both K and L are si and either K is prefix-closed or L is suffix-closed.
>
> Interesting.
>
> >> a ##[i:j] b = a:([*i:j];b)
> > Do you know whether A:(B;C)=(A:B);C ? I'd guess yes, but have no proof
> yet.
>
> That would not work when B=[*0], because A:[*0] = false. However if you
> assume that B has at least one letter, I believe that works.
>
> In the case of "a ##[i:j] b" if i>0 Spot actually rewrite this as "a;[*i-1:j-1];b"
> without using ":".
>
> > I'd add:
> > first_match(L+)= first_match(L) [* is already handled by your rules]
>
> So the general case is first_match(L[*i:j]) = first_match(L[*i]).
> And if L is boolean, this becomes just L[*i].
>
> > first_match(K;L)= first_match(K) if the empty word is in L
> > first_match(K;L)= K;first_match(L) [correct?? It would then
> > imply the above rule]
>
> That last rule doesn't look right to me.
>
> first_match(a[*];b[*]) = [*0]
> a[*];first_match(b[*]) = a[*]
>
> Maybe that rule works if all words accepted by K have the same length.
> (So for an easier rule, if K is Boolean).
>
> So to summarize, assuming b is Boolean, e accepts empty words, and f, and
> g are anything else:
> first_match(b[*i..j]) = b[*i]
> first_match(f[*i..j]) = first_match(f[*i])
> first_match(b;f) = b;first_match(f)
> first_match(f;g[*i..j]) = first_match(f;g[*i])
> first_match(f;e) = first_match(f)
> It's not clear that any of those is going to improve the output
> --
> Alexandre Duret-Lutz
Hi Alexandre,
> Can we detect prefix- or suffix-closure syntactically?
Not sure about omega-languages, but for the "usual" ones the prefix- and suffix-closed languages are closed wrt. | && ; + * at least (and so the derived operations). Not sure about ":", but hope so. Definitely not closed wrt. complement (prefix- and suffix-closed languages always contain the empty word, which is not in the complement). I hope these can be generalized to suffix-closed omega languages.
I have machine proofs for most of these, including the proof that K;L is si if both K and L are si and either K is prefix-closed or L is suffix-closed.
> Meanwhile, I have implemented SVA's first_match and ##[i:j].
Excellent news!
> a ##[i:j] b = a:([*i:j];b)
Do you know whether A:(B;C)=(A:B);C ? I'd guess yes, but have no proof yet. Generally, what properties does ":" have?
> The former is a new operator, with three automatic simplifications:
> first_match(b) = b if b is Boolean,
> first_match(first_match(r)) = first_match(r),
> first_match(r) = [*0] if r accepts the empty word.
> (this last rule makes the translation to automata works almost
> automatically)
I'd add:
first_match(L+)= first_match(L) [* is already handled by your rules]
first_match(K;L)= first_match(K) if the empty word is in L
first_match(K;L)= K;first_match(L) [correct?? It would then imply the above rule]
Regards,
Victor.
Hi Alexandre,
> However now that you have written this down, I think your interpretation r
> SSI => r[+] SSI and r[*] SSI is also sound, but I have no proof for this.
I tried to prove this, but failed, and then found a counterexample: e.g. if L = a[+];(!a)[+];a[+], then L is si but both L[+] and L[*] are not si. I believe if one in addition requires that L is prefix-closed or suffix-closed, then the result would hold (I have an idea how to prove this).
> > > I would suggest that at the SERE level the rule for the n-ary
> concatenation
> > > r1;r2;r3;...;rn
> > > could be extended so that the entire concatenation is SSI iff each
> > > ri is SSI and at most one of them rejects the empty word.
Again, this seems wrong, with the following counterexample:
If K=[*0] | ((!a)[+] ; a[+]) and L=a[+] then K contains the empty word, K and L are si, but K;L is not si: it accepts !a;a;a but rejects !a;a.
I think the result would hold if one replaces the assumption that K or L contains the empty word by K being prefix-closed or L being suffix-closed.
> > > Transposed to {s}|=>t, that rule would state that {s}|=>t is SSI iff
> > > - s and t are both SSI, and
> > > - s recognizes the empty word
Again, I think we could require either s being prefix-closed or t being suffix-closed. Note the symmetry with s;t :-)
Regards,
Victor.
Hi Alexandre,
> Currently r[*i:j] is SSI iff j=inf and i<=1 (used to be i==1 before your mail).
I'm not sure if this is correct, as it implies that r* is ssi if r is ssi, even if r is not a Boolean, but Dax at al. mentioned that the use of * has to be restricted (but without giving an example of ssi violation). So it's your word against theirs :-) Do you have a proof? (I played with Spot a couple of minutes and could not quickly find a violation, so you may well be right.)
> [=i:j] and [->i:j] are sugar on top of ; and [*i:j], so it follows from those
> definitions.
> (Spot's AST has no representation of those operators, they only exist in the
> parser and printer.)
The situation with [=i:j] and [->i:j] is less boring than that! E.g. b[->1:$] would be translated to something like (!b[*];b)[+], which is si but not ssi. I've worked out the cases for these operators as follows (the proofs rely on the magic regex equivalence (a[*];b)[+];a[*] = (a|b)[*];b[+] which can be checked e.g. here: https://regex-equality.herokuapp.com/):
Lemma: b[->i:j] is si iff j=0 or (j=$ and i<=1)
j=0: then i=0 and so b[->i..j] = (!b[*];b)[*0] = [*0], so si
j!=0 and j!=$: then b[->i..j] accepts b[*j] but not b[*j+1], so not si
j=$ and i>1: then b[->i..j] accepts b[*i] but not b[*i-1], so not si
j=$ and i=1: then b[->i..j]=(!b[*];b)[+]=[by regex magic]=(!b|b)[*];b[+]=[*];b[+], so si
j=$ and i=0: then b[->i..j]=(!b[*];b)[*]=[*0]|above line, so si
Lemma: b[=i:j] is si iff j=0 or (j=$ and i<=1)
j=0: then i=0 and so b[=i..j] = (!b[*];b)[*0];!b[*] = !b[*], so si
j!=0 and j!=$: then b[=i..j] accepts b[*j] but not b[*j+1], so not si
j=$ and i>1: then b[=i..j] accepts b[*i] but not b[*i-1], so not si
j=$ and i=1: then b[=i..j] = (!b[*];b)[+];!b[*] = [by regex magic] = (!b|b)[*];b[+];!b[*] = [*];b[+];!b[*], so si
j=$ and i=0: then b[=i..j] = (!b[*];b)[*]];!b[*] = (e|(!b[*];b)[+]);!b[*] = !b[*] | (!b[*];b)[+];!b[*] = [due to previous case] = !b[*] | [*];b[+];!b[*] = [*] so si
> cl(r) in Dax et al. is the same as {r} in Spot.
>
> But you are not the only one having trouble with closure :-) See
> https://gitlab.lrde.epita.fr/spot/spot/issues/242
So, just to confirm, Dax et al.'s cl(), PSL's {}, and Spot's {} are all the same, aren't they?
> I would suggest that at the SERE level the rule for the n-ary concatenation
> r1;r2;r3;...;rn
> could be extended so that the entire concatenation is SSI iff each ri is SSI and
> at most one of them rejects the empty word.
Wow, that is a nice generalisation! Do you have a proof? I think it will be nicer and easier to state for the binary ";", and then the n-ary case immediately follows.
> Transposed to {s}|=>t, that rule would state that {s}|=>t is SSI iff
> - s and t are both SSI, and
> - s recognizes the empty word
I did some experiments with the online tool, and what you say seems correct, but I don't understand why there is asymmetry w.r.t. s (but not t) recognising the empty word - the intuition of s;t seems symmetric?
> If we had complementation of SERE, would first_match(r) be implementable
> as r && ((!r);1[+]) ?
I think you meant r && !(r;[+]), which is a nice idea, but Spot won't accept it (I guess), and generally it seems computationally expensive. I think at the level of automata one can simply get an NFA for r, and then delete all arcs from accepting states?
The other things you mentioned, like $rose etc. seem to need past modalities? Or you can mix state-based and action-based logics?
Generally, "throughout" and "within" are just syntactic sugar, so should be easy to add. The ?: can be added as syntax sugar, but hopefully one can do better than that and avoid the exponential blow-up due to repeating A in A&B|!A&C - this is in fact just a theoretical blow-up, unlikely to happen in practice. The first_match requires some work with automata, but seems possible. I'd say Spot is just a few steps away from full alignment with SVA and PSL.
Regards,
Victor.
Thanks Alexandre,
> The syntactic SI subset we catch should correspond to siPSL. (If you know a
> larger subset, that would be a welcome addition.)
What I'd like is to extend the ssi syntax to "sugar" operators too. Unfortunately, my intuition is unreliable with ssi :-(
To recap, Dax et. al. syntax for siSERE is:
r ::= [*0] | b[+] | b[*];r | r;b[*] | r:r | r|r | r&&r | r[:+]
I believe one can add the following:
- b[*], as b[*]=([*0] | b+), e.g. Spot doesn't recognise it's ssi
- (r & r), as (A & B) = (A;[*] && B)| (A && B;[*])
- any_formula[*0], as it's [*0]
- if the overall formula is {b}, it's ssi.
Another problem is that, say, (a[*];b[*]);(c[*];d[*]) is not ssi, but can be transformed to ssi form using associativity of ";".
Now, for special cases of i and j, the r[*i:j], b[*i:j], r[=i:j], r[->i:j] may be ssi (I tried to work these out, but was confused by the {a[=2:3]}|->b result).
PSL closures:
cl(r) is part of ssi syntax so ok
not sure about {r} - it might be obvious, but I don't understand closures well, especially if negations are involved...
{r}! is equivalent to {r}|->1, so I think it's ssi
Bindings: |-> is ssi, but I'm not sure about when |=> might be ssi?
If you ever going to support SVA-like "throughout" and "within", they are ssi:
A throughout B = (A* && B), A is Boolean
A within B = (([*];A;[*]) && B)
Also, SVA's first_match operator is interesting - do you know of a general way of translating it to other operators, or, alternatively, do you plan to ever add it? (BTW, it would also be nice to have C-like ternary operator ?: to avoid the exponential blow-up in its translation.)
> > {a[->2:3]}|->b
> I can't reproduce this one. It is shown as stutter-sensitive for me.
Sorry, my bad, it's indeed ss.
Thanks,
Victor.
Dear Spotters,
Could anyone explain Spot's algorithm for checking whether a PSL formula is syntactically stutter-invariant (ssi), including all supported PSL operators? I'm aware of Dax et al. ATVA'09 paper, but the syntax there is rather rudimentary, and there seems to be more to this. E.g.
{a[=2:3]}|->b
is rewritten (using the online spot's toolkit) into
a R (!a | X({a[->1..2]}[]-> (b & X(b W a)))) and yet it is classified as ssi in spite of all the Xs. On the other hand, a seemingly similar
{a[->2:3]}|->b
is classified as si but not ssi for some reason...
Many thanks,
Victor.
Hi Alexandre,
I run the experiments and found two formulas where ltl2tgba did not
finish correctly. The formulas were
& | G F p0 F G p1 | G F ! p1 F G p2
& & | G F p0 F G p1 | G F ! p1 F G p2 | G F ! p2 F G ! p0
The according command-line was:
ltl2tgba -D --generic -C -S --lbt-input -f ${FORMULA}
Output was:
ltl2tgba: direct_simulation() requires separate Inf and Fin sets
Best,
David
Question about the command line interface. I know something like
ltlfilt -f 'a U (b U a)' --equivalent-to 'b U a’
can be used to determine if two LTL formulas are equivalent.
Is there a way to do that if both formulas are in files?
From the man page I could only see how to make the first formula come from a file (-F).
