Doubt regarding LO2' to omega automata

Question

Exam : 31.08.2021 : Q. 8(i) : 2021.08.31.vrs.solutions.pdf (uni-kl.de)

I understand about the Subset(p,q), but I am unable to understand about Sing(p) like which formula is applied to convert it.

As Sing(p) acceptance condition is F s1 & G !s2, if I convert it to omega automata there will be 2 states and acceptance condition would not be Fs1. 

Could you please explain how this is done ?

Update : 23.08.2022

My Solution :

Answer 1

Sing(p) should assert that p is a signal that holds exactly once. The automaton that is given in the solution in its symbolic representation looks as follows:

and demands that state s1 must be reached at least once. If you compare it with the automaton suggested on the slides (slide 30), it is not complete, while the one given in the slides is even deterministic (and adds a sink state after s1). 

Did you get it?

Comments

Thanks for your reply.

For the first part, if I use just the one state like below is it correct ? :
A_exist ({s1}, !s1, (!s1 & !p & !Xs1 | !s1 & p & Xs1 | s1 & !p & Xs1), Fs1)

For the second part:
I got your point by mistake I wrote disjunction, I will correct it.

---

Yes, the first part that you mention above is now the same as in the example solution which is correct.

---

Thanks for the clarification, yes I see :)
I just couldn't get why writing !s1 as another variable is wrong ?
As if I translate the provided Sing(p), there are two states. Could you please help me to understand this ?

---

You can try the transition relations you thought of with the tool https://es.cs.uni-kl.de/tools/teaching/SymbolicStateTrans.html, and you can then see the transitions encoded by them.

---

Yes now I compared it, I got your point.
Thanks for clarifying this :)