LTL model checking doubt

Question

Exam : 14.02.2018 : Q 7 b : 2018.02.14.vrs.solutions.pdf (uni-kl.de)

I can't interpret this explanation really well.

As what I understood to do model checking in this product structure is that we have to satisfy :

Phi_I -> A ! accepting_condition

But in this there is no initial condition and no infinite path. 

Could you please reiterate this explanation ?

Answer 1

I hope the new explanation of LTL model and validity checking on slides 67 and 68 on the new slides is more comprehensive. For LTL model checking, of an LTL formula Φ ≡ Aφ, we translate ¬φ to an existential automatn with acceptance condition φF and initial states φI. We then have

    (K,s) |= A φ  ⇔  ¬∃q.(K×KA,s×q) |= φI ∧ EφF
                  ⇔   ∀q.(K×KA,s×q) |= φI → A¬φF

In the exam problem, the automaton for ¬φ is already given with a Kripke structure. So, what needs to be done is to compute the product of the automaton and the Kripke structure, and then we have to check whether for all initial states s, we have ¬∃q.(K×A,s×q) |= φI ∧ EφF.

Computing the product gives us however a structure without any infinite path and no initial states, so that it is clear that all states satisfy Aφ.

Comments

Yes indeed the new video and slides are very detailed and is really good for understanding the concepts.

I understood your explanation.
So basically as A phi holds on every state that has no infinite path and for that reason this product structure is satisfied. Is this right ?

Also if I have some infinite paths in the product structure then I just have to  check  ¬∃q.(K×KA,s×q) |= φI ∧ EφF , and if all the initial states are in this set then it means that it satisfies the A(!a | phi) (just like we check in mu calculus) i.e K |= A(!a | phi) holds. Is this right ?

We had another problem like given a LTL formula and and prove that formula is valid, and to solve this we translate the negation of that formula to an equivalent omega-automata and check all the acceptance conditions if any of the acceptance conditions invalidates then we know that the formula is valid.
So can we also say for this question as if K |= A(!a | phi) holds then that formula is invalid and if it doesn't hold i.e ¬∃q.(K×KA,s×q) |= φI ∧ EφF then the formula is valid ?

---

Yes, A phi holds on every state that has no infinite path and for that reason this product structure is satisfied.

If there are some infinite paths in the product structure starting in state s, then we have to check ¬∃q.(K×KA,s×q) |= φI ∧ EφF, i.e., that there is no run q in the automaton that starts in the initial states and satisfies the acceptance condition.

The nasty thing the the examp problem is that we do not just check there A phi, but A(!a | phi) which is equivalent to !a | A phi. Hence, to check whether there is a state s such that s |= !a | A phi, we have to check that s |= !a or s |= A phi holds. The latter is what we discussed so far, but additionally, we should check also s |= !a for this exam problem.

About validity, we can also say the following: Validity of LTL can be reduced to LTL model checking in the structure that consists of all states that you can construct for the given variables V, i.e., the states are all the subsets of V, and transitions are between every pair of states. Then, this structure has all possible paths in it, and if we state that all states are also initial states, then checking whether this structure satisfies the LTL formula means checking that all paths are satisfying the LTL formula. While that Kripke structure seems to be enormously large (and in fact it is), its symbolic representation is just the formula true, so that is very small.