Global Model Checking (solution sheet 6)

Question

In solution file (https://es.cs.uni-kl.de/teaching/vrs/exercises/06-Solutions.pdf) page 12, step 1, how is the universal predecessor of {s3,s8} is {s3,s8}?

Answer 1

This is because we compute the fixpoint mu y.((c|x)&[]y) and have evaluated the body formula (c|x)&[]y with the current approximation for y which was {}. Using {} for y, we evaluated (c|x)&[]y as {s3,s8} which is now the updated value of y for the next iteration. With that value for y, we obtain again {s3,s8} for (c|x)&[]y which is therefore now the fix point that we wanted to compute.

Recall that the fix point iteration of a function always computes y_{i+1} = f(y_i) and that we start with {} for least fix points while we start with all states for greatest fix points.

Comments

I meant specifically line 3 that is box of y = {s3,s8}. How did we get that? because it means the states whose all successors satisfy {s3,s8}. But I don't understand how it's satisfied!

---

We get that result because according to the definition of universal predecessors in the lecture notes, we call universal predecessors those states whose successors satisfy phi or states that have no successors at all (meaning deadends).

---

The only state that has a successor in {s3,s8} is s2. But since we have a box-operator, we are talking about universal successor. s2 has other successors as well, so s2 doesn't count here. Since having no successors qualifies for “only having successors in a certain set“, our deadend states are an answer. Hence, we add the deadends {s3,s8}

---

If you want to compute []y and know that y corresponds with the states {s3,s8}, you have to compute pre∀({s3,s8}). Now recall that

 pre∀(Q2):={s1 ∈S|∀s2 ∈S.(s1,s2)∈R→s2 ∈Q2}

i.e.

 pre∀(Q2):={s1∈S | suc(s1) ⊆ Q2}

So, we need to find the states s1 such that all of their successors are within {s3,s8}. Checking the table in the slides on page 8, you can check now state by state for which of the states this is the case. You will see that only s3 and s8 (both having no successors) fulfill this while all others have a successor which is not in {s3,s8}.