I could not understand Question 1. Are you aware that the formula Init /\ [][Next]_vars is true of a behavior if and only if Init is true in the initial state and EVERY SUCCESSIVE PAIR of states in the behavior satisfies Next or is a stuttering step?
Question 2: The formula Init /\ Next, interpreted as a temporal-logic formula, makes an assertion about the first two states of the behavior. It makes no assertion about the subsequent states, so it allows behaviors that do anything else in subsequent states.
Question 3: Actions are ordinary formulas, so there is no need for special rules to reason about them. More precisely, the only special rules needed are the following ones for the prime operator:
- c’ = c if c is a constant