1: In this section we introduce a compositional notion
2: of simulation of automata which has a close relation to
3: work on simulations and bisimulations
4: (see~\cite{abramsky:interaction_categories},~\cite{CS:sync_async},
5: and~\cite{JNW:bisim_open}).
6: We will also indicate how simulations can be
7: used to facilitate model checking.
8:
9: \subsection{Comparison of Automata}
10: \label{section:comparison}
11:
12: We begin by defining reflexive graph morphisms. Denote a
13: reflexive graph~$G$ by the pair~$(V,E)$ comprising its set of
14: vertices~$V$ and its set of edges~$E$. A
15: \termdef{reflexive graph morphism}~$f$ from~$G=(V,E)$ to~$G'=(V',E')$
16: consists of functions~$f_V\colon V \to V'$ and~$f_E\colon E \to E'$
17: such that sources and targets of edges are preserved,
18: as are reflexive edges.
19:
20: Suppose~$(S,(X_i, \mu_i)_{i \in I})$ and~$(T,(X_i, \nu_i)_{i \in I})$
21: are two automata with the same boundary action sets~$(X_i)_{i \in I}$.
22: A \termdef{comparison}~$f$ from~$S$ to~$T$ is a reflexive graph
23: morphism~$f$ from~$S$ to~$T$ which preserves
24: the actions on the boundaries -- that is, for each~$i \in I$,
25: we have~$\nu_i \cdot f = \mu_i$. We shall term the function comprising the
26: action of~$f$ on states the \termdef{state map}, and the function comprising
27: the action of~$f$ on motions the \termdef{motion map}.
28:
29: When we are writing automata in the form~$X \to Y$
30: (as two boundary automata),
31: such a comparison is denoted~$f\colon S \compto T\colon X \to Y$,
32: although typically we shall just write~$f\colon S \compto T$ as
33: the boundaries will be
34: understood. In this section we will consider automata
35: equipped with an initial state, and comparisons are asked to
36: preserve initial states.
37:
38: For example, let~$P\colon L \to L$ be the philosopher described in
39: section~\ref{section:dp_automata} (figure~\ref{fig:phil}),
40: let~$P'\colon L \to L$ be the alternative philosopher I depicted
41: in figure \ref{fig:nondet_phil} and let~$P''\colon L \to L$ be the
42: alternative philosopher II depicted in figure~\ref{fig:slow_phil}.
43: There are unique comparisons~$p\colon P' \compto P$,~$q\colon P'' \compto P$
44: and~$r\colon P'' \compto P'$, and these comparisons preserve the
45: initial vertex~$0$.
46:
47: \medskip
48:
49: Action sets, automata and comparisons form what is known as
50: a {\em discrete Cartesian bicategory} (see~\cite{CW:cart_bicat}).
51: Rather than recalling the definition
52: of this complicated algebraic structure, we will only consider
53: the operations relevant to this paper; namely,
54: composition, binding, feedback and product of comparisons.
55:
56: \subsubsection{Composition}
57: \label{section:comparison_composition}
58:
59: Given automata~$R$,~$S$, and~$T \colon X \to Y$, and
60: comparisons~$f \colon R \compto S$ and~$g \colon S \compto T$,
61: we define the \termdef{composite}
62: comparison~$\compose{g}{f}\colon R \compto T$. The composite has
63: state map the composite of the state maps of~$f$ and $g$ and
64: motion map the composite of the motion maps of~$f$ and~$g$ -- both
65: these latter composites being the usual composite of functions.
66: It is routine to check that the composite, so defined, is
67: a comparison~$R \compto T$.
68:
69: In categorical terms, this composite is simply the composite of~$f$
70: and~$g$ in the category of reflexive graphs.
71: In fact, for any two action sets~$X$~and~$Y$ we
72: can form a category~${\bf Aut}(X,Y)$. Its objects are
73: automata of the form~$S\colon X \to Y$ and its arrows are
74: comparisons between these automata.
75:
76: \subsubsection{Binding, feedback and product}
77: \label{section:comparison_bfp}
78:
79: We now describe how the operations on automata described in
80: section~\ref{section:operations} also apply to comparisons. In each
81: case, the data for the operations consists of comparisons between
82: data suitable for the corresponding automata operation.
83:
84: Given automata~$S$ and~$T \colon X \to Y$ and
85: automata~$U$ and~$V \colon Y \to Z$,
86: together with
87: comparisons~$f \colon S \compto T$ and~$g \colon U \compto V$,
88: we define the \termdef{binding} of~$f$~and~$g$ -- a
89: comparison~$\bind{f}{g}\colon \bind{S}{U} \compto \bind{T}{V}$.
90:
91: As described in section~\ref{section:bind}, the state space
92: of~$\bind{S}{U}$ has states consisting of pairs~$(v,w)$ with~$v$
93: a state of~$S$ and~$w$ a state of~$U$, and motions consisting of pairs
94: of motions performing the same action on the common boundary. The
95: comparison~$\bind{f}{g}$ maps the state~$(v,w)$ by mapping~$v$ as~$f$
96: does, and~$w$ as~$g$ does, with the obvious extension to motions.
97:
98: The fact that~$f$ and~$g$ respect the actions of motions on boundaries
99: implies that~$\bind{f}{g}$ maps motions of~$\bind{S}{U}$ to motions
100: of~$\bind{T}{V}$, and it is routine to check we have defined a comparison.
101:
102: \medskip
103:
104: Given automata~$S$ and~$T \colon X \times Y \to Y \times Z$
105: and a comparison~$f \colon S \compto T$,
106: we define the \termdef{feedback} of~$f$ -- a
107: comparison~$\fb{Y}{f} \colon \fb{Y}{S} \compto \fb{Y}{T}$.
108:
109: The state space of~$\fb{Y}{S}$ is that of~$S$, but with motions only
110: those that perform the same action on the two boundaries of~$S$ of type~$Y$.
111: Since~$f$ preserves the actions on boundaries, the image of such a motion
112: under~$f$ is a motion of~$T$ performing the same action on the two boundaries
113: of~$T$ of type~$Y$. Thus the comparison~$f$ restricts to a comparison
114: between the fed back automata, and this latter comparison is~$\fb{Y}{f}$.
115:
116: \medskip
117:
118: Given automata~$S$ and~$T \colon X \to Y$ and
119: automata~$U$ and~$V \colon W \to Z$, together with
120: comparisons~$f \colon S \compto T$ and~$g \colon U \compto V$,
121: we define the \termdef{product} of~$f$~and~$g$ -- a
122: comparison~$\product{f}{g}\colon \product{S}{U} \compto \product{T}{V}$.
123:
124: The product~$\product{f}{g}$ has state (resp. motion) map the product of the
125: state (resp. motion) maps of~$f$ and~$g$. That is, it operates on the
126: state space of~$\product{S}{U}$ componentwise.
127:
128: \subsection{Simulations}
129: \label{section:simulations}
130:
131: If~$S\colon X \to Y$ is an automaton, let~$\reachable{S}\colon X \to Y$
132: denote the reachable subautomaton of~$S$. Note that to give a
133: comparison~$f\colon\reachable{S} \compto T$ is just to give a
134: comparison~$f\colon\reachable{S} \compto \reachable{T}$.
135:
136: By a \termdef{simulation}~$f$ from~$S\colon X \to Y$
137: to~$T\colon X \to Y$ we mean a
138: comparison~$f\colon \reachable{S} \compto \reachable{T}$
139: such that~$f$ satisfies the
140: following `lifting property': for all states~$v$ of $\reachable{S}$
141: and all motions~$e\colon f(v) \to w$ in $\reachable{T}$,
142: there exists a (finite) behaviour of $\reachable{S}$
143: \[
144: \begin{diagram}
145: v=v_0 & \rTo^{e_0} & v_1 & \rTo^{e_1} & \ldots & \rTo^{e_n} & v_{n+1}
146: \end{diagram}
147: \]
148: such that
149: \begin{enumerate}[(i)]
150: \item
151: for~$0 \leq i \leq n-1$, the motion~$f(e_i)$ is the reflexive
152: motion at~$f(v)$
153: \item
154: $f(e_n) = e$
155: \end{enumerate}
156: We say that the automaton~$T$
157: \termdef{simulates~$S$ via~$f$}, and
158: write~$f\colon S \simto T\colon X \to Y$,
159: or merely $f\colon S \simto T$ if the boundaries are understood.
160:
161: \medskip
162:
163: In light of this definition, we should revisit our view of reflexive
164: motions as idling motions. More precisely, we emphasize that reflexive
165: motions are idling {\em at the level of abstraction of the automaton}.
166: When abstracting automata -- that is, constructing comparisons and
167: simulations -- we may have cause to abstract away internal
168: motions which are not germane to the analysis task at hand. Thus
169: reflexive motions may be thought of as representing motions unimportant
170: at the level of abstraction of the automaton, and not necessarily a strictly
171: idle state of the process being modelled.
172:
173: \medskip
174:
175: The proof of the following proposition is straightforward.
176: \begin{proposition}
177: \label{prop:simul_implies_appearance}
178: If there is a simulation $f\colon S \simto T$ then~$S$~and~$T$
179: have the same set of reduced appearances.
180: \end{proposition}
181:
182: Of course, in the above proposition, we are only considering
183: behaviours beginning at initial states.
184: For the connection between this
185: notion of simulation and notions of observational
186: equivalences such as \cite{milner:comm_con},
187: the reader is referred to~\cite{JNW:bisim_open} and~\cite{CS:sync_async}.
188:
189: The comparisons of
190: philosophers~$p\colon P' \compto P$, ~$q\colon P'' \compto P$
191: and~$r\colon P'' \compto P'$ mentioned above are examples of
192: simulations. One class of trivial (but, nevertheless important)
193: simulations is provided by the subautomata reachable from
194: the initial states. That is, for every~$S\colon X \to Y$,
195: the identity graph morphism of $\reachable{S}$ provides a
196: simulation~$1_{\reachable{S}}: S \simto S$.
197:
198: \begin{proposition}
199: \label{prop:sim_deadlocks}
200: Suppose~$f\colon S \simto T$ is a simulation.
201: If~$v$ is a reachable deadlock of~$S$
202: then~$f(v)$ is a reachable deadlock of~$T$.
203: \end{proposition}
204:
205: The above proposition indicates that simulations may be used for
206: detecting deadlocks:
207: given an automaton~$S$ we try to find
208: a simulation~$f\colon S \simto T$
209: where~$\reachable{T}$ has significantly less states
210: than~$\reachable{S}$ (that is,~$\reachable{T}$ is a quotient
211: of~$\reachable{S}$); we then look for deadlocks~$v$ in $\reachable{T}$;
212: if $\reachable{T}$ has no deadlocks, we conclude that neither does~$S$;
213: and if there are deadlocks~$v$ in~$\reachable{T}$, we check to see if there
214: are any among the states~$w \in f^{-1}(v)$ of $\reachable{S}$.
215: We give an example of this process at the end of this section.
216:
217: \medskip
218:
219: Action sets, automata and simulations also form
220: a discrete Cartesian bicategory. The operations
221: composition, binding, product and feedback of comparisons
222: induce the same operations on simulations.
223:
224: \subsubsection{Composition}
225: \label{section:simulation_composition}
226:
227: Given simulations~$f\colon R \simto S$ and~$g\colon S \simto T$
228: where~$R$,$S$, and~$T \colon X \to Y$ are automata,
229: there exists a simulation~$\compose{g}{f}\colon R \simto T$
230: called the \termdef{composite} of~$f$~and~$g$.
231:
232: The composite is formed by composing the
233: comparisons~$\reachable{R} \compto \reachable{S}$
234: and~$\reachable{S} \compto \reachable{T}$ being the data provided for~$f$
235: and~$g$. The requisite lifting property is easily established by first
236: lifting via~$g$, and then lifting each component of this lifting via~$f$.
237:
238: As was the case with comparisons, for any two action sets~$X$~and~$Y$ we
239: can form a category; namely the category~${\bf Sim}(X,Y)$ whose objects
240: are automata with left boundary~$X$ and right boundary~$Y$ and whose
241: arrows are simulations between these automata.
242:
243: \subsubsection{Binding, feedback and product}
244: \label{section:simulation_bfp}
245:
246: Given automata~$S$ and~$T \colon X \to Y$ and
247: automata~$U$ and~$V \colon Y \to Z$, together
248: with simulations~$f \colon S \simto T$ and~$g \colon U \simto V$, we
249: define a simulation~$\bind{f}{g}\colon \bind{S}{U} \simto \bind{T}{V}$
250: called the \termdef{binding} of~$f$ and~$g$.
251:
252: Given a state~$(v,w)$ of~$\reachable{\bind{S}{U}}$, it is clear that~$v$
253: is reachable in~$S$ and~$w$ is reachable in~$U$. Applying~$f$ to~$v$
254: and~$g$ to~$w$ thus yields a pair of states, and the reachability of~$(v,w)$
255: implies this image pair is reachable in~$\bind{T}{V}$. This defines the
256: state map of~$\bind{f}{g}$. The motion map is similarly obtained from~$f$
257: and~$g$.
258:
259: The lifting property is obtained by lifting componentwise. Without loss
260: of generality, the lifted paths have the same length (if not, extend the
261: shorter path by prepending reflexive motions). All but the last
262: motion in each lifting has a reflexive image, and thus will be a motion
263: of~$\bind{S}{U}$. The images of the final motion in each lifting perform
264: a common action on the boundary~$Y$, since we are lifting a motion
265: of~$\bind{T}{V}$. Thus, since~$f$ and~$g$ are comparisons, the
266: lifted motions also agree on their actions on the common boundary.
267:
268: \medskip
269:
270: Given automata~$S$ and~$T \colon X \times Y \to Y \times Z$ and a
271: simulation~$f\colon S \simto T$, we shall construct a
272: simulation~$\fb{Y}{f}\colon \fb{Y}{S} \simto \fb{Y}{T}$
273: called the \termdef{feedback} of~$f$.
274:
275: Given a state~$v$ of~$\reachable{\fb{Y}{S}}$, we have a path from the initial
276: state of~$S$ to~$v$ consisting only of motions performing the same action
277: on the two boundaries of type~$Y$. Such~$v$ is clearly a state
278: of~$\reachable{S}$, and applying~$f$ then gives us a similar
279: path in~$T$, and we see that~$f$ induces a comparison as required.
280:
281: As in the case for binding, the lifting property follows from the property
282: for~$f$ together with the fact that motions with reflexive image clearly
283: perform the same action on the two boundaries of type~$Y$, and the final
284: lifted motion agrees after application of~$f$ and hence before it, since~$f$
285: respects the actions on boundaries.
286:
287: \medskip
288:
289: Given automata~$S$ and~$T \colon X \to Y$
290: and automata~$U$ and~$V \colon W \to Z$, together
291: with simulations~$f \colon S \simto T$ and~$g \colon U \simto V$,
292: we define
293: the \termdef{product} of~$f$ and~$g$, a
294: simulation~$\product{f}{g}\colon \product{S}{U} \simto \product{T}{V}$.
295:
296: Observe
297: that~$\reachable{\product{S}{U}} = \product{\reachable{S}}{\reachable{U}}$,
298: and thus the product of the comparisons underlying the simulations~$f$ and~$g$
299: yields a comparison to underly~$\product{f}{g}$. The lifting is performed
300: componentwise, extending the shorter path by prepending reflexive motions
301: if required.
302:
303: \bigskip
304:
305: It is a crucial aspect of the theory that the operations on designs lift
306: to operations on simulations. Thus, given a design, we can abstract parts
307: of the design (i.e. simulate them with simpler systems) and produce
308: abstractions of the whole system. In the next section we shall indicate how
309: this can be used to support model checking in the concrete example of the
310: dining philosophers.
311:
312: \subsection{Simulations and Dining Philosophers}
313: \label{section:sim_checking}
314:
315: We now indicate how simulations may facilitate the task
316: of model checking.
317:
318: \bigskip
319:
320: Consider the two alternative dining philosophers presented
321: at the end of section~\ref{section:misa_dp} (figures~\ref{fig:nondet_phil}
322: and~\ref{fig:slow_phil}). As noted there, the sizes
323: of the state spaces of these systems which are explored by minimal
324: introspective subsystem analysis grow exponentially with the number
325: of philosophers~$n$.
326:
327: Using these alternative philosophers with the design of the usual dining
328: philosopher systems, we may construct
329: corresponding
330: systems~$\fb{L}{(\bind{P'}{Q})^n}$ and~$\fb{L}{(\bind{P''}{Q})^n}$.
331: We have already noted,
332: however, that there are two simulations~$p\colon P' \simto P$
333: and~$q\colon P'' \simto P$. Thus using the operations of
334: section~\ref{section:simulation_bfp} we can construct
335: simulations
336: \[
337: \tilde{p} = \fb{L}{(\bind{p}{1_{\reachable{Q}}})^n}\colon
338: \fb{L}{(\bind{P'}{Q})^n} \simto \fb{L}{(\bind{P}{Q})^n}
339: \]
340: and
341: \[
342: \tilde{q} = \fb{L}{(\bind{q}{1_{\reachable{Q}}})^n}\colon
343: \fb{L}{(\bind{P''}{Q})^n} \simto \fb{L}{(\bind{P}{Q})^n}.
344: \]
345:
346: Now apply the minimal introspective subsystem analysis to
347: the standard philosopher system (recall the explored state space
348: grows only quadratically with the number~$n$). This analysis
349: will find the unique deadlock~$d$ of $\fb{L}{(\bind{P}{Q})^n}$.
350: Recall from section \ref{section:misa_dp} that this state~$d$ corresponds to
351: each fork being in state~$r$ and each philosopher being in state~$1$.
352:
353: We now know that the only deadlocks of the alternative
354: philosopher systems are contained in $\tilde{p}^{-1}(d)$
355: and $\tilde{q}^{-1}(d)$. It is easy to calculate these
356: sets of states -- for example, a state in $\tilde{p}^{-1}(d)$
357: corresponds to each fork being in state $r$ and
358: each philosopher being in state $1$ or $1'$. In fact,
359: each $v \in \tilde{p}^{-1}(d)$ and each $w \in \tilde{q}^{-1}(d)$
360: is a deadlock of $\fb{L}{(\bind{P'}{Q})^n}$
361: and $\fb{L}{(\bind{P''}{Q})^n}$ respectively,
362: and these are the only deadlocks of these systems.
363:
364: \bigskip
365:
366: What if we want to analyse the dining philosopher system for
367: arbitrary~$n$?
368: With the use of software tools (such a tool is
369: currently being specified and prototyped by the authors),
370: it is reasonably straightforward
371: to construct an automaton~$R: L \to L$, together with
372: a pair of simulations~$f_2 \colon (\bind{P}{Q})^2 \simto R$
373: and~$f' \colon \bind{\bind{P}{Q}}{R} \simto R$.
374:
375: The compositionality of simulations
376: allows us to deduce that for any~$n \geq 2$, there is a
377: simulation~$f_n\colon (\bind{P}{Q})^n \simto R$. We define, inductively,
378: for~$n \geq 2$
379: \[
380: f_{n+1} \colon (\bind{P}{Q})^{n+1} = \bind{\bind{P}{Q}}{(\bind{P}{Q})^n}
381: \simto \bind{\bind{P}{Q}}{R}
382: \simto R
383: \]
384: where the first simulation is~$\bind{1_{\reachable{\bind{P}{Q}}}}{f_n}$ and
385: the second simulation is~$f'$.
386:
387: In other words (from the the point of
388: view of observational equivalence and checking for deadlocks)
389: we can replace a composed sequence
390: of philosophers and forks of any length by the simple system $R$.
391:
392: In the case of checking the dining philosopher system for deadlocks, we first
393: form the
394: simulation~$g = \fb{L}{f_n}\colon \fb{L}{(\bind{P}{Q})^n} \simto \fb{L}{R}$
395: and then note that the automaton~$\fb{L}{R}$ has a unique deadlock~$c$.
396: It is easy to check that the only vertex~$v$ of~$\fb{L}{(\bind{P}{Q})^n}$
397: with the property that~$g(v) = c$ is that corresponding to each philosopher
398: being in state~$1$ and each fork in state~$r$, allowing us to conclude that
399: this is the only deadlock of~$\fb{L}{(\bind{P}{Q})^n}$.
400:
401:
402:
403:
404: