# LTL model checking exam 15.02.2017

I am solving exam question 15.02.2017 - Problem 6 (b) : 2017.02.15.vrs.solutions.pdf (uni-kl.de)

Exam Question: I have some doubt in last part of the solution.

Product of Kripke : Relevant slide : Solution : I followed the above slide and explanations and able to solve till the highlighted part.

Q. Could you please explain what is happening here means states without [EGF(p&b] = {} ?

Q. Could I not find it directly by checking that is there an infinite run in the obtained product of Kripke structures from initial state ?
Like there is an infinite run from SQ3 -> SQ1 -> SQ0 -> ..... and GF (p & b) holds here i.e. p & b holds infinitely often and thatswhy this acceptance is valid which results in A(si | phi) does not hold in K.

The example solution has been adapted to make it more comprehensive. Thanks for pointing out the unclarity.

+1 vote

There are some lines with a bit sloppiness in the argumentation that refer to the reachable states only and not to the real product structure, and some refer to the original structure and not the the product.

The first example solution is fine up to the following line

Kx |= p -> !a | AFG!(p&b)

From here, I suggest a slighly different argumentation. The above is equivalent to the following two statements

Kx |= p -> !a | !EGF(p&b)

Kx |= p -> !a | !nu y. <>(mu x.(y & (p&b) | <>x))

That can be easily checked with our tools, and we get

〖 nu y. <> mu x. (y & p & b | <> x)〗 = {SQ0;SQ1;SQ3}

〖!nu y. <> mu x. (y & p & b | <> x)〗 = {SQ2}

〖!a〗 = {SQ0}

〖!a | !nu y...〗 = {SQ0,SQ2}

〖p〗 = {SQ2,SQ3}

〖p -> !a | !nu y.〗 = {SQ0,SQ1,SQ2}

Hence, the intitial states {SQ3} are not contained, so that the product structure does not satisfy the above formula, and therefore K does not satisfy A(ψ ∨ φ) which is equivalent to this.

Now, consider the alternative solution that starts as follows

K |= A(ψ ∨ φ)

⇔ K |= A(¬a ∨ φ)

⇔ K |= A(a → φ)

⇔ K |= A(¬a ∨ φ)

⇔ K |= ¬a ∨ Aφ

At the next point, it is argued that the above should be equivalent to K |= Aφ. However, in structure K, we have two initial states s2 and s3 where s3 satisfies "a" and s2 does not. So, we should better continue as follows:

⇔ K,s3 |= ¬a ∨ Aφ & K,s2 |= ¬a ∨ Aφ

⇔ K,s3 |= ¬a ∨ Aφ

⇔ K,s3 |= Aφ

⇔ K,s3 |= ¬E¬φ

⇔ K,s3 |= ¬EA∃(Q,φI,φR,φF)

⇔ K×,SQ3 |= ¬EφF

⇔ K×,SQ3 |= ¬EGF(p ∧ b)

⇔ K×,SQ3 |= ¬nu y. <>(mu x.(y & (p&b) | <>x))

As before, we have

〖 nu y. <> mu x. (y & p & b | <> x)〗 = {SQ0;SQ1;SQ3}

〖!nu y. <> mu x. (y & p & b | <> x)〗 = {SQ2}

Hence, the intitial states {SQ3} are not contained, so that the product structure does not satisfy the above formula in SQ3, and therefore K does not satisfy A(ψ ∨ φ) which is equivalent to this.

As you wrote above, there is a path from the initial SQ3 that satisfies GF(p ∧ b), and since that is the only path, we have A¬GF(p ∧ b) which means ¬EGF(p ∧ b).
by (142k points)
selected by
It is clear now :)
Thanks a lot for explaining this very precisely.
+1 vote

Q. Could you please explain what is happening here means states without [EGF(p&b] = {} ?

This double square bracket with a Kripke structure in the subscript means: The set of states of the Kripke Structure in the subscript that do satisfy the formula in the brackets. The first equivalence in the marked line just explains the negation: The state set satisfying the negated formula is exactly the same as all states without the states satisfying the unnegated formula.

Q. Could I not find it directly by checking that is there an infinite run in the obtained product of Kripke structures from initial state ?

What is direct and what is indirect? I'd say one solution is programmatically, the other one manually, finding the counterexample.

by (25.6k points)
Thanks for the explanation.

I got your explanation regarding the notations, but could you please explain briefly on how resultant empty state {} concludes that A(si | phi) does not hold in K ?

Yes you are right directly I meant that manually with some intuition.
So could you please let me know whether below intuition is correct or not ?
*Like there is an infinite run from SQ3 -> SQ1 -> SQ0 -> ..... and GF (p & b) holds here i.e. p & b holds infinitely often and thatswhy this acceptance is valid which results in A(si | phi) does not hold in K. *