Thursday, September 26, 2013

Behaviour of finite state systems

The behaviour of finite state systems. Verification. Bisimilarity.

About half of the received assignments (for assignment 1) were handed back. The rest will be returned next class.

Detailed notes have been written by the professor and are available here (PDF). Only the first 7 pages are examinable material.

1Comments on finite state machines¶

Finite state machines can be found in the lexical analysers of compilers.

Incidentally, any program that uses finite datatypes can be represented as a finite state machine.

Verification: proving that a program behaves as expected for all possible inputs. Makes use of the relationship between structure (algebra) and behaviour (co-algebra). Contrast this with testing, in which you try a finite number of inputs and check that you get the correct output.

2Observed behaviour¶

So far, our definition of "behaviour" has been limited to "what strings are recognised by this machine". There is another definition of behaviour we can consider, which includes interactions.

For instance, take a vending machine that dispenses either tea or coffee. (For simplicity, we ignore the fact that it should go back to the initial state after dispensing - we can treat it as a one-time dispenser.) We describe it with the following diagram:

Suppose we're given another vending machine, which can be described by the following (non-deterministic) diagram:

Are these two vending machines the same, in terms of observed behaviour? Clearly not: with the first machine, if we give it a coin, we can then choose either coffee or tea. With the first machine, if we give it a coin, we can again choose either coffee or tea, but sometimes nothing is dispensed unless we choose the other beverage. And yet, if we were to describe these machines in terms of strings, both would be \$C and \$T - so evidently this description fails the capture the subtleties of what's actually going on.

So the above two machines are not observably equivalent. We will formalise this concept in the next section. Before we do that, a quick example of two machines that are observably equivalent:

2.1Labelled transition systems¶

First, we define a labelled transition system as $\mathcal L = (S, \mathcal A, \to)$ where:

• $S$ is the set of states;
• $\mathcal A$ is the set of actions;
• $\to \subseteq S \times \mathcal A \times S$ is a relation. For convenience, instead of writing $(s, a, s') \in \to$, we write $s \overset{a}{\to} s'$. We can think of it as representing a potential transition from state $s$ to state $s'$ to another though action $a$. In order words, $s$ can perform action $a$ to get to $s'$.

Note that actions can be non-deterministic.

2.2Bisimilarity¶

Definition: Given a labelled transition system $\mathcal L = (S, \mathcal A, \to)$, we say that $s$ and $t$ (where $s, t \in S$) are bisimilar if, for every state $s'$ and action $a$ such that $s \overset{a}{\to} s'$ is possible, there is a state $t$ such that $t \overset{a}{\to} t'$ is possible, with $s'$ and $t'$ also being bisimilar; also, we need that for every state $t'$ and action $a$ such that $t \overset{a}{\to} t'$ is possible, there is a state $s$ such that $s \overset{a}{\to} s'$ is possible, with $s'$ and $t'$ being bisimilar.

This definition seems pretty complicated, and even appears to be a circular definition. How can we make sense of it? There are actually 4 different ways. We'll examine each of them in turn, though note that this material is optional. Understanding bisimulation is important, though, and the explanations below may help with that.

2.2.1Co-induction¶

The "co" means that this is kind of like the opposite of induction: instead of starting from the base case and building up, we start with everything and pare down (intersection instead of union at each step).

We define an $n$-indexed family of equivalence relations, denoted by $\sim_n$ (so $\sim_0, \sim_1, \ldots$), inductively. $\forall s, t \in S$, we have that $s \sim_0 t$ (so all states are 0-equivalent). Then, $s \sim_{n+1} t$ if, whenever $s \overset{a}{\to} s'$, then $t \overset{a}{\to} t'$ (and vice versa) where $s' \sim_{n} t'$.

So then we have that $\sim_0 \supseteq \sim_1 \supseteq \cdots \supseteq \sim_n$. Then we define the equivalence relation $\sim$ as follows: $s \sim t$ if and only if $\forall n, s \sim_n t$.

Here's an example:

We know that $s_0 \sim_0 t_0$. What about $s_0 \sim_1 t_0$? Yes, this is also true. However, $s_0 \sim_2 t_0$ is not true, since $s_1$ and $t_1$ are not 1-equivalent, because you can make a $c$ transition from $s_1$ but not from $t_1$.

As an exercise: for every $n$, define a pair of states that are $n$-equivalent but not $n+1$ equivalent, using the above diagrams.

This method removes the apparent circularity in the definition through indexing. However, this method is somewhat clunky, and we don't want to use this in practice.

2.2.2Bisimulation relations¶

Let $R$ be any relation. We say that $R$ is a bisimulation relation (where bisimulation is merely a property that a relation can have) if, whenever $sRt$ and $s \overset{a}{\to} s'$, then $t \overset{a}{\to} t'$, with $s' Rt'$, and vice versa. Then, given any relation, we can check whether or not it is a bisimulation relation.

Finally, we define a new relation $\sim$, expressing bisimilarity, as follows: $s \sim t$ if there exists a bisimulation relation $T$ such that $sRt$. So bisimilarity, as a property of states, is simply the union of all bisimulation relations on those states.

2.2.3Fixed-point theory¶

Let $R$ be the lattice (!!) of all binary relations ordered by inclusion. (So we have the empty relation at the bottom, and the universal relation - the one that relates everything to everything else - at the top.) We define a function $\mathcal F: R \to \mathcal R$ (which takes in a relation and produces a new one) as follows. $s \mathcal F(R) t$ if, whenever $s \overset{a}{\to} s'$, then $t \overset{a}{\to} t'$ and $s'Rt'$ and vice versa.

Theorem: there is a unique greatest fixed point for $\mathcal F$ (i.e., the largest relation $R$ such that $R = \mathcal F(R)$). This relation is a bisimulation. (We will not prove this theorem in class. See the notes for more details.)

Incidentally, automated tools for checking bisimilarity are based on this method.

2.2.4Two-way similarity¶

We define the similarity relation as follows. $s$ simulates $t$ if, whenever $t \overset{a}{\to} t'$, there exists $s'$ such that $s \overset{a}{\to} s'$ and $s'$ simulates $t$.

We say that $s$ and $t$ are in a 2-way simulation if $s$ simulates $t$ and $t$ simulates $s$. Note that this is not quite the same as bisimulation; for example, in the diagram below, the two LTS are clearly not bisimilar, and yet they are 2-way similar.

We can use this definition to create a game-like way of understanding bisimulation. Suppose you're given one machine, and your opponent is given another. If, no matter what move you make, your opponent can make an equivalent move on the other machine, then your opponent's machine simulates your own. However, if your opponent has the ability to switch machines with you at any point, and still you can simulate any move he makes, then the two machines are bisimilar.