Order to be followed while solving <>[]X in model checking questions attached

Question

For the following model checking questions, are we supposed to apply [] first and then <>on x or it is the other way around?

Answer 1

Not necessarily.

Comments

In general, I would say: Yes, necessarily.

<> tells us to pick a successor and then evaluate the inner formula, [] tells us to evaluate the inner formula for all successors.

So it is a difference, which one we evaluate first. In one case, you find states where at least one successors only has successors with a certain property. In the other case, you find states where all successors have one successor with a certain property.

Let's take in easy example in the Kripke structure we have. Let's arbitrarily say, we have x={s5}, and the formulas <>[]x and []<>x. Consider the state s5. It has one successor, s4, whose all successors (just s5) are in x. But s5 has a successor, s2, that has no successors in x (s1, s6). Thus, s5 satisfies <>[]x but not []<>x.

Answer 2

It depends: For a formula like <>[]a, there is no choice; you first have to compute the states where "a" holds, then those where all successors are in that set, and then the states having at least one successor in the previously computed set.

If you have (<>a) & ([]b), you can compute the states satisfying <>a and []b in any order before computing their intersection.