Re: [Spot] SPoT + PSL + Dynamic Logic.

Hi Martin, This formula can also be written {(true;true)*}[]->p, getting closer to what you wanted to write. The official PSL syntax for "suffix implication" (the operator {φ}[]->ψ used above) is {φ}|->ψ. They also have {φ}|=>ψ as syntactic sugar for {φ;1}|->ψ (note: not the same as {φ}|->Xψ if φ can match the empty word) so you can easily say if the ψ must hold on the last letter of φ or right after it. PSL don't provide a dual operator, which sucks when implementing a translation, so several papers use []-> instead so the dual can be written <>->, and we can still keep the []=>,<>=> sugar. My questions are the followings: If only looked briefly at the formal definition of the paper you quoted as well as in https://core.ac.uk/download/pdf/82563040.pdf [FL79], and it seems to me that PDL's [φ]ψ would correspond to {φ}[]=>ψ, not to {φ}[]->ψ. In particular, example 3(1) of [FL79] states that <a;a>p is the same as <a><a>p. Using Spot's PSL-derived operators it would be true that {a;a}<>=>p is the same as {a}<>=>{a}<>=>p, which is equivalent to a&X(a&Xp)) when a and p are boolean; while {a;a}<>->p would be equivalent to a&X(a&p). You can use the "rewrite" and "compare" tabs of https://spot.lrde.epita.fr/app/ to toy with these formulas and test equivalences. The semantics of the operators supported in Spot are in https://spot.lrde.epita.fr/tl.pdf in case you haven't seen that already. Before talking about the parser, isn't it acceptable to rewrite your formulas using Spot's syntax? % echo '[a]<b>[c|d]<e>p' | sed 's/\[\([^]]\+\)\]/{\1}[]=>/g;s/<\([^>]\+\)>/{\1}<>=>/g' {a}[]=>{b}<>=>{c|d}[]=>{e}<>=>p (I'm not sure if that's always as simple.) Teaching Spot's parser to support <φ>ψ as syntactic sugar for {φ}<>=>ψ should be quite straightforward. However dealing with [φ]ψ would be harder. The problem is that the next release of Spot includes support from TLSF's X[n], F[n:m], and G[n:m] operators. Basically sugar for multiple Xs: X[6]a = XXXXXXa F[2:4]a = XX(a | X(a | Xa)) G[2:4]a = XX(a & X(a & Xa)) So currently in the development version of Spot I can write X[1]a and that's synonym for Xa. But if we now decide to support [φ]ψ as sugar for φ[]=>ψ, then X[1]a can also mean X([1]a) = X({1}[]=>a) = XXa. I think the issue occurs only with [1], that can be interpreted either as a number or as true depending on the context. [1:1] would also be ambiguous because ":" is a supported operator for regular expressions. Best regards -- Alexandre Duret-Lutz