\documentstyle[12pt,twoside,amsfonts,amstex]{article}
\input{macros-course-lectures}

\parskip1.5ex
\parindent0pt

\begin{document}

\lecture{notes11}{Notes 11}{October 16, 1996}

\section{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: \\
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

\subsection{Definitions: State Machine, Executions and Reachability}

A {\em state machine} is a triple $(Q, Q_0, \delta)$, 
where:
\begin{enumerate}
\item 
$Q$ is a nonempty (finite or infinite) set of {\em states}.
\item
$Q_0 \subseteq Q$ is a nonempty subset of the states known as the {\em
start states}.
\item
$\delta \subseteq Q \times Q$ is a binary relation over $Q$.
\end{enumerate}

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 {\em executes\/}, producing
{\em executions}. \\
Starts from any start state, and moves along, following transitions. \\
In this way, it models a computational process. \\
\\
An {\em execution fragment} of a state machine is a finite or infinite
sequence $q_0, q_1, \ldots$ such that
$(q_i,q_{i+1}) \in \delta$ for every $i \geq 0$. \\
\\
An {\em 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 {\em 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. 

\begin{example}
Counter \\
\\
$Q = \naturals$, $Q_0 = \{ 0 \}$ \\
\\
$\delta = \{ (n, n+1) | n \in \naturals \}$ \\
\\
Intuitively, this models a counting process that starts with value $0$
and increments (forever). \\
\\
The reachable states are all of $Q = \naturals$. \\
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. \\
\end{example}

The counter is an example of a special kind of state machine that we
call {\em 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 \in Q$, there is
at most one $q'$ such that $(q,q') \in \delta$. \\
\\
If a state machine isn't deterministic, we say it's {\em
nondeterminisitic}. \\
Means it has choices, either of starting state, transitions, or both. \\
\\
The following is an example of a nondeterministic state machine: \\

\begin{example}
Linear hopscotch, with steps of $12$ and $18$: \\
\\
$Q = \mbox{ integers }$ \\
$Q_0 = \{ 0 \}$ \\
\\
$\delta = \{ (i,i+12) | i \in \integers \} 
\cup \{ (i,i-12) | ... \} 
\cup \{ (i,i+18) | ... \}
\cup \{ (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 \pmod 6 \}$. \\
E.g., $Q_0 = \{ 0, 2 \}$. \\
\end{example}

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 {\em 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. \\

\begin{example}
2-dimensional hopscotch, say with $12$ and $18$ in EW and $9$ and $12$
in NS direction. \\
$Q$: Consists of values for two {\em variables}: \\
$\ms{east-west} \in \integers$, initially $0$ \\
$\ms{north-south} \in \integers$, initially $0$ \\
\\
Formally, $Q$ is the Cartesian product, $\integers \times \integers$.
\\
And $Q_0$ consists of the single pair, $(0,0)$. \\
\\
$\delta$:  \\
All transitions of the following forms: \\
\\
$\ms{move-east}(12)$ \\
Effect: \\
  $\ms{east-west} := \ms{east-west} + 12$ \\
\\
$\ms{move-east}(18)$ \\
Effect: \\
  $\ms{east-west} := \ms{east-west} + 18$ \\
\\
$\ms{move-west}(12)$ \\
Effect: \\
  $\ms{east-west} := \ms{east-west} - 12$ \\
\\
$\ms{move-west}(18)$ \\
Effect: \\
  $\ms{east-west} := \ms{east-west} - 18$ \\
\\
$\ms{move-north}(9)$ \\
Effect: \\
  $\ms{east-west} := \ms{east-west} + 9$ \\
\\
Etc. \\
The names of the transitions are called {\em labels}.  \\
They have no formal significance here, but are convenient for
presenting the state machine.  \\
Formally, $\delta$ consists of all pairs that are described by any of
the little code fragments. \\
A code fragment describes a {\em set} of pairs of states, in an
obvious way. \\
E.g., the first fragment denotes all pairs $(q,q')$, where
$\ms{east-west}$ in $q'$ is 12 more than it is in $q$, and
$\ms{north-south}$ is the same in $q'$ as it is in $q$. \\
\\
Written concisely: $q'.\ms{east-west} = q.\ms{east-west} + 12$,
$q'.\ms{north-south} = q.\ms{north-south}$. \\
\end{example}

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: \\

\begin{example}
2-dim hopscotch on only northeast quadrant: \\
\\
The same as above, only now the two state components $\ms{east-west}$
and $\ms{north-south}$ take on nonnegative values only (values in
$\naturals$). \\
\\
So now we have to be careful -- some of the named transitions can't be
applied in all situations, e.g.: \\
\\
$\ms{move-west}(12)$ \\
Precondition: \\
  $\ms{east-west} \geq 12$ \\
Effect: \\
  $\ms{east-west} := \ms{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. 
\end{example}

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.

\subsection{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. \\
\\
\begin{defin}
An {\em invariant} of a state machine $M$ is any predicate  that is
true of all the reachable states of $M$.
\end{defin}

\begin{example}
In the general 2-dim hopscotch, with initial state $(0,0)$, the
statements that \\
$\ms{east-west}$ is a multiple of $6$, \\
and
$\ms{north-south}$ is a multiple of $3$, \\
are invariants.
\end{example}

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. \\
\\
\begin{example}
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.\ms{east-west}$ is a multiple of $6$ and
$q.\ms{north-south}$ is a multiple of $3$. \\
We must show that $q'.\ms{east-west}$ is a multiple of $6$ and
$q'.\ms{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.\ms{east-west}$ is a multiple of $6$ and $q'.\ms{east-west} =
q.\ms{east-west} + 12$, we also have $q'.\ms{east-west}$ a multiple of
$6$. \\
Also (don't forget) since $q.\ms{north-south}$ is a multiple of $3$
and $q'.\ms{north-south} = q.\ms{north-south}$, we also have
$q'.\ms{north-south}$ a multiple of $3$. \\
\\
QED
\end{example}

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

\begin{example}
Euclid's GCD algorithm: \\
\\
State components: \\
$x, y \in \naturals$, initially arbitrary, subject to:  not both $0$,
$x \geq y$ \\
These are the values for which we want to find the GCD \\
\\
Also need components: \\
$x_1, y_1 \in \naturals$, the current values on which we're working \\
Initially, $x_1 = x$, $y_1 = y$ \\
\\
And a component to hold the final answer: \\
$\ms{answer} \in \naturals \cup \{ \ms{null} \}$, initially
$\ms{null}$. \\
\\
$\delta$: \\
\\
Two kinds of things happen:  recursive calls, and final decisions. \\
\\
$\ms{recursive-call}$ \\
Precondition: \\
  $\ms{answer} = \ms{null}$ \\
  $y_1 \neq 0$ \\
Effect: \\
  $(x_1,y_1) := (y_1,x_1 \bmod y_1)$ \\
\\
$\ms{final-decision}$ \\
Precondition: \\
  $\ms{answer} = \ms{null}$ \\
  $y_1 = 0$ \\
Effect: \\
  $\ms{answer} := x_1$ \\
\\
Want to prove that if $\ms{answer} \neq \ms{null}$ then
$\ms{answer} = \gcd{x}{y}$. \\
\\
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 $\ms{answer} = \ms{null}$. \\
\\
Here, what works is a 2-part invariant:
\begin{enumerate}
\item
If $\ms{answer} \neq \ms{null}$ then $\ms{answer} = \gcd{x}{y}$. \\
\item
If $\ms{answer} = \ms{null}$ then $\gcd{x_1}{y_1} = \gcd{x}{y}$. \\
\end{enumerate}
Now can prove this 2-part invariant by induction. \\
BASE: In initial state, $\ms{answer} = \ms{null}$.  \\
Since $x_1 = x$ and $y_1 = y$, obviously $\gcd{x_1}{y_1} =
\gcd{x}{y}$. \\
\\
INDUCTIVE STEP: \\
Consider cases based on the type of action -- recursive-call or
final-decision. \\
\\
Recursive-call only occurs when $\ms{answer} = \ms{null}$, and it
keeps it $\ms{null}$. \\
So we must show that $\gcd{x_1}{y_1} = \gcd{x}{y}$ 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.x}{q.y}$. \\
Prove $\gcd{q'.x_1}{q'.y_1} = \gcd{q'.x}{q'.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 \bmod 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 \bmod q.y_1$. \\
\\
\\
$\ms{final-decision}$ only occurs when $\ms{answer} = \ms{null}$ and
$y_1 = 0$. \\
After it occurs, $\ms{answer} \neq \ms{null}$. \\
So we must show that $\ms{answer} = \gcd{x}{y}$. \\
We may assume the invariants before the step: \\
$\gcd{q.x_1}{q.y_1} = \gcd{q.x}{q.y}$. \\
Prove $q'.\ms{answer} = \gcd{q'.x}{q'.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'.\ms{answer} = q.x_1$.
\end{example}

This example has illustrated strengthening the hypothesis. \\
Next, another number theory example. \\
  
\begin{example}
Russian peasant's multiplication: \\
\\
The states are composed of variables, all in $\naturals$: \\
$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: \\
\\
$\ms{even}$ \\
Pre: \\
$s$ is even \\
$s > 0$ \\
Eff: \\
$r := 2r$ \\
$s := {s \over 2}$ 

$\ms{odd}$
Pre: \\
$s$ is odd \\
Eff: \\
$a := a + r$ \\
$r := 2r$ \\
$s := {s-1 \over 2}$ \\
\\
The answer is the value in $a$ when $s = 0$. \\
\\
Example execution: \\
\\
\begin{verbatim}
$x$   $y$   $r$   $s$   $a$
 5     9     5     9     0
            10     4     5
            20     2     5
            40     1     5
            80     0    45
\end{verbatim}
Proof: Would like to prove invariant: \\
\\
Invariant 1: If $s = 0$ then $a = x y$. \\
\\
Of course, need to strengthen. \\
Turns out that the key is: \\
\\
Invariant 2: $x y = r s + 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. \\
\\
$\ms{even}$: Doubling $r$ while halving $s$ doesn't change the product
$rs$, and $a$ doesn't change, so easy. \\
\\
$\ms{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 = {q.s - 1 \over 2}$, and $q'.a = q.a + q.r$. \\
So $(q'.r)(q'.s) + q'.a = 2 (q.r)({ q.s - 1 \over 2 }) + q.a + q.r$. \\
Reorganizing terms yields $(q.r)(q.s) + q.a$, which suffices. \\
\end{example}

Now an algorithm based on ordering:

\begin{example}
Bubble sort \\
\\
Fix $n \geq 2$. \\
State has: \\
$a$, a length $n$ sequence of integers, write components $a(1), a(2),
\ldots a(n)$. \\
Initially arbitrary. \\
$i$, $j$, pointers in range $[2,n+1]$, initally $2$ \\
\\
Only one type of transition: \\
\\
$\ms{compare}$ \\
Precondition: \\
$j \leq n$
Effect:
if $a(j-1) \leq a(j)$ then $i, j := i+1$ \\
else 
\hspace{2mm} interchange $a(j-1)$ and $a(j)$ \\
\hspace{2mm} 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: \\
\begin{enumerate}
\item
$2 \leq j \leq i \leq n+1$
\item
$a(1), \ldots, a(j-1),a(j+1), \ldots, a(i)$ is sorted. \\
(That is, all elements up to $i$, except possibly for the $j$th
element, are in sorted order.) 
\item
$a(j) \leq a(k)$ for all $k$, $j+1 \leq k \leq i$. \\
(That is, the $j$th element is in the right place with respect to the
elements in higher-numbered positions -- up to $i$th position.)
\end{enumerate}
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 $j$th
element is already in the right position relative to all others, total
order for $a(1), \ldots, 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. 
\end{example}

Now some graph algorithms.

\begin{example}
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: \\
\\
$\ms{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) \in E$ \\
$E := E \cup \{ (v,w) \mid w \in W \} - \{ (w,v) \mid w \in 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 {\em all} edges incoming to
$v$.
\end{example}

\begin{example}
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 {\em
weight}, $\ms{weight}(v,w)$. \\
(Could be different from $\ms{weight}(w,v)$.) \\
Finally, each node $v$ has a path-weight estimate, $\ms{pweight}(v)$, either
a nonnegative real or $\infty$. \\
Initially, $\ms{pweight}(v0)$ is set to $0$, and all the others are
$\infty$. \\
\\
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$: \\
\\
$\ms{improve}(w,v)$ \\
Pre: \\
$(w,v) \in E$ \\
$\ms{pweight}(w) + \ms{weight}(w,v) < \ms{pweight}(v)$ \\
Eff: \\
$\ms{pweight}(v) := \ms{pweight}(w) + \ms{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 $\ms{pweight}(v) \neq \infty$, then
$\ms{pweight}(v)$ is
the total weight of some path from $v0$ to $v$. \\
\\
Prove by induction as usual. \\
BASE:  Only non-$\infty$ node is $v0$, and there is a path of total
weight $0$. \\
INDUCTIVE STEP: \\
By inductive hypothesis, $\ms{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$.
\end{example}

\begin{example}
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.
\end{example}

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

\begin{example}
Token-based leader election, in a ring of proceses. \\
\\
Imagine a collection of processes numbered $1,\ldots, n$, arranged in
a ring (mod $n$). \\
Want to elect exactly one as a leader. \\
Each starts with a {\em 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 \leq i \leq n$: \\
$\ms{val}(i)$, $i$'s identifier (initially, all are unique) \\
$\ms{buffer}(i,i+1 \bmod n)$, a finite sequence, initially containing
just $\ms{val}(i)$ \\
$\ms{leader}(i)$, a Boolean, initially $\ms{false}$ \\
\\
$\ms{move}(i)$ \\
Pre: $\ms{buffer}(i-1,i)$ is nonempty \\
Eff: \\
let $t$ be the first element in $\ms{buffer}(i-1,i)$ \\
remove it from the buffer \\
if $t > \ms{val}(i)$ then add $t$ to end of $\ms{buffer}(i,i+1)$ \\
if $t = \ms{val}(i)$ then $\ms{leader}(i) := \ms{true}$ \\
\\
\\
We would like to prove that exactly one $\ms{leader}(i)$ flag gets
set. \\
For now, we'll content ourselves with just showing that {\em at
most\/} one flag is set. \\ 
\\
Invt1: At most one $\ms{leader}(i)$ is $\ms{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 $\ms{val}(i)$ is in $\ms{buffer}(j,j+1)$, then
$\ms{val}(i)$ is greater than all of $\ms{val}(i+1), \ms{val}(i+2),
\ldots, \ms{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 {\em somewhere} in the state. \\
\end{example}

And a final example:
\begin{example}
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: \\
$\ms{buf}_1$, a finite sequence of $M$ elements, initially arbitrary,\\
$\ms{work-buf}_1$, same, initially equal to $\ms{buf}_1$ \\
(This captures the remaining messages to be sent.) \\
$\ms{tag}_1 \in \{ 0, 1 \}$, initially $1$. \\
\\
$\ms{buf}_2$, a finite sequence of $M$ elements, initially empty,\\
$\ms{tag}_2  \in \{ 0, 1 \}$, initially $0$. \\
\\
$\ms{channel}_{1,2}$, a finite sequence of elements of $M \times \{ 0, 1 \}$, 
  initially empty, \\
$\ms{channel}_{2,1}$, a finite sequence of elements of 
  $\{ 0, 1 \}$, initially empty \\
\\
Transitions: \\
\\
$\ms{send}(m,b)_{1,2}$ \\
Pre: \\
$m = \ms{first}(\ms{work-buf}_1)$ \\
$b = \ms{tag}_1$ \\
Eff: \\
add $(m,b)$ to $\ms{channel}_{1,2}$ \\
\\
$\ms{send}(b)_{2,1}$ \\
Pre: \\
$b = \ms{tag}_2$ \\
Eff: \\
add $b$ to $\ms{channel}_{2,1}$ \\
\\
$\ms{receive}(m,b)_{1,2}$ \\
Pre: \\
$(m,b) = \ms{first}(\ms{channel}_{1,2})$ \\
Eff: \\
remove first element \\
if $b \neq \ms{tag}_2$ then \\
\hspace{2mm} add $m$ to $\ms{buf}_2$ \\
\hspace{2mm} $\ms{tag}_2 := \ms{tag}_2 + 1 \bmod 2$ \\
\\
$\ms{receive}(b)_{2,1}$ \\
Pre: \\
$b = \ms{first}(\ms{channel}_{2,1})$ \\
Eff: \\
remove first element of $\ms{channel}_{2,1}$ \\
if $b = \ms{tag}_1$ then \\
\hspace{2mm} remove first element (if any) of $\ms{work-buf}_1$ \\
\hspace{2mm} $\ms{tag}_1 := \ms{tag}_1 + 1 \bmod 2$ \\
\\
\\
Goal invariant, Invt1: \\
$\ms{buf}_2$ is a prefix of $\ms{buf}_1$ \\
\\
Needs intermediate invariant: \\
\\
Let $\ms{tag-sequence}$ be the sequence consisting of elements of
$\ms{channel}_{2,1}$, \\
followed by $\ms{tag}_2$, \\
followed by the tag components of the elements of $\ms{channel}_{1,2}$, \\
followed by $\ms{tag}_1$. \\
\\
Use sequence concatenation notation. \\
\\
Invt2: \\
$\ms{tag-sequence}$ consists of one of the following:
\begin{enumerate}
\item
All $0$'s.
\item
All $1$'s. 
\item
A positive number of $0$'s followed by a positive number of $1$'s.
\item
A positive number of $1$'s followed by a positive number of $0$'s.
\end{enumerate}

This is proved easily by induction (no extra hypotheses needed); talk
through. \\
\\
Also need: \\
\\
Invt3: \\
If $(m,\ms{tag}_1)$ is in $\ms{channel}_{1,2}$, then $m =
\ms{first}(\ms{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 $\ms{tag}_1$ changes and there is something
else already in $\ms{channel}_{1,2}$ with the same tag. \\
But this can't happen, by Invt2 applied before the step.) \\
\\
Finally, need: \\
Invt4: \\
1. If $\ms{tag}_1 \neq \ms{tag}_2$ then: \\
$\ms{buf}_2 \ms{work-buf}_1 = \ms{buf}_1$. \\
2. If $\ms{tag}_1 = \ms{tag}_2$ then \\
$\ms{work-buf}_1$ and $\ms{buf}_2$ are nonempty, \\
$\ms{first}(\ms{work-buf}_1) = \ms{last}(\ms{buf}_2)$, and \\
$\ms{buf}_2 \ms{all-but-first}(\ms{work-buf}_1) = \ms{buf}_1$. \\
\\
Invt4 easily implies the goal Invt1. \\
Also implies that $\ms{work-buf}_2$ is always nonempty when the
$\ms{receive}_1$ occurs for equal tags. \\
\\
Prove Invt4 by induction. \\
BASE:  tags unequal, $\ms{work-buf}_1 = \ms{buf}_1$ and $\ms{buf}_2$
empty. \\
INDUCTIVE STEP: \\
When send, don't change tags or buffers.  So only consider receives.\\
\\
$\ms{receive}(m,b)_{1,2}$: \\
If $b = \ms{tag}_2$, nothing happens, so preserved. \\
If $b \neq \ms{tag}_2$, arriving message is same as first on
$\ms{work-buf}_1$, by Invt3. \\
Change tag to make equal, replicate $\ms{first}(\ms{work-buf}_1)$ at
end of $\ms{buf}_2$. \\
Since concatenation previously held (by inductive hypothesis),
now the modified concat does. \\
\\
$\ms{receive}(b)_{2,1}$ \\
Similar argument. \\
If $b \neq \ms{tag}_1$, nothing happens, preserved. \\
If $b = \ms{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. 
\end{example}

Liveness?  Temporal logic?
Progress functions?

Simulations?

\end{document}

This lecture depends on previously having taught:
Sets, natural numbers
Sequences, concatentation 

Graphs, digraphs, weighted graphs
Acyclic graphs

Trees
Konig's Lemma and applications.

Fox, chickens, melon.

