Massachusetts Institute of Technology Lecture ?? 6.042J/18.062J: Mathematics for Computer Science October 16, 1996 Professors Nancy Lynch and Tom Leighton

Notes 11

1 State Machines

Now another data type: “state machines”. Uses as the basis for modelling algorithms and physical machines, in order to give precise specifications of their behavior and in order to verify their properties.

Will present: Definitions of state machines, executions, reachability.

Basic examples: Illustrate how to use state machines to represent interesting computational processes. Decomposition of state into variables, for convenience in representation and manipulation. Deterministic vs. nondeterministic state machines.

The introduce the key notion of invariants: Properties that are always preserved by state machines. These are the main tool used in careful reasoning about algorithms and machines.

Show how invariants can be proved. By induction. Some that don’t need strengthening of inductive hypothesis. Others that do. Proofs of invariants in batches.

Examples: Numbers: hopscotch Euclid’s GCD algorithm Russian peasant multiplication

Posets: Bubble sort, or some other sort

Graphs:

2 Lecture ??: Notes 11 Acyclic graph maintenance Breadth-first search, relaxation Distributed algorithms: Leader election Alternating Bit Protocol

If time, say something about: Safety vs. liveness Progress functions. Temporal logic – box and diamond. Simulation relation

1.1 Definitions: State Machine, Executions and Reachability

A state machine is a triple (Q, Q_{0}, δ), where:

1. Q is a nonempty (finite or infinite) set of states.

2. Q_{0} ⊆ Q is a nonempty subset of the states known as the start states.

3. δ ⊆ Q × Q is a binary relation over Q. Don’t confuse with 6.045 FSM’s – these machines need not be finite. Similar to digraphs, but can have self-edges, and has distinguished start states.

The point of a state machine is that it executes, producing executions. Starts from any start state, and moves along, following transitions. In this way, it models a computational process. An execution fragment of a state machine is a finite or infinite sequence q_{0}, q_{1}, … such that (q_{i}, q_{i+1}) ∈ δ for every i ≥ 0. An execution is an execution fragment in which the initial state q_{0} is an element of Q_{0}. A state of Q is said to be reachable if it is the final state of some finite execution.

Simple examples. Begin with a simple state machine with one initial state, no choices of what to do next. Has infinitely many states.

Example 1 Counter

Q = ℕ, Q_{0} = {0}

δ = {(n, n + 1)|n ∈ ℕ}

Intuitively, this models a counting process that starts with value 0 and increments (forever).

The reachable states are all of Q = ℕ. Each natural number n is only reached by an execution with n transitions (n + 1 states). There is only one execution of each number of transitions.

The counter is an example of a special kind of state machine that we call deterministic. This means that it has only a single start state: |Q_{0}| = 1, and each state has at most one successor: for each q ∈ Q, there is at most one q′ such that (q, q′) ∈ δ.

If a state machine isn’t deterministic, we say it’s nondeterminisitic. Means it has choices, either of starting state, transitions, or both.

The following is an example of a nondeterministic state machine:

Example 2 Linear hopscotch, with steps of 12 and 18:

Q = integers Q_{0} = {0}

δ = {(i, i + 12)|i ∈ ℤ} ∪ {(i, i − 12)|...} ∪ {(i, i + 18)|...} ∪ {(i, i − 18)|...}. Thas has many different executions, all leading to states that are multiples of the GCD, which is 6.

Can also vary this machine to allow multiple start states.

E.g., Q_{0} = {i|i = 0 (mod 6)}. E.g., Q_{0} = {0, 2}.

In most examples of state machines that occur in practice, the state has structure. Can describe it as containing different sorts of information, represented as values of state variables. Different from graphs, which are usually thought of as unstructured. (Normally represented by a dot for each vertex, arrow for each edge.) The variable structure leads to concise, understandable representations.

Example 3 2-dimensional hopscotch, say with 12 and 18 in EW and 9 and 12 in NS direction. Q: Consists of values for two variables: east-west ∈ ℤ, initially 0 north-south ∈ ℤ, initially 0

Formally, Q is the Cartesian product, ℤ × ℤ. And Q_{0} consists of the single pair, (0, 0).

δ: All transitions of the following forms:

move-east(12) Effect: east-west := east-west + 12

move-east(18) Effect: east-west := east-west + 18

move-west(12) Effect: east-west := east-west − 12

move-west(18) Effect: east-west := east-west − 18

move-north(9) Effect: east-west := east-west + 9

