Describing state machines mathematically

Question

The short paper "Computer Science and State Machines" by Leslie Lamport seems quite strange to me.
On the one hand, I am surprised to see that an important hardware protocol called "two-phase handshake" can be derived from a trivial program, simply by mathematical substitution.
On the other hand, I think that this example is (and should be) chosen deliberately. What I doubt about is its generality. If this method (i.e., describing state machines mathematically and deriving a protocol from its specification by mathematical substitution) is so fresh that researchers have not developed a general theory, I would like to see more examples.

My question is straightforward:

Is this derivation a coincidence? Could anyone offer more examples or related references?

---

The derivation of the "two-phase handshake" protocol from a trivial program:

The trivial program mentioned above is just to alternately perform the $\mathcal{P}$ and $\mathcal{C}$ operations:

$\mathcal{X}: \textrm{ loop } \mathcal{P} \textrm{ } ; \textrm{ } \mathcal{C} \textrm{ endloop}$

By introducing a variable $pc$ to represent the "program counter", $\mathcal{X}$ can be described as the following state machine:

• $Init_{\mathcal{X}} \triangleq (pc = 0) \land Init_{\mathcal{PC}}$
• $Next_{\mathcal{X}} \triangleq \big( (pc = 0) \land \mathcal{P} \land (pc' = 1) \big) \lor \big( (pc = 1) \land \mathcal{C} \land (pc' = 0) \big)$

where $Init_{\mathcal{X}}$ denotes the set of initial states; $Next_{\mathcal{X}}$ specifies the next-step transition. $Init_{\mathcal{PC}}$ specifies the initial values of the variables in $var_{\mathcal{PC}}$ involved in $\mathcal{P}$ and $\mathcal{C}$. The primed variable ($pc'$ here) is used to represent the modified version of its unprimed counterpart ($pc$ here).

The two-phase handshake protocol can be described as follows, where $p$ and $c$ are initially equal.

\begin{eqnarray} \mathcal{Y} : & \textrm{ process } & Prod: \textrm{ whenever } p = c \textrm{ do } \mathcal{P} \textrm{ } ; \textrm{ } p = p \oplus 1 \textrm{ end} \\ & \Arrowvert & \\ & \textrm{ process } & Cons: \textrm{ whenever } p \neq c \textrm{ do } \mathcal{C} \textrm{ } ; \textrm{ } c = c \oplus 1 \textrm{ end} \end{eqnarray}

Note that process $Prod$ reads $c$ and writes $p$ while $Cons$ reads $p$ and writes $c$. It is not hard to find out that $\mathcal{Y}$ alternately performs $\mathcal{P}$ and $\mathcal{C}$.

The protocol $\mathcal{Y}$ can also be described as a state machine:

• $Init_{\mathcal{Y}} \triangleq (p = c) \land Init_{\mathcal{PC}}$
• $Next_{\mathcal{Y}} \triangleq Prod \lor Cons$
• $Prod \triangleq (p = c) \land \mathcal{P} \land (p' = p \oplus 1) \land (c' = c)$
• $Cons \triangleq (p \neq c) \land \mathcal{C} \land (c' = c \oplus 1) \land (p' = p)$

The amazing observation is:

$\mathcal{Y}$ can be obtained from $\mathcal{X}$ by substituting $p \oplus c$ for $pc$ in their state machines.

Answer 1

There is a general theory here, which was introduced into CS by Robin Milner, which Lamport did not go into.

A state machine is generally given as a triple $(Q \in \mathrm{Set}, q \in Q, f \in I \times Q \to \mathcal{P}(O \times Q))$, consisting of a state set $Q$, an initial state $q$, and a transition relation $f$.

Now, suppose we have two automata $(Q, q, f)$ and $(T, t, g)$. Let's ask a question: when are these automata equivalent? If all we are going to do is take the machines and send them inputs and listen to the outputs, we don't want to require the state sets to be the same (for example, if $(T, t, g)$ is the result of running a DFA minimization algorithm on $(Q, q, f)$).

It turns out that the right notion of equivalence is bisimulation. The idea is that we take two state machines to be the same, if we can produce a relation $R \subseteq Q \times T$, such that

• $(q,t) \in R$
• for all $(q,t) \in R$ and $i \in I$ and $o \in O$ then:
  • for all $q' \in Q$, if $(o, q') \in f(i, q)$, then there is a $t' \in T$ such that $(o, t') \in g(i, t)$.
  • for all $t' \in T$, if $(o, t') \in g(i, t)$, then there is a $q' \in Q$ such that $(o, q') \in f(i, q)$.

This says that if we can figure out any relation such that (a) the initial states are related, and (b) from related initial states, any I/O action the first machine can take can be mimicked by the second machine in a way that keeps you in the relation, and (c) similarly, the first machine can mimic anything the second can do.

Lamport's notation with primes is a way of concisely describing input-output relations. In this case, the state sets are the program counter of the first program, and the two program counters of the second program. The bisimulation relation is $R(pc, (p, c)) \triangleq pc = p \oplus c$, and then the bisimulation conditions follow trivially (since the relation expressions are equal under the subsitution).

The general theory at work is the theory of coinduction. State machines are representions of corecursively defined sets, and bisimulations tell you when two state machines are representations of the same potentially-infinite object.

Incidentally, this paper is written in a rather polemical style. Equally polemically, I'll point out that the style he advocates in this paper simply fails should you ever need to verify part of a program in isolation -- for example, if you want to prove a library implementation correct, or verifying a program using higher-order functions (or even just dynamic linking).

But both of us will use coinduction, nonetheless.