What is the LTL expression for "there is a value of y whose next value is 8"?

Question

Basically i have a program which increases a variable by 1 in each iteration and resets it to 0 as soon as y becomes 8 (i.e. mod 8).

It is a quite simple example but it still bugs me out because i cannot clarify if my LTL-formula is correct for the property "there is a value of y whose next value is 8". For this i came up with the:

$$FX(y \doteq 8)$$

which means "somewhere in the future the next value of y is 8".

Is it the correct LTL formula for my question (even though it is of course invalid for my application)?

Answer 1

The important thing that is missing from your question is how you model your program, and specifically, what are the atomic propositions you allow.

If your atomic propositions are "y=0",...,"y=8", and your transition system is modeled accordingly, then the formula $FX y=8$ means the eventually, the next position would have "y=8". Note that this is equivalent to the formula $XF y=8$, which basically says that y=8 sometime after the first position.

However, you phrased your requirement as "there is a value of y whose next value is 8", and it's not clear what this means. What is the "next value of y"? LTL does not recognize y as an entity, only the propositions mentioned above. So you cannot really talk about values of variables in LTL, without first adding all possible values as propositions.