
\section{\label{trans}Models and Simulations: I. Simple and Extended
Transition Systems}

     State transition models are very often used to give
operational semantics to concurrent systems.  Here transition
models will be assume a less fundamental role---they simply encode
particular CSP processes in a convenient way.
% possibly refer to Jifeng here
The main advantage of a transition model representation is that it
makes available the powerful technique of {\em simulation} (and {\em
bisimulation}) for establishing relationships and equivalences between
processes.  A simulation is a binary relation between the state-spaces of
two transition models, which has some commutative relationship with the
transition behaviour of the models.
% add lots of references.

    There is a great deal of freedom in the definition
of state transition models, especially for encoding
non-deterministic processes.  From our viewpoint, all that really
matters is that useful simulation results should exist between
the types of model chosen.  Three (???) different types of
model will be considered here.

\begin{description}

\item{Simple Transition Models} (TMs) are represented by a tuple
$(S, A, T)$ where $S$ is a state space, $A$ is an alphabet of events,
and $T$ is a transition function.  $T$ is a tertiary relation from
$S \times A \times S$ with the property
\begin{displaymath}
((i, e, i') \in T \land (i, e, i'') \in T) \Rightarrow i' = i''.
\end{displaymath}
Usually $T$ will regarded as a function from $S$ to the space
of {\em partial} functions from $A$ to $S$.  So $T (i)$ denotes
such a partial function---evidently $(e \mapsto i') \in T (i)$
means that the system can move from state $i$ to state $i'$
through occurence of event $e$.

\item{Extended Transition Models} (ETMs) are a generalisation of
TMs which include unlabelled arcs.  They are represented by
a tuple $(S, A, T, U)$.  $S$, $A$ and $T$ have the same role
as for a TM, whereas $U$ is a binary relation on $S$.  $U$
will be treated as a function from $S$ to $\Pow S$.  $U (i)$ is
a set of states to which $i$ can move {\em without} engaging
in any external event.

\item{Acceptance Transition Models} (ATMs) are a second generalisation
of TMs, which introduce non-determinism in a different way.
Represented by the tuple $(S, A, T, W)$, $S$, $A$ and $T$
again follow their definitions for a TM.  $W$ is a function from
$S$ to $\Pow \Pow A$ with the property
\begin{displaymath}
\bigcup_{w \in W (i)} w = \dom T (i).
\end{displaymath}
Informally, when an ATM is in state $i$, it has an associated hidden variable
whose value is some element $w$ of $W (i)$.  If the environment
offers to engage in some event $e$ from $w$, the ATM will accept that
event and undergo the transition defined by $i' = T (i) (e)$ (and choose
a new hidden value from $W (i')$).  But if the environment only
offers events outside $w$, the ATM refuses these events, even if
they are in $\dom T (i)$.
\end{description}

% References for extended transition systems and acceptance trees,
% but emphasise that their semantics aren't necessarily those
% assumed here.

The semantics of these models, and their properties, will be
discussed more fully in the following subsections.  Before that,
I'll try to motivate working with such a variety of different
types of model.

     TMs are good for representing deterministic processes, or
for representing prefix-closed sets of traces.  Deterministic
processes represented as TMs can be composed in parallel in a
straightforward way to build new TMs; conversely
a deterministic process will often factorise cleanly into
two or more parallel deterministic processes.
Equivalences between the trace-sets
represented by two TMs can be established through a particularly
simple type of simulation.  For such reasons it seems wise to
work with TMs whenever they suffice.

    At some stage, however, an abstraction step is needed, where some
internal events are concealed.  This is where an ETM is needed.
A TM yields an ETM in a very straightforward way upon concealment
of some subset of its alphabet.  Unfortunately, ETMs aren't
particularly easy to manipulate.  Also, it isn't very
easy to show what specifications they satisfy.  For example,
their traces aren't encoded in a simple way.

    On the other hand, ATMs are relatively easy to work with---we
will give simple rules for establishing that they satisfy certain
specifications.  In later subsections we give a simulation result
which can be used for establishing that a process represented by an
ETM implements a process represented by an ATM.

    Notice, by the way, that the transition function, $T$, for
both an ETM and an STM satisfies the same restriction as that for
for a TM---one way in which non-determinism {\em won't} be introduced
here is by allowing more than one arc with the same event labelling
to emerge from a state.

\subsection{\label{TM}Simple Transition Models}

     A TM can be viewed as a device for encoding a prefix-closed set of traces:
$\cal T$, say.  We have
\begin{displaymath}
\cal T \subset A^* \land ((s < s' \land s' \in \cal T) \Rightarrow
		          s \in \cal T).
\end{displaymath}
Suppose $\cal S$ is a function from $\cal T$ to some state space $S$.
Define
\begin{displaymath}
{\cal S}^{-1} (i) = \{ \underline{s} \suchthat \cal S (\underline{s}) = i \}
\end{displaymath}
and
\begin{equation}
T (i) = \{ (\setvar{e}, \setvar{j}) \suchthat
	   \exists s:{\cal S}^{-1} (i). \,\, s \concat \langle \setvar{e} \rangle
	   \in {\cal S}^{-1} (\setvar{j}) \}. \label{simple}
\end{equation}
Now $(S, A, T)$ is a simple transition model of $\cal T$ iff
\begin{equation}
\forall i. \,\,  \forall (e, j):T (i).  \,\,
		      \forall s:{\cal S}^{-1} (i). \,\,
			s \concat \langle e \rangle \in {\cal S}^{-1} (j)
\end{equation}
In terms of the transition model, ${\cal S}^{-1} (i)$ is the set of
traces leading the system to state $i$.
$(e, j) \in T (i)$ means that the system
can move from state $i$ to state $j$ by executing event $e$.
The requirement \ref{simple} states that
if the system can get to state
$i$ after some history, then move to state
$j$ by executing $e$ next, then {\em any} history leading
to state $i$ also allows this.
In particular, this implies that $T (i)$ is a partial function.
$\cal S (\langle \rangle)$ is the initial state for the transition
model which generates $\cal T$.

\subsubsection{Specifications \label{sec:TMspec}}

     Suppose $\cal S$ is a partial function from $A^*$ to $S$
satisfying
\begin{eqnarray*}
{\cal S} (\langle \rangle) & = & i, \\
(s \concat \langle e \rangle \mapsto j) \in {\cal S} & \Leftrightarrow &
s \in \dom {\cal S} \land (e \mapsto j) \in T ({\cal S} (s)),
\end{eqnarray*}
then the (deterministic) process generated by $(A, S, T)$
from initial state $i$ satisfies
\begin{displaymath}
\symbol{tr} \in \dom {\cal S}.
\end{displaymath}

\subsubsection{Simulations}

     Suppose $(S, A, T)$ and $(S', A, T')$ are two TMs.  Also, suppose
there exists a relation $R$ from $S$ to $S'$ such that
\begin{equation}
i \infix{R} i' \Rightarrow (\forall (e, j):T (i) \truethat
  (\exists j' \truethat (e, j') \in T' (i') \land j \infix{R} j')).
\end{equation}
Then $R$ is a {\em simulation}, and if $i \infix{R} i'$ the trace set
generated by $(S, A, T)$ from initial state $i$ is a subset of
the trace set generated by $(S', A, T')$ from initial state $i$.
If $R^{-1}$ is also a simulation, then $R$ is a {\em bisimulation},
and the two trace sets are equal.

\subsubsection{\label{compose}Trace predicates, and composition}

     A set of traces can be regarded as a predicate on traces.
A very common form of specification takes the form of the
conjunction of a set of predicates, each applied
to the process's trace restricted to some sub-alphabet.
Suppose we have a specification of the form
\begin{displaymath}
     \bigwedge_n ((\symbol{tr} \restrict A_n) \in {\cal T}_n)
\end{displaymath}
and $(S_n, A_n, T_n)$ is a TM generating ${\cal T}_n$ from
initial state $i_n$.  Then the specification above is equivalent to
\begin{displaymath}
     (\symbol{tr} \restrict (\bigcup_n A_n)) \in \cal T
\end{displaymath}
where $\cal T$ is generated by the TM $(S, A, T)$ with
\begin{eqnarray*}
     A & = & \bigcup_n A_n \\
     S & = & S_1 \times S_2 \times \ldots \\
     T (i_1, i_2, \ldots ) & = &
       \{ (\setvar{e} \mapsto (\setvar{j_1}, \setvar{j_2}, \ldots)) \suchthat
       \bigwedge_n
       \function{Accept} (A_n, T_n, \setvar {e}, i_n, \setvar{j_n}) \}
\end{eqnarray*}
from initial state $(i_1, i_2, \ldots)$.  Here
\begin{displaymath}
\function{Accept} (A, T, e, i, j) \Leftrightarrow
  (\bif (e \in A) \bthen (e \mapsto j) \in T (i) \belse j = i)
\end{displaymath}
\newpage
It may be helpful to present an explicit procedure for constructing
$T (i_1, i_2, \ldots)$.  This procedure may be used in cases
where not {\em too} many systems are being composed.
Note that very often the transition
function is only needed on some subset of the composite state space.
\begin{tabbing}
\hspace{0.5cm} \= \hspace{0.5cm} \= \hspace{0.5cm} \=
\hspace{0.5cm} \= \hspace{0.5cm} \= \kill
\> Construct the set $D = \dom T_1 (i_1) \cup \dom T_2 (i_2) \cup \ldots $ \\
\\
\> For each $e \in D$: \\
\\
\> \> if there is any $k \in \{1, 2, \ldots \}$ such that $e \in A_k$ but
					       $e \not \in \dom T_k (i_k)$ \\
\> \> \> this $e$ isn't in
		    $\dom T (i_1, i_2, \ldots ) $. \\
\\
\> \> Otherwise \\
\> \> \> for each $k$, \\
\> \> \> \> if $e \in A_k$ set $j_k$ to $T_k (i_k) (e)$, or \\
\> \> \> \> if $e \not \in A_k$ set $j_k$ to $i_k$. \\
\> \> \> Add $(e \mapsto (j_1, j_2, \ldots ))$ to $T (i_1, i_2, \ldots )$.
\end{tabbing}


\subsubsection{Association with deterministic CSP processes}

     In CSP, a deterministic process is completely determined by
its traces, so it can also be determined by a TM which generates
those traces from some initial state.  In fact, the set of deterministic
CSP process (one for each initial state in $S$) defined in
this way by $(S, A, T)$ is given by the mutual recursion
\begin{displaymath}
\mu X:A \truethat (e:\dom T (i) \rightarrow X (T (i) (e)))
\end{displaymath}
With this interpretation, the composition operation in the
previous section is just CSP parallel composition.

\subsection{\label{ETM}Extended Transition Models}

     An ETM is a tuple $(S, A, T, U)$.
$T$ is defined in the same way as for a simple TM.
$U$ is a {\em nilpotent} binary relation over $S$.  The
term ``nilpotent'' is used here in a weak sense meaning
\begin{displaymath}
\forall i:S \truethat \exists n:\Nat \truethat \tilde{U}^n \{i\} = \emptyset
\end{displaymath}
where $\tilde{U} X = \bigcup_{i \in X} U (i)$.
We associate a set of CSP processes with an ETM, one
for each element of S (any of which can be chosen
as initial state) by the recursion
\begin{equation}
\mu X:A \truethat P (U (i), \dom T (i), T (i)) (X)    \label{extend}
\end{equation}
where
\begin{eqnarray*}
P (u, v, t) (X) & = & \left\{ \begin{array}{ll} R (v, t) (X),  & u = \emptyset \\
	  Q (u) (X) \ndchoice (Q (u) (X) \choice R (v, t) (X)), & \mbox{otherwise} \end{array}
	       \right. \\
Q (u) (X)    & = & \begin{array}{c} \ndchoice \\ j \in u \end{array} X (j) \\
R (v, t) (X)    & = & (e:v \rightarrow X (t (e)))
\end{eqnarray*}
This definition has been chosen specifically to ensure that concealment
of events has a simple representation.  The nilpotency of $U$ ensures that
the processes defined in \ref{extend} are divergence-free.
Note that a simple TM, interpreted
as a model for a deterministic process, is recovered by
setting $U = \emptyset$.

\subsubsection{Concealment}

     The semantics of the ETM is chosen to facilitate concealement.
If $\symbol{Proc}$ is the set of processes associated with an
ETM $(S, A, T, U)$, and
\begin{displaymath}
\symbol{Proc}' (i) = \function{Proc} (i) \setminus C
\end{displaymath}
for some $C \subset A$, then $(S, A, T', U')$ is an ETM for the system
$\symbol{Proc}'$, where
\begin{eqnarray*}
T' (i) & = & (A - C) \lhd T (i) \\
U' (i) & = & U (i) \cup \ran (C \lhd T (i)).
\end{eqnarray*}

\subsubsection{Simulations}

\def\sim{\infix G}

     In this section we introduce a simulation relation wherebye
the deterministic process associated with some simple TM can implement
the process associated with some ETM.  Of course, this is only
possible if the latter system of processes is also deterministic
(although this may not be obvious in the ETM representation).
Suppose $(S, A, T, U)$ is an ETM and $(S', A, T')$ is a simple TM.
The relation $\sim $ from $S$ to $S'$ is a simulation if
\begin{eqnarray*}
i \sim  i' & \Rightarrow &
  ((\dom T (i) \subset \dom T' (i')) \land \\&&
  (\forall e:\dom T (i) \truethat T (i) (e) \sim  T' (i') (e)) \land \\&&
  (\forall j:U (i) \truethat j \sim  i') \land \\&&
  (U (i) = \emptyset \Rightarrow \dom T (i) = \dom T' (i'))).
\end{eqnarray*}
If $\sim $ is a simulation, and $i \sim  i'$, and $\function{Proc}$ is the
system of processes associated with the ETM, and $\function{Proc}'$ is the
set of process associated with the TM, then
\begin{equation}
\function{Proc} (i) \sqsupseteq \symbol{Proc}' (i') \label{ineq1}
\end{equation}
This kind of simulation isn't a direct generalisation of the traces-model
simulation in section ??.  The inequality here refers to the full refusals
model.  In fact, since $\symbol{Proc}'$ is deterministic, this inequality
implies also equality (because deterministic processes are maximal in
the refusals model), so in the special case $U = \emptyset$, this
simulation is as strong as the previous bisimulation.

