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