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

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.