# LTL Model checking

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?

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.

by (166k points)
edited by
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.