Leads-To: Examples

\(\leadsto\) Basics

Which of the following are true? Try to answer these questions on your own before looking at the answers.

1. \(P \leadsto P\)
2. \([Q \Rightarrow P] \; \Rightarrow \; (Q \leadsto P)\)
3. \( ((P \leadsto Q) \wedge [Q \Rightarrow R]) \; \Rightarrow \; (P \leadsto R)\)

Answers

All are true.

1. \(P \leadsto P\)

   In terms of paths from sets of states, there is a path of zero hops from every state to itself. So, there is a path from each state in P to a state in P.

2. \([Q \Rightarrow P] \; \Rightarrow \; (Q \leadsto P)\)

   In terms of paths from sets of states, there is a path of zero hops from every state to itself. So, there is a path from each state in Q to a state in Q, and each state in Q is also in P. So, there is a path from each state in Q to a state in P.

3. \( ((P \leadsto Q) \wedge [Q \Rightarrow R]) \; \Rightarrow \; (P \leadsto R)\)

   In terms of paths from sets of states, there is a path from each state in P to a state in Q. Because \([Q \Rightarrow R]\), every state in Q is a state in R. So, there is a path from each state in P to a state in R.

Example: State Transition Diagram

This diagram shows a state transition system with states 1, 2, 3, 4, 5, 6 and two actions shown as transitions colored blue and red. Our convention in drawing these diagrams is that there is exactly one transition for each action from each state, and if the transition is not shown on the graph then that transition is from a state to itself. For example, there is no red edge shown from vertex 5, and the convention is that a red edge from vertex 5 back to itself is not shown.

1. What is always({3, 4, 5, 6})?
2. What is eventually({1, 5, 6})?
3. What is eventually(always({3, 4, 5, 6}))?
4. What is eventually({1, 5, 6})?
5. What is always(eventually({1, 5, 6}))
6. What is always({1, 5, 6})?
7. What is eventually(always({1, 5, 6}))?

Answers

1. What is always({3, 4, 5, 6})?

   One way to find always(P), where P is a set of states, is to inspect each state in P in turn and determine if there is a path from that state to a state that is not in P. There is a path from vertex 3 to vertex 2 which is not in {3, 4, 5, 6} so, 3 is not in always({3, 4, 5, 6}). Similarly 4 is not in always({3, 4, 5, 6}). All paths from vertices 5, 6 remain for ever in the set {3, 4, 5, 6}, and so 5, 6 is in always({3, 4, 5, 6}). Therefore

   always({3, 4, 5, 6}) = {5, 6}

2. What is eventually({5, 6})?

   Every state in P is in eventually(P). So 5, 6 are in eventually({5, 6}). We inspect each state that is not in P and determine if all fair paths from the state reach states 5 or 6.

   A fair path which never reaches 5 or 6 is 1, 3, 2, 4, 1, 3, 2, 4, 1,..... So, 1, 2, 3, 4 are not in eventually({5, 6}).

   Therefore, eventually({5, 6}) = {5, 6}

3. What is eventually(always({3, 4, 5, 6}))?

   always({3, 4, 5, 6}) = {5, 6}
   eventually({5, 6}) = {5, 6}
   So, eventually(always({3, 4, 5, 6})) = {5, 6}.

   A vertex v is in eventually(always(P)) if every infinite fair path from v has the property that the path has a suffix (a tail) in which every vertex in the suffix is in P, i.e., a point in which the path enters P and remains forever thereafter in P.

