LTL validity checking

Question

I have a doubt regarding the transitions of this omega automaton, I tried to give to give values to  p and q like 00,01,10,11. But I'm not getting the exact same transitions like in the diagram. I think I need to add some case splits for a and b as well. But I'm unsure about how to proceed further, got stuck in this part. Could you please help on this?

Answer 1

We get

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

and thus

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

and thus

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

Now, note that

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

and

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

Comments

!(a | b & Xp) & !(a & Xq)
    = !a & !(b & Xp) & !(a & Xq)
    = !a & !(b & Xp) & !(0 & Xq) in this step, how can we put 0, in one-side ? why not 1? What is the purpose this case split, if i split using 1 , is it invalid?

---

This is mentioned on page 69 of VRS-04-TransitionSystems for example. It is a general simplification rule of propositional logic which is the unit clause rule in DPLL: If x&phi is given with a variable x, any model must make x true, so that we can consider x&(phi[x<-1]) instead.

---

okay.. i checked the slides.
    here !a & !(b & Xp) & !(a & Xq), as per my understanding
  X is !a and Phi is  !(b & Xp) & !(a & Xq) .
φ ∧ ¬ x ⇔ using this,
!a & !(b & Xp) & !(0 & Xq) ?

If we have.  a & !(b & Xp) & !(a& Xq) , i can use
φ ∧  x ⇔  
!a & !(b & Xp) & !(1 & Xq) ? will it work if we have positive x&phi?


And also !a & !b | !a & !Xp which is the transition relation for {} state,
it has to take !a then go to {q} ,{} . also !a&!b, it should go to all the states , but transition is given to only {p} and {p,q} ,why is that ?

---

No, for !a & !(b & Xp) & !(a & Xq) we know that variable "a" must be false in any model, so we replace "a" in the second conjunct !(b & Xp) & !(a & Xq by 0 (denoting false).

In a & !(b & Xp) & !(a& Xq), we know that every model must satisfy "a", so we replace "a" by true in !(b & Xp) & !(a& Xq).

---

I understood that clearly. But i have query here,
!a & !b | !a & !Xp which is the transition relation for {} state,
it has to take !a then go to {q} ,{} . also !a&!b, it should go to all the states , but transition is given to only {p} and {p,q} ,why is that ? And why !a&!b is not going to state {},{q} ?

---

As you realized,  !a & !b | !a & !Xp describes the transitions from state {}. For a=b=0, we can go to any states, and for a=0 and any b, we can go to either {} or {q}. So the condition for the transition {}->{} is !a which encodes a=b=0 and a=0&b=1, the condition for {}->{p} is a=b=0, and so on.

---

Okay..but if I draw a transition for {} with  !a&!b to all other states like {},{p},{q},{p,q}  will it be a valid? Since here !a&!b is only given to {p} , {p,q} and {},{q} are missing in the diagram

---

If you write a transition from {} to any other state and label it with a=b=0, that is correct, but not sufficient, since the transitions {}->{} and {}->{q} are also possible with a=0&b=1. That would then be missing unless you add these transitions as well. Note that !a&!b | !a&b = !a, so that is why there is only one transition that has actually both labels.

---

(a | b & Xp) here, I have expanded this to
(a | (b&Xp) ) = (a | b) & (a | Xp ) = (a & a) | (a & Xp) | (b & a) | (b & Xp)
                                                   = a | Xp(a | b) | b & a = Xp(a | b ) | a (b | a )
                                                   = a | Xp( a | b)
So the transition of {p,q} will be
taking a | b then has to go to {p} , {p,q} .
taking a alone, it has to go to {},{p},{p,q},{q} . But in the figure it goes to only {q} and {}. Since to the {p} , {p,q} states with a | b, b can be either present or not , and  the input (a | b) , (a),   in which (a) is already covered in the (a | b) , that's why we are not repeating the transition for input (a) to {p}, {p,q} . Is the correct ?

---

While your equivalences are correct, your conclusions are wrong. Also, you do not need these transformations. With a | b & Xp, we know that we can reach any state from {p,q} with inputs that satisfy a which are four transitions each one with two possible inputs. Moreover, we can reach the states {p} and {p,q} when b holds even if a does not hold.

---

Thank you professor , I understood it.