We get a specification $\varphi \in \mathsf{LTL}$ and we translate a real system to some NFA $A$.
The problem is to construct an NFA $A'$ with $L(A) = L(\neg \varphi)$, so we can check for $L(A') \cap L(A) = \emptyset$
Question: When translating a real system, which shouldn't end (i.e like an OS), to a NFA $(Q, \Sigma, \delta, I, F)$, we need to avoid final states $q_f \in F$. But when doing this, we get $L(A) = \emptyset$ since we never accept anything? So how can we avoid this in modelchecking?
In my understanding, this problem can be resolved by making every state a final state. This means, there are no special final states and still, words can be accepted. The steps of a path in the automaton correspond to time steps and when every state is a final one, the 'word' is accepted in every time step, meaning that is is still a valid system.