Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

917 questions

1k answers


441 users

0 votes

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

in * TF "Emb. Sys. and Rob." by (260 points)

2 Answers

0 votes
Not necessarily.
by (360 points)
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.
+1 vote
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.
by (142k points)
Imprint | Privacy Policy