# Translation of Omega Automaton to LO2

Exam : 15.02.2017 : Q 8 d part 2 : 2017.02.15.vrs.solutions.pdf (uni-kl.de)

Problem : Translate below formula to LO2 :

I am first using boolean operations for disjunction of two automaton.

Then I am just translating it to LO2 presented in lecture (Module 8 - Slide 25)

Q. Could you please check if the steps I am following is correct ?

Q. Also could you please check if the solution is correct ?

Update : 25.08.2022

Final resultant in LO2 of Product automaton

edited

+1 vote

Well, there are many ways how you can solve this. As I can see, you used the sum automaton to compute the disjunction of the two automata, and then you translated the result to LO2. That is fine.

However, you do not need the sum automaton here. The disjunction of universal automata is dual to the conjunction of existential automata, and for the latter, the simple product automaton would  be sufficient. Hence, you don't need an additional state variable.

I would have solved it as follows without modifying the automata:

```    ∀p.
(
(∀t1. (t0≤t1 → (∃t0. t1<t0 ∧ (∀t2. (t1<t2 → t0≤t2)) ∧ p[t0]) ∧ p[t1] ∧ a[t1]))
→
(∀t1. (t0≤t1 → ¬p[t1]))
)
∨ ∀q.q[t0]

```
by (166k points)
selected by
Thanks for the clarification and the property.
I have applied the product automaton and the final result I have updated in the problem.
I understood your solution as well.
Could you please let me know if my updated solution in the problem is also correct or not ?
I think that your new solution is also correct. As said, there are many ways how to solve this, and the formula can be simplified further if wanted. But there is no need to do so.
Thanks for the clarification :)