Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers


510 users

0 votes
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?
in # Study-Organisation (Master) by (2.7k points)

1 Answer

+1 vote
Best answer

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


by (162k points)
selected by
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 .

Related questions

Imprint | Privacy Policy