Doubt in LTL model checking

Question

Exam : 16.02.2022 : Prob 6 a : 2022.02.16.vrs.solutions.pdf (uni-kl.de)

I tried without shannon normal form i.e just putting q0 =0, q1=1, q2 =0 in the transition relation but the result is different from exam solution i.e my result came as (a & !xq0 & xq1 & !xq2) and in exam solution it is 0 i.e deadend state.

Q1. Why directly putting values of q0,q1,q2 from truth table and solving is not working ?

Q2. Could you please explain why there is a need for SNF here ?

Q3. How could I determine whether to apply SNF or just putting values from TT will work ?

Answer 1

Q1: It certainly has to give the same results, and it does so:

q0=0, q1=1, q2=0 yields

    (0↔¬a∨Xq0) ∧ (1↔a∧Xq1) ∧ (0↔1∨q0∧Xq2)
    = ¬(¬a∨Xq0) ∧ (a∧Xq1) ∧ ¬1
    = 0

Q2: There is no need for a SNF, it is just suggested to compute the solution in the example solution. There are also many alternatives for sure.

Q3: For reasoning about SAT, there is no recipe that you can follow. If that would be known, you can win a million dollar price. Instead, you always have to check the formula and have to see what works best in the given case. 

Comments

I checked it again and indeed the result is same.
I did slight mistake while solving.

I understood all your point on reply for Q1,Q2 and Q3.

Thanks for clarifying the doubts :)