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

First of all thanks for the explanation.

So as the question also provided some hint that the automaton formula doesn't have to be deterministic so thatswhy the solution for the exam is non deterministic like as you explained. Am I right ?

If I make a deterministic automaton with sink state, would it be also right for the exam problem ?

---

Sure, unless otherwise it is stated that your automaton must not be deterministic, but I cannot image why one should demand that.

---

Totally understood your point.
Thanks a lot :)

---

I have updated my solution as well in the problem, could you please take a look and please let me know if it is correct ?

Could you also please point out mistake if any ?

Thanks in advance .

---

Your automaton formula for Sing(p) is not correct. The state transition diagram you have drawn corresponds with the example solution, but the formula is another one which is not correct. The automaton formula you have given starts also in s0 with a self-loop labeled with !p, then a transition from s0 to s1 labeled with p, but in s1 you can make the self-loop not only with !p but also with p which is not allowed for a singleton signal.

---

Thanks for the clarification.

From your answer I infer the following:
So, earlier I was translating to omega automata by just looking the acceptance condition of Sing(p) and then writing equivalent representation which is given in module 6 omega automata slide 65 (Transformation of Acceptance Conditions) which is wrong.
I just need to see the given automata representation of Sing(p) or the automata drawn above for Sing(p) and just write it in symbolic representation like the states set {S}, the initial condition Q, the transition relation R, and finally the acceptance condition F.

Is this right ?

I have also updated my solution, could you please check if it is correct now ?

---

Your automaton for Sing(p) is still not correct. Now you are using two state variables s1 and s2 and three of the four possible states are actually reachable. Also the conjunction of the two automata you got for Sing(p) and Subset(p,q) should have the conjunction of the transition relations and not their disjunction.

---

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 :)