LO2 to omega automata

Question

Exam : 17.02.2021 : Q. 8 (i) : 2021.02.17.vrs.solutions.pdf (uni-kl.de)

As the above formula is Sing(p), my questions are :

Q1. As it is Sing(p), so we can directly convert it to omega automata as defined in the slide 30 of lecture 8 (From LO2' to Omega Automata) using acceptance as Fs1 & G !s2 (Deterministic) or Fs1 (non-deterministic). Is it correct ?

Q2. Also for others i.e Subset(p,q) and PSUC(p,q), we can do the same as stated in question 1 directly. Is this right ?

Q3. As in the slide below it is mentioned that Subset, Sing, PSUC belong to LO2', but as Sing contains t1 = t2 which is numeric variables, so how is it LO2'? Could you please explain ?

Q4. As LO2' is a special form of LO2 in which numerical variables are not allowed, so if the formula contains numerical variables i.e in LO2 we need to use algorithm ElimFO(phi) to convert it into LO2'. Is this right ?

Answer 1

Q1: yes

Q2: yes

Q3: LO2' uses the atomic formulas Subset(p,q), Sing(p) and PSUC(p,q) as written here, they are not expanded with their definitions. The syntax of LO2' considers them as given basic atoms.

Q4: yes, LO2' is a logic on its own that is following the syntax as given on the slide you mention. There are no numerical variables allowed in that logic.

Comments

Now its clear.
Thanks a lot for clarifying and explaining this :)

---

Can we add transition relations here similar to the method described in the Q:5(b) from https://es.cs.uni-kl.de/teaching/vrs/exams/2022.02.16.vrs/2022.02.16.vrs.solutions.pdf ?

For eg. (Xs0 <-> s0 & !s1 & !s2 & !p) & (Xs1 <-> ...) & (Xs2 <-> ... )

---

As the automata are all deterministic, this is possible, yes.