Etc. The names of the transitions are called labels. They have no formal significance here, but are convenient for presenting the state machine. Formally, δ consists of all pairs that are described by any of the little code fragments. A code fragment describes a set of pairs of states, in an obvious way. E.g., the first fragment denotes all pairs (q, q′), where east-west in q′ is 12 more than it is in q, and north-south is the same in q′ as it is in q.

Written concisely: q′.east-west = q.east-west + 12, q′.north-south = q.north-south.

The transitions above are described using assignment statements. Nice for programmers. Sometimes use equations (like the ones just above) instead.

One more wrinkle: When using code fragments to represent state transitions, sometimes it’s convenient to give a predicate restricting when the code fragment is allowed to be applied:

Example 4 2-dim hopscotch on only northeast quadrant:

The same as above, only now the two state components east-west and north-south take on nonnegative values only (values in ℕ).

So now we have to be careful – some of the named transitions can’t be applied in all situations, e.g.:

move-west(12) Precondition: east-west ≥ 12 Effect: east-west := east-west − 12

The precondition is a predicate on the state variables restricting when the transitions denoted by this code fragment are permitted to occur. Formally, the transitions denoted by this fragment are all (q, q′) for which the precondition predicate is true of q and for which q′ is obtained from q by executing the effect code.

State machine can be used to describe most computing processes, including both algorithms and computing machines.

The state variable structure is usually crucial for obtaining understandable respresentations.

1.2 Invariants

Now we are ready to introduce the main practical method for reasoning about the correctness of algorithms/machines represented as state machines.

Argue that the machine preserves some invariants. This is often the key to understanding what the machine does, and why.

Definition 1.1 An invariant of a state machine M is any predicate that is true of all the reachable states of M.

Example 5 In the general 2-dim hopscotch, with initial state (0, 0), the statements that east-west is a multiple of 6, and north-south is a multiple of 3, are invariants.

Of course, these statements give a lot of insight into what this machine does.

How to prove that some state machine satisfies an invariant? Must be true of all reachable states. Reachable states are those that are reached by some number of transitions, beginning from a start state. So, prove by induction on number of transitions. Breaks down into base, 0 transitions, which shows the property is true in the initial states, and inductive step, which shows the property is preserved by all steps.

Example 6 2-dimensional hopscotch.

Invariant as stated above. Prove by induction

BASE: Initial state (0, 0) multiples of 6, 3 respectively. INDUCTIVE STEP: Suppose true for all states reachable after n steps.

Now consider state reachable after n + 1 steps. That state is reached by an execution with n steps, then one more step. Say the state after n steps is q and the final state is q′. By inductive hypothesis, we may assume that the invariants are true for q. That is, q.east-west is a multiple of 6 and q.north-south is a multiple of 3. We must show that q′.east-west is a multiple of 6 and q′.north-south is a multiple of 3.

Consider cases based on type of transition. (The usual, when the machine is represented by code fragments.)

Here, all the cases are basically the same, so just consider the first. Since q.east-west is a multiple of 6 and q′.east-west = q.east-west + 12, we also have q′.east-west a multiple of 6. Also (don’t forget) since q.north-south is a multiple of 3 and q′.north-south = q.north-south, we also have q′.north-south a multiple of 3.

QED

Do more examples. First, number theory. Then graphs. Then some arising from distributed systems.

Example 7 Euclid’s GCD algorithm:

State components: x, y ∈ ℕ, initially arbitrary, subject to: not both 0, x ≥ y These are the values for which we want to find the GCD

Also need components: x_{1}, y_{1} ∈ ℕ, the current values on which we’re working Initially, x_{1} = x, y_{1} = y

And a component to hold the final answer: answer ∈ ℕ ∪ {null}, initially null.

δ:

Two kinds of things happen: recursive calls, and final decisions.

recursive-call Precondition: answer = null y_{1} ≠ 0 Effect: (x_{1}, y_{1}) := (y_{1}, x_{1} mod y_{1})

final-decision Precondition: answer = null y_{1} = 0 Effect: answer := x_{1}

Want to prove that if answer ≠ null then answer = gcd xy.

Can’t prove just this by induction – not strong enough. Need to strengthen the inductive hypothesis (as usual), this time to say something about the case where answer = null.

Here, what works is a 2-part invariant:

1. If answer ≠ null then answer = gcd xy.

2. If answer = null then gcd x_{1}y_{1} = gcd xy.

