VRS : Global Model Checking Question

Question

<>x : it means atleast one successor

[]x : it means all successors or {}

suppose if x has some states like {s0,s1,s2,s3}

s0 has successors (s0,s1,s2)

s1 has successors ( s1,s2)

s2 has successors (s3)

s3 has successors {}

now if we have x = { s0,s1,s2,s3}

then following queries I have:

1.  <>x = {s0,s1,s2}  OR {s0,s2}   // because s0 already has succssor s0,s1,s2 , so can we exclude s1 in <>x ?

2. []x = {s0,s1,s2,s3} OR {s3} // []x means all successors or {} , so should we exclude s0,s1,s2 because they don't contain all successors mentioned in x?

Answer 1

Let's use the teaching tool for answering your question: you are considering the following transition system:

Here, we have

     〖x〗  = {s0;s1;s2;s3}
     〖<>x〗= {s0;s1;s2}
     〖[]x〗= {s0;s1;s2;s3}

It does not matter that s0 is already in x; <>x are the states that have a successor that satisfies x, and if such a state has a transition to itself or another one satisfying x, it belongs to <>x. Similarly with []x.

Comments

So can we say that []x contains all states which are in <>x and also the states which has empty successor?

Can you give an example where clear difference can be understood between <>x and []x?

---

Have a look at slide 52 of the Chapter on Transition Systems. The operators <> and [] are implemented by pre_Exist and pre_Forall.