Why my Automata is FG?

Question

I got an Automaton below by Breakpoint construction:

labels 0:s0,s1; 1:s1,s2; 2:s3; 3:s3; 4:s0; 5:;     // encode Q

labels 0:; 1:s2; 2:; 3:s3; 4:; 5:;     // encode Qf

init 0;

transitions (0,{},,1); (0,{a},,3); (1,{},,3); (1,{a},,2); (2,{},,4); (2,{a},,3); (3,{a},,3); (3,{},,4); (4,{},,1); (4,{a},,5); (5,{a},,5); (5,{},,5);

accept 1,3;

As a type of Automaton, system accepted "FG". But, I would consider it as "GF". Because F holds infinitely often, but not always after sometime. Also, there is a state 5, which is not F state, but system my reach here and be here always after sometime. This also creates doubts. Could you please describe why my Automaton is "FG"?

Is the definition in Wiki is correct https://en.wikipedia.org/wiki/Co-B%C3%BCchi_automaton?

Comments

No answer, but why do you list the labels? They don't help because init, transitions, and accept work with the state is. Also, I find it hard to read  the transitions. Maybe writing it one transition per line helps.

---

What do you mean by "F holds infinitely often"? Fp means, some predicate p holds eventually, but a single F?

---

PS: After looking into the wikipedia article, I bet your confusion comes indeed from F. In the article, it's for the accepting states, in your lecture probably for eventually, as I sketched in my previous comment ;)

---

That were just a exercise system format.)

---

"F holds infinitely often" - mean that there is an Accaptance state that holds.

Answer 1

First of all, just from an automaton, you can't tell how the acceptance condition shall look like. There might be two automata one with FG and one with GF acceptance with the same transitions, states, labels, and initial states. These automata might both be meaningful but accept a different language.

We introduced the breakpoint construction as a way to determinize non-deterministic FG-automata (slide 90 in the automata chapter). Automata with FG-acceptance (Co-Büchi-automata) accept words if the word induced an infinite path consisting of a finite prefix and an infinite suffix, such that the infinite suffix only consists of states satisfying the propositional property. Graphically: While reading the word, we may finitely often enter and leave the states satisfying the propositional property, but after some (finite) time, we stay in these states forever.

Now what's the reason for the breakpoint construction? We want to determinize an FG-automaton. Now imagine, we just applied the Rabin-Scott subset construction. In the subset construction, if we are in a state, then this state represents a set of states of the original automaton where we could have been now. A state in the Rabin-Scott subset construction is accepting if and only if it contains at least one accepting state of the original automaton. Here's the problem: If we now have a sequence of n accepting subset states, this doesn't mean that there is a matching sequence of n accepting states in the original automaton. (See the example on slide 88 and 89) Hence, we introduced the breakpoint construction. It represents a tuple of sets. The first set tell us where we could be in the original automaton. The second tuple tells us which of these states were reached can be reached without interrupting a sequence of accepting states.

To come back to your main question: If we apply breakpoint to an FG-automaton, we get a deterministic automaton that accepts the same language when the acceptance condition is FG. Side fact: There might be automata where different temporal quantifiers won't change the accepted language.

About your automaton: You are right that the FG automaton has an empty language. That does happen. You are right that GF-acceptance would lead to a non-empty language. You are also right that state 5 is a sink state. Runs reaching state 5 are trapped there and won't be accepted. This state represents those situations of the original automaton where there was no matching transition (with the correct label).