Validity of self refering state with linear temporal logic 'X' connective

Question

Lets say we have model like the one above or a similar one where a node refers back to itself.

Now let's say if I want to know the validity of the formula:

$M, s_2 \models Xr$

Will this be valid or not. In my textbook it says :

$\pi \models X\phi$ iff $\pi^2 \models \phi$

If we are starting at state 2 then our path would be $S_2 -> S_2 -> ...$

So, I'm not sure since state 2 is not actually transitioning to another states like State 0 or 1. Otherwise would transitioning to the same state in a path $\pi$ be enough to satisfy the "X" connective.

Answer 1

Your textbook correctly states that

$\pi \models X\phi$ iff $\pi^2 \models \phi$

under the assumption that $\pi$ is a word/trace of the transition system and the characters of the word are numbered starting with 1.

So the question that you should ask is how an infinite trace from state $s_2$ would look like and then evaluate the formula on that trace. LTL is only defined on infinite traces, so these are the ones that you should be looking at.

Note that checking if

$M, s_2 \models Xr$

holds does not make sense (in general), as LTL is defined over traces, but from a state in a labeled transition system, there could be multiple traces. So it is not clear what $M, s_2 \models Xr$ should mean - does it mean that it's defined on any trace or every trace? This syntax seems to come from computation tree logic (CTL).