Dear SPoT developers, I am writing to you to ask you a question about the semantics of PSL and SPoT. I will start by explaining my problem. I am interested in computing the automata associated to a Linear Dynamic Theory under Linear Dynamic Logic semantics. The semantics can be found in the following paper: https://www.cs.rice.edu/~vardi/papers/ijcai13.pdf Although the semantics are interpreted on finite traces I would be interested in using infinite traces. I found out that SPoT allows expressing PDL regular expressions on linear (infinite) traces, which is what I was looking for. 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. My questions are the followings: 1) Do they allow to express the same properties ? and 2) How faisable is to accomodate the parser to accept the PDL syntax ? Could you give me some hints on this case ? Kind regards, Martin.