# Meaning of I' in omega automata

I am a bit confused about the meaning the primed version of the initial states in omega automata.

The first time it is used is in the following sentence:

I guess here it is used to make clear that the automata have (potentially) different initial states.

However, the next time it is used is in the context of applying temporal operators on automata:

Is the I' here used to indicate that we take the formula for the initial states and replacing every variable with a primed version of them? If that is the case, the I' simply means that the next state has to be an initial state, right?

Indeed, the meaning of the primed variables may be ambiguous. In general, it is just used to  denote a copy of a variable which may have another value. For instance, for the variables of a current point of time, we may generated primed variables for the next point of time. But that may not always be just the next-time operator, it may also just denote another variable.

For the closure under the temporal operators, the primed variables denote the next point of time, so q' denotes next(q) and I' denotes anyone of the initial states at the next point of time. Hence, the automaton for the F-closure starts in anyone of the original initial states where q is false, and will remain there for a while, and may or may not  set next(q). If q is made true, then the transitions R of the original automaton are enabled.

In the first case that you mention (with the flat formulas), the primed variables are just other variables, not related to the others.
by (166k points)
selected
I understand now, thank you!
It is similar than in maths, where f' may denote the derivative of function f or just a variant of the function f where we modified the value at a particular argument x. You need the context to understand that.