Now can prove this 2-part invariant by induction. BASE: In initial state, answer = null. Since x_{1} = x and y_{1} = y, obviously gcd x_{1}y_{1} = gcd xy.

INDUCTIVE STEP: Consider cases based on the type of action – recursive-call or final-decision.

Recursive-call only occurs when answer = null, and it keeps it null. So we must show that gcd x_{1}y_{1} = gcd xy after the step. We may assume this before the step, by inductive hypothesis. That is, assume gcd q.x_{1}q.y_{1} = gcd q.xq.y. Prove gcd q′.x_{1}q′.y_{1} = gcd q′.xq′.y.

This follows because q.x = q′.x, q.y = q′.y, the interesting fact, proved earlier in the course: gcd q.x_{1}q.y_{1} = gcd q.y_{1}q.x_{1} mod q.y_{1}, and the behavior of the code fragment, which ensures that q′.x_{1} = q.y_{1} and q′.y_{1} = q.x_{1} mod q.y_{1}.

final-decision only occurs when answer = null and y_{1} = 0. After it occurs, answer ≠ null. So we must show that answer = gcd xy. We may assume the invariants before the step: gcd q.x_{1}q.y_{1} = gcd q.xq.y. Prove q′.answer = gcd q′.xq′.y.

This follows because q.x = q′.x, q.y = q′.y, the interesting fact that: gcd q.x_{1}0 = q.x_{1}, and the behavior of the code fragment, which ensures that q′.answer = q.x_{1}.

This example has illustrated strengthening the hypothesis. Next, another number theory example.

Example 8 Russian peasant’s multiplication:

The states are composed of variables, all in ℕ: x, y, the values to be multiplied, initially arbitrary positive a, the accumulator for the answer r, s, temporaries

Initially, r = x, s = y, a = 0.

Transitions:

even Pre: s is even s > 0 Eff: r := 2r s := \frac{s}{2}

odd Pre: s is odd Eff: a := a + r r := 2r s := \frac{s−1}{2}

The answer is the value in a when s = 0.

Example execution:

$x$   $y$   $r$   $s$   $a$
 5     9     5     9     0
            10     4     5
            20     2     5
            40     1     5
            80     0    45

Proof: Would like to prove invariant:

Invariant 1: If s = 0 then a = xy.

Of course, need to strengthen. Turns out that the key is:

Invariant 2: xy = rs + a

So, add this one to invt 1 and prove the two together by induction. Or, better, just prove this one by itself, by induction, and then infer invt1 as a trivial corollary.

Proving invt2 is straightforward by induction. BASE: True initially because r = x, s = y and a = 0. INDUCTIVE: Consider cases based on type of action, odd or even.

even: Doubling r while halving s doesn’t change the product rs, and a doesn’t change, so easy.

odd: Assuming (q.x)(q.y) = (q.r)(q.s) + q.a. Must show (q′.x)(q′.y) = (q′.r)(q′.s) + q′.a. Now q′.x = q.x, q′.y = q.y, so LHS unchanged. Also, q′.r = 2(q.r), q′.s = \frac{q.s−1}{2}, and q′.a = q.a + q.r.

So (q′.r)(q′.s) + q′.a = 2(q.r)(\frac{q.s−1}{2}) + q.a + q.r. Reorganizing terms yields (q.r)(q.s) + q.a, which suffices.

Now an algorithm based on ordering:

Example 9 Bubble sort

Fix n ≥ 2. State has: a, a length n sequence of integers, write components a(1), a(2), … a(n). Initially arbitrary. i, j, pointers in range [2, n + 1], initally 2

Only one type of transition:

compare Precondition: j ≤ n Effect: if a(j − 1) ≤ a(j) then i, j := i + 1 else interchange a(j − 1) and a(j) if j > 2 then j := j − 1 else i, j := i + 1

Final invariant will be: If j = n + 1 then a is sorted (in nondecreasing order).

Describe operation informally.

To prove this by induction, need invariants representing partial progress:

1. 2 ≤ j ≤ i ≤ n + 1

2. a(1), …, a(j − 1), a(j + 1), …, a(i) is sorted. (That is, all elements up to i, except possibly for the jth element, are in sorted order.)

3. a(j) ≤ a(k) for all k, j + 1 ≤ k ≤ i.

(That is, the jth element is in the right place with respect to the elements in highernumbered positions – up to ith position.)

Must argue these three invariants are preserved. The first is trivial, prove by itself. Then prove the second and third together. Argue in cases, based on which clause in the effect is followed.

