Hi Martin,

However, after checking the specification language, I found that the dynamic operators are not "exactly" the same as those of Linear Dynamic Logic. I mean, I was expecting to write [(true;true)*] p instead of {(1;1)[*]}[]->p to represent the even-state problem.

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:

1. Do they allow to express the same properties ? and

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.

2. How faisable is to accomodate the parser to accept the PDL syntax ? Could you give me some hints on this case ?

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