Alpern, B., Schneider, F.B. Recognizing safety and liveness. Distrib Comput 2, 117–126 (1987). Is there is a mistake in the proof?

Question

I believe there is a mistake in the proof of Theorem 1 in the article Alpern, B., Schneider, F.B. Recognizing safety and liveness. We assume that $m$ specifies a safety property. We want to show $L(cl(m)) = L(m)$. When proving $L(cl(m))\subseteq L(m)$, the authors state $\alpha[..i]\beta\in L(m)$ since it causes $m$ to visit accepting states infinitely often. However, according to the definition, for a sequence to belong to a language defined by $m$, it shall cause $m$ to visit an accepting state infinitely often.

Based on this reasoning, we can provide a counterexample, e.g., an automaton with an infinite set of accepting states (for example, countably), such that any run visits them infinitely often, but each particular one only once.

So, is there a mistake?

Answer 1

The authors make it clear on page 128 that they use finite-state automata:

However, for our purposes, it will be convenient to specify properties using Buchi automata - finite-state automata that accept infinite sequences

Thus your counterexample does not work in this case.