If the first test comes out right, then it means that the jth element is already in the right position relative to all others, total order for a(1), …, a(i). As needed to start next phase with new i.

Otherwise, a single interchange occurs. The new element is correctly ordered with respect to all later elements, after the exchange. And all other elements are still correctly sorted. The final test just says if we are done with this i. LTTR to do carefully. Boring case analysis.

Now some graph algorithms.

Example 10 Acyclic graph.

State is a directed graph G (no self-loops). Represented by components V and E. Initially, it is any acyclic graph (define). Transition: Pick a node with only incoming edges. Reverse all the edges simultaneously:

reverse(v) Precondition: E contains no edge of the form (v, w) Effect: let W be the set of vertices w such that (w, v) ∈ E E := E ∪ {(v, w) | w ∈ W } − {(w, v) | w ∈ W }

Invariant: Graph is always acyclic. Prove by induction. Inductive step: Suppose graph is acyclic. Claim one reversal can’t introduce a cycle. If it did, then one of the new edges inserted by the reversal would have to be involved in the cycle. But each such edge starts at v, so the cycle would have to have an edge that ends with v. But this can’t be, since we are reversing all edges incoming to v.

Example 11 Minimum weight paths (“shortest paths”):

State contains a digraph G again, represented by components V and E. Also v0, a distinguished node in V.

Also, each edge (v, w) in E has a nonnegative real-valued weight, weight(v, w). (Could be different from weight(w, v).) Finally, each node v has a path-weight estimate, pweight(v), either a nonnegative real or ∞. Initially, pweight(v0) is set to 0, and all the others are ∞.

There is only one type of transition, in which one of the vertices, v, improves (lowers) its path weight estimate based on the latest estimate of one of its neighbors, w:

improve(w, v) Pre: (w, v) ∈ E pweight(w) + weight(w, v) < pweight(v) Eff: pweight(v) := pweight(w) + weight(w, v)

Very nondeterministic – this has lots of different executions, depending on which vertices improve based on which neighbors, in which order. What happens? First, at any time, for each vertex that has a finite estimate, the estimate corresponds correctly to some path from v0 to itself. Second, if all vertices keep trying to improve based on all incoming neighbors, then eventually each will have as its estimate the actual minimum-weight of a path from v0 to itself.

The second is a termination property, and invariants aren’t much help in proving termination. So we only concentrate on the first property. This is proved as an invariant:

Invt1: For any v, if pweight(v) ≠ ∞, then pweight(v) is the total weight of some path from v0 to v.

Prove by induction as usual. BASE: Only non-∞ node is v0, and there is a path of total weight 0. INDUCTIVE STEP: By inductive hypothesis, pweight(w) starts out as the total weight of some path from v0 to w. Augment this path with one additional edge to get a path to v.

Example 12 MST Skip for now. State has graph with weights, current forest.

Transition adds in another edge – smallest from some component. Invariant: The current forest is always a subgraph of a MST. Proof: The usual argument forms the inductive step.

Now two examples motivated by distributed algorithms. Represent each as a single state machine.

Example 13 Token-based leader election, in a ring of proceses.

Imagine a collection of processes numbered 1, …, n, arranged in a ring (mod n). Want to elect exactly one as a leader. Each starts with a unique identifier, say a natural number. (Any combination of identifiers can appear in the ring, as long as there are no repeats.)

Each process sends its own identifier clockwise to its neighbor, pass around ring. But: Each process only passes on identifiers greater than its own. If a process receives its own identifer, it elects self leader. (The idea is that only the max uid will succeed in getting all the way around the ring.)

Formally, state consists of, for each i, 1 ≤ i ≤ n: val(i), i’s identifier (initially, all are unique) buffer(i, i + 1 mod n), a finite sequence, initially containing just val(i) leader(i), a Boolean, initially false

move(i) Pre: buffer(i − 1, i) is nonempty Eff: let t be the first element in buffer(i − 1, i) remove it from the buffer if t > val(i) then add t to end of buffer(i, i + 1) if t = val(i) then leader(i) := true

We would like to prove that exactly one leader(i) flag gets set. For now, we’ll content ourselves with just showing that at most one flag is set.

Invt1: At most one leader(i) is true.

Needs strengthening:

Invt2:

Loosely: “A uid in a buffer is greater than the uids of all processes that it has passed.” More formally: If val(i) is in buffer(j, j+1), then val(i) is greater than all of val(i+1), val(i+ 2), …, val(j).

