universal pred of a state = exist pred of a stat + deadends?

Question

Hello,

For the kripke:

vars a,b,c; init 3,6; labels 0:;1:a,b;2:;3:c;4:;5:;6:b;7:c;8:a,c; transitions 0->2;1->2;2->0;2->6;2->8;4->6;2->5;6->3;6->2;6->4;5->6;7->1; 3->5

and formula: nu x. (<> mu y. ((c | x) & [] y));

in step1, for "y={s8}", the tool is computing []y as {s8}. But why it does not including "s2" also, since it is a predecessor of s8. Is my understanding correct, that [universal pred of a state = exist pred of a stat + deadends] or the tool is wrong?

Answer 1

The definition of universal predecessor states is as follows:

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

Hence, a state s1 belongs to the universal predecessors of a set of states Q2 if all of its successor states are in Q2. The state s2 in your example has however a successor state s5 which is not in {s8}. 

Your understanding of the universal predecessor states is not correct. Use the above definition instead.

Comments

Thank you! Got it. I was missing the keyword "ALL" here. (

---

@erji Yes! That's exactly the point. Very good. Existential predecessors (diamond) have at least one edge to a given set, universal predecessors (box) only have edges to a given set.