Omega Automata

Question

1) Why are we using the automata definition of FG here? 

2) In solution formula for L2 is considered as :-GF(a & Xa). But why can't we use FG(a&Xa)?

3) If I use GF(a & X(!a & Xa)) how will definition of Automata will change for L1.

4) Is there a deterministic automaton that accepts L1 AND L2? but why?

Can someone please help?

Answer 1

1. The task asked for a Büchi-automaton. Büchi is GF, Co-Büchi is FG.
2. You'd have to negate the inner part as well. FG( ¬a | X¬a) But consider 1.
3. The language should stay the same. Just the translation to a non-nested automata formula might be different.
4. I'm not sure whether I understood the question correctly. The said words can be detected deterministically. When that's done, we set a state variable. We then ensure that it occurs infinitely often by using an appropriate temporal acceptance criterion.

Comments

Yes, it is asking for Buchi automata. We don't have any definition for GF in automata. We only have definitions of FG, G and F in transformation of acceptance conditions. So which definition are we using?

Also can you please explain why FG(a&Xa) is wrong acceptance condition for L2? I am not able to figure out why to negate inside?

---

It's just stepwise moving the backwards-X from the acceptance condition to the transition relation until the acceptance condition is just one state variable.

---

Sorry, but I am not getting how to write the acceptance condition on the basis of L1/L2?