Transition Relation - SNF - LTL Model Checking

Question

For the transition relation (q0 <-> !a | Xq0) & (q1 <-> a & Xq1) & (q2<-> q1 | q0 & Xq2), how do we get the truth table values? I see that SNF is used here but I tried doing on my own without using SNF like just plugging in values like how we do for symbolic computation, but that does not seem to be the case.

 Could you please explain one example atleast: when q0=q1=q2=0

Answer 1

For q0=q1=q2=0, we replace these variables by 0 in the transition relation, but not those behind an X-operator. Hence, from 

    (q0 <-> !a | Xq0) & (q1 <-> a & Xq1) & (q2<-> q1 | q0 & Xq2)

we get

    (0 <-> !a | Xq0) & (0 <-> a & Xq1) & (0<-> 0 | 0 & Xq2)

which is equivalent to

    !(!a | Xq0) & !(a & Xq1) 

Comments

I got the same answer that you got. It seems that I made a small mistake by not further simplifying the equation which results in a & !Xq0& !Xq1. I was however aware that the "next state X" should not be substituted.

Thank you very much for the clarification.