# LO2 to omega automata

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 ?

+1 vote

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.
by (142k points)
selected by
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.