omega automaton

Question

I have a doubt :

Question: FGa∧G¬b into an Lω formula with Co-Büchi (FG) acceptance condition. (3P)

We know that,   G¬ϕ = ¬Fϕ  and

Fϕ = A∃ ({q}, ¬q, q ′ ↔ q ∨ ϕ, FGq) . How the  ¬Fϕ can be represented in A∃ ? Are they, ¬Fϕ and Fϕ the same? Where should we include the negation part in the Automaton?

Answer 1

If you use Fϕ = A∃ ({q}, ¬q, q ′ ↔ q ∨ ϕ, FGq), you get some trouble. You may negate both sides to get G¬ϕ = ¬Fϕ = ¬A∃ ({q}, ¬q, q ′ ↔ q ∨ ϕ, FGq) = A∃ ({q}, ¬q, q ′ ↔ q ∨ ϕ, ¬FGq), but that gives you a deterministic Büchi automaton. 

Why not converting G¬b to a co-Büchi automaton using G¬b = A∃ ({q}, q, q′ ↔ q & ¬b , FGq)? Then, the rest is easy:

FGa∧G¬b = FGa ∧ A∃ ({q}, q, q′ ↔ q & ¬b , FGq) = A∃ ({q}, q, q′ ↔ q & ¬b ,FGa∧FGq) = A∃ ({q}, q, q′ ↔ q & ¬b ,FG(a∧q))

Combin

Comments

I have a doubt about G¬b.

Gϕ = A∃ ({q}, q, q′ ↔ q ∧ ϕ, FGq)

 Is it equal to G¬b?
I mean, is it correct Gb=G¬b?

---

No, it is not. Gb means that b holds at every point of time, and G¬b means that b is always false.

---

Yeah..i got it.. we need to replace ϕ  with ¬b .