# LTL to Omega Automata (Exam paper 2021-02-17 Question 6b).

LTL to Omega Automata (Exam paper 2021-02-17 Question 6b). How to generate the Kripke structure from ¬q0 ∧ ¬q1 ∧ a ∧ ¬b ∧ ¬Xq0 ∧ ¬Xq1(highlighted in the image attached).  I tried to substitute the values of 00, 01, 10, 11 for  q0, q1 in ¬q0 ∧ ¬q1 ∧ a ∧ ¬b ∧ ¬Xq0 ∧ ¬Xq1 and get the transitions. But I was not sure how to handle ¬Xq0 ∧ ¬Xq1 while doing this.

The transition relation of the automaton is (q0 ↔ b ∨ a ∧ Xq0) ∧ (q1 ↔ ¬b ∧ (¬a ∨ Xq1)) which can be rewritten as DNF as follows:

```¬q0 ∧  q1 ∧      ¬b ∧ ¬Xq0 ∧  Xq1 ∨
¬q0 ∧ ¬q1 ∧  a ∧ ¬b ∧ ¬Xq0 ∧ ¬Xq1 ∨
q0 ∧  q1 ∧  a ∧ ¬b ∧  Xq0 ∧  Xq1 ∨
q0 ∧ ¬q1 ∧       b               ∨
q0 ∧ ¬q1 ∧  a      ∧  Xq0 ∧ ¬Xq1 ∨
¬q0 ∧  q1 ∧ ¬a ∧ ¬b
```

Looking at it this way shows that we may end up with a lot of satisfying assignments and thus, with a lot of transitions in the Kripke structure. Fortunately, most of them are not reachable, so we better concentrate on the reachable states.

Starting with the initial state of the automaton ¬q0 ∧ ¬q1, we pick the transitions that are encoded by the following disjunct that is contained in the above DNF. Even not having the DNF, we can obtain that formula differently as shown in the example solutions:

¬q0 ∧ ¬q1 ∧  a ∧ ¬b ∧ ¬Xq0 ∧ ¬Xq1

For the automaton, we consider this as a formula over the "variables" q0,a1,a,b,Xq0,Xq1 and therefore, we get only one assignment that encodes the transition from state {} for input {a} to the next state {}. So, we do not reach a new state, and therefore that transition is all we need. You may now derive the Kripke structure from this automaton.

Alternatively, for the Kripke structure, we consider the above formula over the "variables" q0,q1,a,b,Xq0,Xq1,Xa,Xb and therefore get four assignments that encode the transitions from state {a} to states {},{a},{b},{ab}, respectively.

So, we just have to compute the satisfying assignments of a propositional logic formula reading Xq0 as a propositional variable.

by (166k points)