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

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.

$$\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).

• So, if the trace from $s_2$ is an infinite one such as $s_2$ infinitely coming back to itself (s_2 -> s_2-> ... forever) then the next state will always be $s_2$ right? – Papaya Automata Dec 12 '19 at 17:09
• @PapayaAutomata Well, yes, there is exactly one trace from $s_2$ of this form in your example. I'd like to stress, however, that this has nothing to do with LTL - that's just the definition of a trace. – DCTLib Dec 13 '19 at 8:51
• Thank you I understand now. – Papaya Automata Dec 13 '19 at 15:30