Suppose we consider TLSF instead of LTL, that means you can write F_k phi meaning things have to be satisfied within k steps. Can we use the fact that we strengthen semantics in the game to avoid unrolling the F_k into k-nested next? What about G or Until?
Suppose we consider TLSF instead of LTL, that means you can write F_k phi meaning things have to be satisfied within k steps. Can we use the fact that we strengthen semantics in the game to avoid unrolling the F_k into k-nested next? What about G or Until?
This was proposed by A. Cimatti.