# Transition Relation - SNF - LTL Model Checking

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

+1 vote

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)

by (166k points)
selected by
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.
SNF - LTL model checking