4. What is eventually({1, 5, 6})?

   The answer is obvious; however, I've gone into detail to illustrate how the four rules for proving leads-to are used.

   {1, 5, 6} is a subset of eventually({1, 5, 6}). What about the other vertices?

   Every red edge from {4} is to a vertex that is not in {4}. Therefore, fair paths that enter {4} will exit {4} eventually. (We could also have used the argument that every blue edge from {4} is to a vertex not in {4}.)

   All edges from {4} are to {1, 5, 6}. Therefore, from the basic property, fair paths will not remain for ever in {4}, and when the paths leave {4} they enter {1, 5, 6}. So {4} \(\leadsto\) {1, 5, 6}.

   {4} \(\leadsto\) {1, 5, 6} implies that {4} is a subset of eventually({1, 5, 6}).

   Using the basic property again, {2} \(\leadsto\) {1, 4, 5, 6}. Using the disjunction property and {4} \(\leadsto\) {1, 5, 6}, we see that {2} \(\leadsto\) {1, 5, 6}.

   Using similar arguments {3} \(\leadsto\) {1, 5, 6}.

   Therefore, eventually({1, 5, 6}) = {1, 2, 3, 4, 5, 6}

5. What is always(eventually({1, 5, 6}))?

   always(eventually({1, 5, 6})) =
   always({1, 2, 3, 4, 5, 6}) =
   {1, 2, 3, 4, 5, 6}

6. What is always({1, 5, 6})?

   always({1, 5, 6}) = {5, 6}

7. What is eventually(always({1, 5, 6}))?

   eventually(always({1, 5, 6})) =
   eventually({5, 6}) =
   {5, 6}

Example: Proving \(\leadsto\) in a program

Program P1

begin
   S0: NOT y   ->   y = True
   S1: y       ->   x, y = x+1, False
   S2: y       ->   x, y = x+1, True
end

Program P2

begin
   S0: NOT y   ->   y = True
   S1: y       ->   x, y = x+1, False
   S2: y       ->   x, y = x+1, True
   S3: y       ->   y = False
end

S0, S1, S2, S3 are statement labels. All commands are executed infinitely often.

Is the following statement true or false for each of programs P1 and P2?

\( (x = 0) \; \leadsto \; (x > 0) \)

Is the following statement true or false for each of programs P1 and P2?

\( \forall n: (x = 0) \; \leadsto \; (x > n) \)

Answers

For program P1:

For all statements s, and all n:

\(\{y \wedge (x = n) \} \; s \; \{ (y \wedge (x = n)) \vee (x > n) \} \)

There exists a statement (for example S2) which is executed infinitely often where

\( \{y \wedge (x = n) \} \quad S2 \quad \{ \neg (y \wedge (x = n)) \} \)

From the above two formulae and the basic rule for \(\leadsto\):

\( (y \wedge (x = n)) \; \leadsto \; (x > n) \)

From the atomic property of \(\leadsto\) and because S0 is executed infinitely often:

\( (\neg y \wedge (x = n)) \; \leadsto \; (y \wedge (x = n)) \)

From transitivity of \(\leadsto\) and the above two formulae:

\( (\neg y \wedge (x = n)) \; \leadsto \; (x > n) \)

From disjunction of left-hand sides of \(\leadsto\) and because \( (x = n) \; \equiv \; ((x = n) \wedge y) \vee (x = n) \wedge \neg y) \)

\( (x = n) \; \leadsto \; (x > n) \)

The formula holds for \(n = 0\), and so:

\( (x = 0) \; \leadsto \; (x > 0) \)

By induction on \(n\) and transitivity of \(\leadsto\):

\( \forall n: \; (x = 0) \; \leadsto \; (x > n) \)

Program P2

These formula are not true for program P2. Here is an infinite fair path in which \(x = 0\) at every state in the path.

Initially: y = true

S3; S1; S2; S0;    S3; S1; S2; S0;    S3; S1; S2; S0; ...

What part of the proof for P1 failed for P2?

The following triple does not hold for program P2.

For all statements s, and all n:

\(\{y \wedge (x = n) \} \; s \; \{ (y \wedge (x = n)) \vee (x > n) \} \)

Why?

Because with the above precondition for statement S3, the above postcondition does not hold because \(x, y = n, False\).

---

K. Mani Chandy, Emeritus Simon Ramo Professor, California Institute of Technology