W-Automata: Procedure to convert Co-Buchi to liveness

Question

Example: Question 6 a, February 2018.

what is the general procedure/ trick to convert Co-Buchi to liveness?
My understanding is: find the satisfying note with self loop like s1, right now it has only one path from s0 with input {}, now we are creating a new node and introducing non-determinism by branching s0 to s1 and new node for {}. Is this always the procedure?

Comments

This is almost correct. You are right that you just have to duplicate accepting states that are on an accepting loop. The duplicates then become accepting and have no edge back to the non accepting states.

However, you just mentioned self-loops. That is not enough. Also loops involving multiple states need to be considered.

A structured approach to this looks like this: Add a second layer of only accepting states using non-determinism, don't put any edges in the new layer that lead back to the old layer, simplify.

Answer 1

Consider an accepting run through a co-Büchi automaton: Since it must satisfy the acceptance condition FGφ, it must finally end with a loop in φ-states (which may not just be a self-loop). If the φ-states are a strongly connected component (i.e., non-φ-states may reach them, but you cannot go back from the φ-states to the non-φ-states) then FGφ and Fφ means the same.

Otherwise, the trick is as you say and how it is described in the solution of the mentioned exam question: Make a copy of the φ-states that inherit all transitions from non-φ-states towards them, but not those from the new φ-states to the non-φ-states. This makes the automaton nondeterministic, but now you can say that the newly added states should be the accepting states. Why that? The automaton has no new runs, but now the φ-states form a connected component, so that you can replace now FG by F.

Comments

FG means finally always phi holds, F means finally phi holds. it can either once or forever. But in the given  co buchi automaton it has an outgoing edge from s1 to s3 thus going from safe state to non safe state. How it is considered as co buchi automaton?

---

We can declare any set of states as accepting states for co-Büchi (and also other) acceptance conditions. If you consider a run through the considered automaton that will infinitely often use the transition s1->s3, then this run is not accepting. Still, the automaton is a co-Büchi automaton, and it has accepting runs, namely those that will finally reach {s0,s1} and will never leave these states via s1->s3.

The crucial point is that the liveness automaton constructed as described above is equivalent to the co-Büchi automaton in that it forbids exactly to take that transition s1->s3, but it does not remove any previously existing run and neither does it add runs that did not exist before (if we map s1' to s1).