Hi Alexandre, 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.) 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 So, just to confirm, Dax et al.'s cl(), PSL's {}, and Spot's {} are all the same, aren't they? 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. 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? 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.