Omega automata

Question

Suppose the non Deterministic automata is given with input set (a,b). And in the transition different types of input is given. Like on state {p} input is (!a or b) and the transition is on state {q}. Again from state {p} input {a &b } transition is on state {p,q}. Again of the same state on input !b transition is on self loop. How I can construct this type of transition on drawing breakpoint construction or rabin/scott.

Another scenario might be the state is {s0,s2,s3}. And the transition is like on state s0 on i/p a|b it goes s1. on s2 on i/p a|!b it goes s4. On s3 on i/p a it goes on s0. How I would construct this?

If the input will be single. Like only a. Then we can easily be did with on ip a where it goes and on ip !a where it is going. But if it is two variables there can be multiple boolean logic. Like on input a|b or a&!b or a exor b. Anything can be there. How can I interpret this ?

Answer 1

I think that you misunderstand what really an input is. The symbolic representation is used to encode the real inputs which are assignments to the boolean input variables. Thus, having two input variables like a and b, we have the four inputs {a=0,b=0},  {a=0,b=1}, {a=1,b=0},  {a=1,b=1}. If in one state there is a transition labelled with !a|b then this transition can be taken for inputs {a=0,b=0},  {a=0,b=1}, {a=1,b=1}, and if there is another transition labelled with a&b, it can be taken for input {a=1,b=1}. Hence, for the input {a=1,b=1}, both transitions can be taken.  For the subset of breakpoint construction, we considered explicit encodings of the automata, and not the symbolic ones. There are also algorithms for the determinization of the symbolic versions, but that is more difficult (and also implemented in the teaching tools for translating LTL to deterministic automata). The principles behind are the same, but the implementation is more involved for the symbolic versions.