# LTL Formula Until with same atoms (aUa)

I am trying to solve some past papers in preparations for my next exam and I've stumbled across the following exercise: While I managed to solve most parts of the exercise, I am still unsure about the formula ((b)U(b)). I am unsure which node I should start checking from and on the general definition of U.

As far as I understood a state matches a general formula aUb if it satisfies the proposition b. So in this example would the states s1, s2 and s4 all satisfy ((b)U(b))? Am I approaching this the wrong way?

Thanks a lot

First of all LTL is defined over traces. In verification, we typically say that a state satisfies some LTL formula if all of the traces starting in the state satisfy the formula. I henceforth assume that this is what is meant in the question and this definition has been given in your course.

The Until operator is defined over a word as follows:

$$w \models \psi \mathcal{U} \phi \quad \text{ iff } \quad \exists i \in \mathbb{N}: \forall j\leq i. w^i \models \psi \wedge m^j \models \phi$$

In this equation, $w^i$ represents the word starting at position $i$, where all letters before position $i$ have been removed. Applied to the concretization $\psi = b$ and $\phi = b$, we have:

$$w \models b \mathcal{U} b \quad \text{ iff } \quad \exists i \in \mathbb{N}: \forall j\leq i. w^i \models n \wedge m^j \models b$$

Note that without loss of generality, we can assume that the $i$ searched for in the definition is always 0, because for $j=0$, we need to have $w^0 \models b$ for a word $w$ to be a model of $b \mathcal{U} b$. But then we can also choose $i=0$. Then the definition simplifies to:

$$w \models b \mathcal{U} b \quad \text{ iff } \quad m^0 \models b$$

Hence, you are searching for all states for which all outgoing paths start with a $b$ state, which is equivalent to saying that you search for all states in which $b$ hold.