2
$\begingroup$

I am trying to solve some past papers in preparations for my next exam and I've stumbled across the following exercise: 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

$\endgroup$
0
$\begingroup$

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.

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