Shannon normal form with Temporal operator

Question

I am solving exam problem 16.02.2022 Q 6 a - 2022.02.16.vrs.solutions.pdf (uni-kl.de)

The first part is clear where we translate negation of LTL to the omega automata but for the second part I have some query.

Q1 : I interpreted X q0 , X q1, X q2 as q0', q1', q2' respectively in transition relation because it says in the next time (next state) ? Is it right ?

Q2 : Based on above interpretation I calculated the SNF normally and came as below (solution). But for some combination of q0, q1 and q2 the result is not as written in exam solutions for example for q0 = 0, q1 = 1, q2 = 0. Could you please confirm if my SNF is right or there is mistake in this ? 

I tried with tool but tool calculates SNF for every variable so it was hard to interpret from there (or you can please guide me how to calculate SNF while not calculating the result for certain variables and give the result in propositional formula) 

Comments

I got the same SNF but I am still quite confused as to how it has been added to the relation table. For e.g q0=q1=q2=0, the answer would be (a & !xq0 & !a | !xq1 )right? but the table shows (a & !xq0 & !xq1). Am I missing something?

If you have solved it or figured out the right way to do it, please post it back.

Tool shows huge tree for SNF and BDD isn't helpful either

---

Hi

I assume that you are missing a bracket and the equation should be like this (a & !xq0 & (!a | !xq1))

There is a slight simplification you have to do like below in order to get the same result as in the solution :
a & !xq0 & (!a | !xq1)

=(a & !xq0 & !a) | (a & !xq0 & !xq1)

The first part becomes 0 because of a & !a and the rest is the same as in the solution.

Hope it helps.

---

Got it. Thank you!

Answer 1

Yes, you may ready X q as q' since both shall express the value of q in the next step. 

You can use the tools if you abstract the next-variable formulas to a new variable. For instance, for the transition relation in question, i.e.,

    (q0 ↔ ¬a ∨ X q0)   ∧

    (q1 ↔ a ∧ X q1)    ∧

    (q2 ↔ q1 ∨ q0 ∧ X q2)

We may abbreviate X q0, X q1, X q2 with new variables xq0,xq1 and xq2 to get the following:

    (q0 ↔ ¬a ∨ xq0)   ∧

    (q1 ↔ a ∧ xq1)    ∧

    (q2 ↔ q1 ∨ q0 ∧ xq2)

Now that is propositional logic, and you can use tools for the latter. For instance, you can compute the following BDD: 

Comments

I got it.
Thank you for the detailed explanation.