3
$\begingroup$

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

$\endgroup$
3
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.