LTL Model checking

Question

Hi, 

I have a doubt regarding the relationship and omega automaton transition.  

From the transition relation, how can I draw the transitions? Should I substitute like  {p=false, q= false} , {p=false, q= true} , {p=true, q= false} , {p=true, q= true}. When i tried to substitute like this i got the solution like this. Is it the proper way to convert , Could you please help to solve this?

Answer 1

Okay, I will do that in great detail below, and you can do many of these steps at once, of course. Instantiating all cases for p and q yields:

    p q
    0 0  (0 <-> a V b & Xp) ^ (0 <-> 0 V a & Xq)
    0 1  (0 <-> a V b & Xp) ^ (1 <-> 0 V a & Xq)
    1 0  (1 <-> a V b & Xp) ^ (0 <-> 1 V a & Xq)
    1 1  (1 <-> a V b & Xp) ^ (1 <-> 1 V a & Xq)

and thus

    p q
    0 0  !(a V b & Xp) ^ !(0 V a & Xq)
    0 1  !(a V b & Xp) ^  (0 V a & Xq)
    1 0   (a V b & Xp) ^ !(1 V a & Xq)
    1 1   (a V b & Xp) ^  (1 V a & Xq)

which simplifies to (note that x&phi is equivalent to x&(phi[x<-1]))


    p q
    0 0  !(a V b & Xp) ^ !(a & Xq)
    0 1  !(a V b & Xp) ^ a & Xq
    1 0   0
    1 1   (a V b & Xp) 

and further to 


    p q
    0 0  !(a V b & Xp) ^ !(a & Xq)
    0 1  !(1 V b & Xp) ^ a & Xq
    1 0   0
    1 1   (a V b & Xp) 

which results in

    p q
    0 0  !(a V b & Xp) ^ !(a & Xq)
    0 1  0
    1 0  0
    1 1  a V b & Xp 

So, we have no outgoing transitions in states {p} and {q}. For state {p,q}, we have outgoing transitions for a to anyone of the four states, and for b to the states {p} and {p,q} since Xp must hold then. 

The transitions of state {} are more difficult. We further simplify the transition relation and get the following

    !(a V b & Xp) ^ !(a & Xq)
    = !a & !(b & Xp) ^ !(a & Xq)
    = !a & !(b & Xp) ^ !(0 & Xq)
    = !a & !(b & Xp) ^ !(0)
    = !a & !(b & Xp) 
    = !a & (!b | !Xp)
    = !a & !b | !a & !Xp     

Hence, we have transitions to anyone of the four states with !a&!b and to the states {} and {q} for input !a. 

Comments

Thanks for the reply. I understood most of the steps,
    p q
    0 1  !(1 V b & Xp) ^ a & Xq

but why here 'a'=1 in one side and not in another side? Is there any particular rules for case splitting? Also in this step as well,     !(a V b & Xp) ^ !(a & Xq)
    = !a & !(b & Xp) ^ !(a & Xq)
    = !a & !(b & Xp) ^ !(0 & Xq) , do we have certain rules for case splitting? I didnt understand that

---

For the first point, note that x&phi is equivalent to x&(phi[x<-1]) and !x&phi is equivalent to x&(phi[x<-0]) in general. For the second thing, I first wrote we make a further case split on variable "a", but then I rather simplified the transition relation. I fixed the text accordingly.