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)?