Can prove by induction. Key is that a node only lets the value pass if it’s greater.

Showing some leader is eventually elected is a liveness property; however, showing it can use an auxiliary invariant saying that the maximum uid is always somewhere in the state.

And a final example:

Example 14 Alternating Bit Protocol

A common communication protocol. Sending a sequence of messages from a set M, from process 1 to process 2. Using underlying FIFO communication channels, can lose or duplicate messages. Process 1 keeps sending first message tagged with 1. When process 2 receives, accepts and outputs. Acks repeatedly with tag 1. When process 1 receives 1, starts sending next message, tagged with 0. Process 2 ignores tag 1, until is sees first 0; then accepts and outputs, and then acks repeatedly with 0. Process 1 now waits to receive 0, then goes back to tag 1. Alternates.

The claim is that this causes process 2 to output a prefix of the sequence of process 1. (To see that it gives all requires a liveness argument.)

States: buf_{1}, a finite sequence of M elements, initially arbitrary, work-buf_{1}, same, initially equal to buf_{1} (This captures the remaining messages to be sent.) tag_{1} ∈ {0, 1}, initially 1.

buf_{2}, a finite sequence of M elements, initially empty, tag_{2} ∈ {0, 1}, initially 0.

channel_{1,2}, a finite sequence of elements of M × {0, 1}, initially empty, channel_{2,1}, a finite sequence of elements of {0, 1}, initially empty Transitions:

send(m, b)_{1,2} Pre: m = first(work-buf_{1}) b = tag_{1} Eff: add (m, b) to channel_{1,2}

send(b)_{2,1} Pre: b = tag_{2} Eff: add b to channel_{2,1}

receive(m, b)_{1,2} Pre: (m, b) = first(channel_{1,2}) Eff: remove first element if b ≠ tag_{2} then add m to buf_{2} tag_{2} := tag_{2} + 1 mod 2

receive(b)_{2,1} Pre: b = first(channel_{2,1}) Eff: remove first element of channel_{2,1} if b = tag_{1} then remove first element (if any) of work-buf_{1} tag_{1} := tag_{1} + 1 mod 2

Goal invariant, Invt1: buf_{2} is a prefix of buf_{1}

Needs intermediate invariant:

Let tag-sequence be the sequence consisting of elements of channel_{2,1}, followed by tag_{2}, followed by the tag components of the elements of channel_{1,2}, followed by tag_{1}.

Use sequence concatenation notation.

Invt2: tag-sequence consists of one of the following:

1. All 0’s.

2. All 1’s.

3. A positive number of 0’s followed by a positive number of 1’s.

4. A positive number of 1’s followed by a positive number of 0’s.

This is proved easily by induction (no extra hypotheses needed); talk through.

Also need:

Invt3: If (m, tag_{1}) is in channel_{1,2}, then m = first(work-buf_{1}).

This again follows by induction. Uses Invt2 in the proof. (BASE obvious. If add new message to channel, obvious. Only interesting case is if tag_{1} changes and there is something else already in channel_{1,2} with the same tag. But this can’t happen, by Invt2 applied before the step.)

Finally, need: Invt4:

1. If tag_{1} ≠ tag_{2} then: buf_{2}work-buf_{1} = buf_{1}.

2. If tag_{1} = tag_{2} then work-buf_{1} and buf_{2} are nonempty, first(work-buf_{1}) = last(buf_{2}), and buf_{2}all-but-first(work-buf_{1}) = buf_{1}.

Invt4 easily implies the goal Invt1. Also implies that work-buf_{2} is always nonempty when the receive_{1} occurs for equal tags.

Prove Invt4 by induction. BASE: tags unequal, work-buf_{1} = buf_{1} and buf_{2} empty. INDUCTIVE STEP: When send, don’t change tags or buffers. So only consider receives. receive(m, b)_{1,2}: If b = tag_{2}, nothing happens, so preserved. If b ≠ tag_{2}, arriving message is same as first on work-buf_{1}, by Invt3. Change tag to make equal, replicate first(work-buf_{1}) at end of buf_{2}. Since concatenation previously held (by inductive hypothesis), now the modified concat does.

receive(b)_{2,1} Similar argument. If b ≠ tag_{1}, nothing happens, preserved. If b = tag_{1}, change tag to make unequal, remove first element of work-buf. Since modified concat previously held (by inductive hypothesis), now ordinary concat does.

Liveness? Temporal logic? Progress functions?

Simulations?