29 Dec
2023
29 Dec
'23
11:31 a.m.
Hi Marco,
Marco Faella <marfaella(a)gmail.com> writes:
It seems that subformulas of the type "X p"
get translated into "X
(!alive | p)" instead of "X (alive & p)", as they should be according
to the LTLf semantics, as well as the translation outlined in the
Memocode '14 paper by Dutta and Vardi.
This all depends on whether you consider X to be weak or strong. That
paper gives the semantics for a strong X. However, in Spot
- X is the weak next.
- X[!] is the strong next.
See https://spot.lre.epita.fr/tut12.html#org0e1e575