Oh, does "there exists" here mean existential quantification (i.e.
∃ ) ?
The behavior does not end in a state sn if there exists a state sn+1 such that the sequence s1 → ... → sn+1 also satisfies condition 2.
Ah, so "
state sn+1" refers not to the next state in the
behavior, but to
some state which satisfies condition 2?
How does this help? Suppose the behavior is safe (it satisfies condition 2), and has also ended, so the behavior's next state (as well as all of its other future states) is the same state as s_n. What prevents me from choosing s_n as the state to use as the s_{n+1} state here? After all, it satisfies condition 2, and so would trivially make all safe behaviors weakly fair... what am I missing?