Issue in translation from LTLf
Dear all, there seems to be a problem with the translation LTLf -> LTL, as supported by the "ltlfilt --from-ltlf" command from the SPOT distribution. 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. Do you agree or am I missing something? By the way, we are planning to use SPOT as part of a toolchain to check the satisfiability of a flavor of LTLf-modulo-theory. Thanks, Marco Faella -- Associate professor Electrical Engineering and Information Technologies University of Naples Federico II, Italy http://wpage.unina.it/m.faella
Hi Marco, Marco Faella <marfaella@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
participants (2)
-
Alexandre Duret-Lutz -
Marco Faella