1: The goal of this section is to present {\em automata with boundary} as
2: a model for systems composed from a number of communicating parts.
3: The {\em boundaries} form an integral part of our theory -- all interactions
4: of a system with its environment occur across its boundaries. We
5: discuss {\em behaviours} of an automaton, and how these behaviours
6: appear on boundaries of the automaton. Requirements on automata
7: can be expressed by restricting the behaviours of an automaton as they
8: appear on given boundaries. We describe the operations {\em bind},
9: {\em feedback}, and {\em product} of automata with boundary, enabling
10: larger systems to be built by combining smaller systems in a way that
11: interacts well with behaviours. Importantly, these operations can
12: be represented pictorially as {\em designs}, allowing us to give
13: high level views of systems.
14:
15: As we introduce the basic definitions, we shall present an example
16: illustrating the concepts being defined. We shall use the example
17: of the dining philosophers, much favoured amongst works on distributed
18: systems.
19:
20: \subsection{Automata with Boundary}
21: \label{section:sys_bdry}
22:
23: The use of finite state automata to model transition systems has
24: a long history (see~\cite{arnold:transitions}). In this paper,
25: an automaton will consist of a
26: reflexive graph plus other data. A \termdef{reflexive graph} consists
27: of a directed graph (with parallel edges and loops allowed), together
28: with a specified \termdef{reflexive edge}~$v \to v$ for each
29: vertex~$v$ of the graph. We do not insist that our automata be
30: finite, but all the examples we present are finite. We do restrict
31: our attention to finite automata when considering model checking.
32:
33: A crucial element of our theory is that of {\em boundary}. All
34: boundaries are typed by the kind of synchronization actions which
35: can occur across the boundary. By an \termdef{action set}
36: we mean a finite set~$X$ with a distinguished element, denoted~$\refl$.
37: We refer to elements of~$X$ as \termdef{actions},
38: and~$\refl$ as the {\em trivial}, or {\em reflexive} action.
39:
40: An \termdef{automaton with boundary}~$(S,(X_i,\mu_i)_{i \in I})$ consists
41: of the following data:
42: \begin{enumerate}
43: \item
44: A reflexive graph~$S$, called the \termdef{state space} of the
45: automaton, whose vertices are termed \termdef{states} and
46: whose edges are termed \termdef{motions}.
47: \item
48: A finite set~$I$ indexing the boundaries of the automaton.
49: \item
50: For each~$i \in I$, a \termdef{boundary}~$(X_i, \mu_i)$ consisting
51: of an action set~$X_i$ and a labelling~$\mu_i(e)$ of each
52: motion~$e$ by an element of~$X_i$, such that~$\mu_i(e)$ is trivial
53: if~$e$ is reflexive.
54: \end{enumerate}
55: Note that the state space of the automaton is the reflexive graph~$S$ --
56: it includes not only the states but the motions of the automaton, which
57: provide the cohesion of the states to justify the terminology of a space.
58: We have in mind that the reflexive edges of the state space~$S$ are
59: \termdef{idling} motions - see the comments after the definition of
60: simulation (section~\ref{section:simulations})
61: for a further exploration of this view.
62:
63: The labelling of the motions indicates the
64: actions on the boundaries which accompany given motions, and we require
65: that if the automaton is idling, then it is idling on each boundary. Of course,
66: nontrivial motions (i.e., motions which are not reflexive), may still
67: idle on some or all boundaries. Those motions idling on all boundaries
68: are called \termdef{internal}
69: motions. They reflect the ability of an automaton to change state without
70: this being reflected in its interaction with the environment.
71:
72: We shall occasionally say a motion of~$S$
73: \termdef{performs} an action on a boundary to mean that it is labelled
74: by the specified action on the specified boundary. Note also that
75: while a boundary consists both of the action set~$X$ and the labelling of
76: motions~$\mu$, we shall often speak of the boundary~$X$ when no
77: confusion arises. We shall say the \termdef{type} of a boundary~$(X,\mu)$
78: to mean the action set~$X$.
79:
80: It is also worth noting that to give an action set is precisely to
81: give a reflexive graph with one vertex. That is, the action set may
82: be considered to be an automaton with trivial state. While not explored
83: in this paper, a more general theory of this kind can relax this restriction,
84: and allow one to calculate with boundaries which possess internal state.
85:
86: \subsubsection{Two boundary Automata}
87: \label{section:two_boundary_automata}
88:
89: When dealing with an automaton, we typically focus temporarily on a
90: subfamily of the boundaries over which some operation is being performed --
91: for example the gluing of boundaries (i.e., {\em binding} -- see
92: section~\ref{section:bind} below). Given a subset~$J$
93: of the set~$I$ indexing the boundaries of~$S$, we may write~$S$ as an
94: arrow
95: \[
96: \prod_{j \in J} X_j \rTo^{S} \prod_{k \in I\setminus J} X_k
97: \]
98: and picture the motions of~$S$ as being labelled in the two products via
99: tupling of the labelling on individual boundaries. We shall typically
100: abbreviate to just~$S \colon X \to Y$ when we wish to emphasize the division,
101: rather than the particular boundaries. In this case, we shall term~$X$ the
102: \termdef{left} boundary, and~$Y$ the \termdef{right} boundary, of~$S$. The
103: passage from the product of~$X_i$'s to the single object~$X$ may be seen as
104: the collection of a bundle of wires into a single cable for purposes of
105: hierarchical design. This view gives the connection between automata
106: with boundary and the theory of bicategories (see \cite{KSW:bicat_processes}).
107:
108: This passage between multiple boundary and two boundary automata allows
109: for a more natural and workable definition of the operations on automata,
110: without sacrificing either expressive power or precision.
111:
112: \subsubsection{Pictorial representation of Automata}
113: \label{section:pictures}
114:
115: When describing automata, we typically draw pictures
116: by drawing the state space of the automaton, with edges labelled
117: to indicate the actions performed by the motions.
118: For an automaton~$S \colon X \to Y$, we write
119: the label~$(x|y)$ to indicate the motion performs the action~$x$ on the
120: left boundary and the action~$y$ on the right boundary.
121: We shall omit drawing reflexive edges, as they add no information to the
122: picture -- however the existence of these edges is crucial,
123: as they allow subautomata in bound systems to act independently
124: (see section~\ref{section:bind}, below).
125:
126: We can depict automata with other than two boundaries in a similar manner.
127: For an automaton with boundaries indexed by~$I$, the labels on motions
128: are~\hbox{$I$-tuples} with entries drawn from the types of the corresponding
129: boundary.
130: In this case, we make explicit the correspondence between tuple entries and
131: boundaries.
132:
133: \subsubsection{Automata for the Dining Philosophers}
134: \label{section:dp_automata}
135:
136: For the example of the dining philosophers, we shall present two
137: automata with boundary -- a philosopher and a fork. Each philosopher will
138: have two boundaries (the left and the right fork from her perspective),
139: and each fork will likewise have two boundaries (the philosophers who
140: can manipulate the fork). We shall thus have an action set~$L$, and
141: and automata with boundary~$P \colon L \to L$ (a philosopher)
142: and~$Q \colon L \to L$ (a fork).
143:
144: The action set~$L$ consists of the actions which a philosopher and
145: a fork jointly perform. A given nontrivial action on which a
146: philosopher and a fork synchronize consists of the fork being either
147: picked up or put down. We model this by taking the action
148: set~$L=\{\refl,\lock,\unlock\}$.
149:
150: The philosopher~$P$ is shown in figure~\ref{fig:phil}.
151: The philosopher has four states, corresponding to whether she is
152: attempting to acquire her left fork, acquire her right fork, relinquish
153: her left fork, or relinquish her right fork. The motions
154: between these states are labelled by the boundary actions performed
155: by the motion.
156: \begin{figure}
157: \[
158: \xymatrix
159: {
160: && 0 \ar[rr]^{(\lock|-)}="top" && 1 \ar[dd]^{(-|\lock)}="right" \\
161: L && && && L \\
162: && 3 \ar[uu]^{(-|\unlock)}="left" && 2 \ar[ll]^{(\unlock|-)}="bot"
163: \save
164: "2,5"."left"."top"."bot"."right"*[F-]\frm{} \ar@{-}"2,1" \ar@{-}"2,7"
165: \restore
166: }
167: \]
168: \caption{\label{fig:phil} A Philosopher~$P$}
169: \end{figure}
170:
171: The fork~$Q$ is shown in figure~\ref{fig:fork}. The fork has
172: three states, corresponding to whether it is unacquired (state~$u$),
173: acquired by its left boundary~(state~$l$), or acquired by its right
174: boundary~(state~$r$). Once again, the motions are labelled by
175: the boundary actions they perform.
176: \begin{figure}
177: \[
178: \xymatrix
179: {
180: L & l \ar@/^/[rr]^{(\unlock|-)}="top" &&
181: u \ar@/^/[ll]^{(\lock|-)}="bot" \ar@/_/[rr]_{(-|\lock)} &&
182: r \ar@/_/[ll]_{(-|\unlock)} & L
183: \save
184: "1,2"."top"."bot"."1,6"*[F-]\frm{} \ar@{-}"1,1" \ar@{-}"1,7"
185: \restore
186: }
187: \]
188: \caption{\label{fig:fork} A Fork~$Q$}
189: \end{figure}
190:
191: \subsection{Behaviour of Automata}
192: \label{section:behaviour}
193:
194: For an automaton~$S \colon X \to Y$ and a state~$v_0$ of~$S$,
195: a \termdef{behaviour~$\beta$ of~$S$ with initial state~$v_0$} is
196: a sequence of motions~$(e_0, e_1, \ldots)$ (finite or infinite)
197: of~$S$ such that~$s(e_0) = v_0$ and~$s(e_{k+1}) = t(e_k)$ (for all
198: appropriate~$k$).
199: That is, a behaviour of~$S$ is nothing more than a path in its state
200: space. We write such behaviours
201: \[
202: \beta = v_0 \rTo^{e_0} v_1 \rTo^{e_1} \ldots
203: \]
204:
205: Given a boundary~$(X,\mu)$ of~$S$, any behaviour of~$S$ is reflected
206: on the boundary via~$\mu$. Precisely, by the \termdef{appearance}
207: of a behaviour~$\beta = (e_0, e_1, \ldots)$ on~$X$ we mean the
208: sequence of actions~$(\mu(e_0), \mu(e_1), \ldots)$. We say a
209: \termdef{behaviour of~$S$ on a boundary~$X$} to mean a sequence which is
210: the appearance of some behaviour of~$S$ on~$X$. Finally, we shall
211: refer to \termdef{reduced} appearances and behaviours on boundaries
212: to mean sequences obtained by eliding all trivial actions from
213: an appearance or behaviour.
214: It is crucial to note that a reduced appearance or behaviour need not
215: be an actual appearance or behaviour, as nontrivial motions of~$S$
216: may appear to be trivial actions on a given boundary.
217:
218: An automaton gives rise to a relation between behaviours
219: on its boundaries. Given a behaviour of~$S$ on the boundary~$X$ and
220: a behaviour of~$S$ on the boundary~$Y$, we may say these are related
221: if they are the appearances of the same behaviour of~$S$ on the boundaries
222: in question. It is
223: typical to specify a system by requesting this be a specific relation,
224: or by requesting properties of this relation. For example, performing
225: a given set of actions on the keypad of an automatic teller machine (one
226: of its boundaries) is required to result in cash being dispensed (the
227: action performed by the machine on the boundary with the cash dispenser)
228: and in an amount being deducted from the user's account (the action performed
229: by the machine on its boundary with the bank's account record).
230:
231: For an automaton~$S \colon X \to Y$ and a given state~$v$ of~$S$, by the
232: \termdef{subautomaton of~$S$ reachable from~$v$} we mean the
233: automaton~$S' \colon X \to Y$ with states those states~$v'$ of~$S$ such
234: that exists a behaviour of~$S$ of the form
235: \[
236: v \rTo \ldots \rTo v'
237: \]
238: That is to say, there is a path of motions of~$S$ from~$v$ to~$v'$.
239: The motions of~$S'$ are all motions of~$S$ between states
240: of~$S'$, and the boundaries and labelling of~$S'$ are inherited directly
241: from~$S$.
242:
243: We shall often assign to an automaton~$S$ of interest an initial state --
244: that is, a specified state~$v_0$ of~$S$. In this case we speak
245: merely of \termdef{behaviours of~$S$} to mean behaviours of~$S$ with
246: initial state~$v_0$, and the \termdef{reachable subautomaton} to mean
247: the subautomaton reachable from~$v_0$.
248:
249: The interpretation of time implied by this treatment of behaviour
250: is that of `discretized continuous time' -- there is an underlying
251: continuous time which is being discretely approximated by some fixed
252: time interval. An aspect of this continuity is contained in the use
253: of the motions - each motion represents an atomic transition with
254: the same duration. We distinguish this from a purely `discrete time',
255: in which the motions are atomic processes which may have different
256: durations.
257:
258: Thus while synchronization may be viewed as a real world process which
259: takes variable time - we model an instance of such a synchronization by
260: a behaviour consisting of internal motions bracketed by atomic
261: synchronizing transitions of the same duration.
262:
263: \subsubsection{Behaviour for the Dining Philosophers}
264: \label{section:dp_behaviour}
265:
266: Returning to the dining philosopher example of
267: section~\ref{section:dp_automata}, we choose the state~$0$
268: of the philosopher (figure~\ref{fig:phil}) to be the initial state.
269: A behaviour of the philosopher then consists of a repeating
270: sequence of the cycle ``\lock\ left boundary'', ``\lock\ right boundary'',
271: ``\unlock\ left boundary, ``\unlock\ right boundary'', possibly
272: interspersed with reflexive edges. The reduced appearance on a given
273: boundary is simply an alternating sequence of ``\lock'',``\unlock''
274: actions.
275:
276: With the state~$u$ as initial, a behaviour of the fork
277: (figure~\ref{fig:fork}) consists of a sequence
278: of ``\lock\ boundary'', ``\unlock\ boundary'' pairs, with the boundary
279: possibly differing from pair to pair, and again possibly interspersed
280: with reflexive edges. Again, the reduced appearance on a given boundary
281: is an alternating sequence of ``\lock'',``\unlock'' actions.
282:
283: \subsection{Operations: Binding, Feedback and Product}
284: \label{section:operations}
285:
286: We describe three operations which may be used to construct new
287: automata with boundary from old. In each case, we have a diagrammatic
288: view of the operation, which should be considered to be a {\em design} --
289: an expression in variable, or unimplemented, automata.
290: It is an important feature of the methodology presented here that
291: we can depict operations on systems without depicting the internals
292: of the systems, thus allowing hierarchical design. The connection
293: between the operations discussed here and Hoare's parallel operation
294: is discussed in \cite{KSW:span_graph}, section~4.
295:
296: For each operation, we describe the effect of the operation on
297: behaviours, in the sense that we describe the behaviours of the new
298: system in terms of the behaviours of the given automata. It is an
299: important feature of our theory that the operations on automata work
300: fluidly with the notion of behaviour described in
301: section~\ref{section:behaviour}.
302:
303: Each operation is described here for two boundary automata --
304: as noted in section~\ref{section:two_boundary_automata} this is
305: sufficient to describe it for all automata.
306:
307: \subsubsection{Binding}
308: \label{section:bind}
309:
310: The first operation we consider is binding. Given two
311: automata with a common boundary, say~$S \colon X \to Y$
312: and~$T \colon Y \to Z$,
313: we can produce a new automaton, their \termdef{binding},
314: denoted~$\bind{S}{T}$. A
315: state of~$\bind{S}{T}$ is a pair~$(v,w)$, where~$v$ is a state of~$S$
316: and~$w$ is a state of~$T$. A motion~$(v,w) \to (v',w')$
317: of~$\bind{S}{T}$ consists of a pair~$(e,f)$, where~$e \colon v \to v'$
318: is a motion of~$S$ and~$f \colon w \to w'$ is a motion of~$T$, and
319: such that~$e$ and~$f$ perform the same action on the boundary~$Y$.
320: A given motion~$(e,f)$ of~$\bind{S}{T} \colon X \to Z$ is labelled on
321: the boundary~$X$ by the action~$e$ performs on~$X$ (in~$S$), and is
322: labelled on the boundary~$Y$ by the action~$f$ performs on~$Z$ (in~$T$).
323: If each of~$S$ and~$T$ have initial
324: states~$v_0$ and~$w_0$ respectively, we take~$(v_0,w_0)$ as the initial
325: state of the binding.
326:
327: The binding~$\bind{S}{T}$ thus has states the Cartesian
328: product of the states of~$S$ and~$T$, but motions the subset
329: of the Cartesian product of motions consisting of those on which
330: the automata~$S$ and~$T$ synchronize on the common boundary~$Y$. The
331: reflexive motions of~$T$ allow~$S$ to move independently of~$T$,
332: provided~$S$ is performing trivial actions on the common boundary.
333:
334: Binding models two automata communicating by synchronizing on a
335: common boundary.
336: We draw diagrams of bound systems by connecting the boundaries of
337: the automata being bound.
338:
339: We draw the
340: binding of two automata~$S \colon X \to Y$ and~$T \colon Y \to Z$
341: as follows:
342: \[
343: \xymatrix
344: {
345: X \ar@{-}[r] & \boxedvar{S} \ar@{-}[r] & Y \ar@{-}[r]
346: & \boxedvar{T} \ar@{-}[r] & Z
347: }
348: \]
349:
350: Importantly, binding interacts well with the behaviours of automata:
351: \begin{proposition}
352: Let~$S \colon X \to Y$ and~$T \colon Y \to Z$ be automata with boundary.
353: To give a behaviour~$\beta$ of~$\bind{S}{T}$ is precisely to
354: give a behaviour~$\gamma$ of~$S$ and a behaviour~$\delta$ of~$T$ such
355: that~$\gamma$ and~$\delta$ have the same appearance on~$Y$.
356: \end{proposition}
357:
358: \subsubsection{Feedback}
359: \label{section:feedback}
360:
361: Given an automaton~$S \colon X \times Y \to Y \times Z$, we can ``bind~$S$
362: with itself''. This operation, called \termdef{feedback}, and
363: denoted~$\fb{Y}{S}$, is used to form closed systems by
364: connecting boundaries. We define~$\fb{Y}{S} \colon X \to Z$ to be
365: the automaton with states precisely those of~$S$, and motions those
366: motions~$e$ of~$S$ such that~$e$ performs the same action on the factor~$Y$
367: of its left boundary and the factor~$Y$ of its right boundary. This
368: yields an automaton with left boundary~$X$ and right boundary~$Z$, where
369: the labelling is inherited from~$S$ in the obvious manner. If~$S$
370: has an initial state~$v_0$, we take~$v_0$ as the initial state of the
371: fed back automaton.
372:
373: Just as with binding, feedback may be presented diagrammatically by
374: connecting the fed back boundaries:
375: \[
376: \xymatrix
377: {
378: X & \ar@{}[rd]|*{S}&& \\
379: &&
380: & & Z \ar@{-}[l] \\
381: &&&
382: \save "1,3"."2,2"*[F-]\frm{}="frame" \ar@{-}"1,1" \restore
383: \save "2,2"."1,3" \ar@{-}"2,4"
384: \ar@{-}`l"3,1"`"3,4"`"1,4"|*{Y}`"frame""frame"
385: \restore
386: }
387: \]
388:
389: Again, behaviours of the fed back automaton are easy to calculate:
390:
391: \begin{proposition}
392: Let~$S \colon X \times Y \to Y \times Z$ be an automaton with boundary.
393: To give a behaviour~$\beta$ of~$\fb{Y}{S}$ is precisely to
394: give a behaviour~$\gamma$ of~$S$ such that~$\gamma$ has the same appearance
395: on the factor~$Y$ of the left boundary as on the factor~$Y$ of the
396: right boundary.
397: \end{proposition}
398:
399: \subsubsection{Product}
400: \label{section:product}
401:
402: Given two automata~$S \colon X \to Y$ and~$T \colon Z \to W$, we define
403: the \termdef{product} of~$S$ and~$T$, an
404: automaton~$\product{S}{T} \colon X \times Z \to Y \times W$,
405: in the obvious way -- form the Cartesian product of the states
406: (resp.~motions) of~$S$ and~$T$ to obtain the states (resp.~motions)
407: of~$\product{S}{T}$. Note that the
408: boundaries are likewise formed by Cartesian product -- the product automaton
409: has boundaries those of~$S$ and those of~$T$. The labelling of
410: motion~$(e,f)$ is obtained from the labellings of~$e$ and~$f$.
411: If each of~$S$ and~$T$ have initial
412: states~$v_0$ and~$w_0$ respectively, we take~$(v_0,w_0)$ as the initial
413: state of the product.
414:
415: The product models combining two automata in parallel with no
416: communication between them. As with binding, we note that
417: the reflexive actions in the automata allow the automata to act independently.
418:
419: Diagrammatically, products are shown as follows:
420: \[
421: \xymatrix
422: {
423: X \ar@{-}[r] & \boxedvar{S} \ar@{-}[r] & Y \\
424: Z \ar@{-}[r] & \boxedvar{T} \ar@{-}[r] & W
425: }
426: \]
427:
428: Behaviours of the product are easily characterized:
429:
430: \begin{proposition}
431: Let~$S \colon X \to Y$ and~$T \colon Z \to W$ be automata with boundary.
432: To give a behaviour~$\beta$ of~$\product{S}{T}$ is precisely to
433: give a behaviour~$\gamma$ of~$S$ and a behaviour~$\delta$ of~$T$.
434: \end{proposition}
435:
436: \subsubsection{Structural Automata}
437: \label{section:structural}
438:
439: In addition to the operations on automata, there are a number of constant
440: operations, or ``structural automata'' which are useful for constructing
441: systems. Two examples of note are the identity on a given action set~$X$
442: (figure~\ref{fig:identity}) and the diagonal on a given action set~$X$
443: (figure~\ref{fig:diagonal}).
444:
445: \begin{figure}[h]
446: \[
447: \xymatrix
448: {
449: X && \bullet
450: \ar@(ul,dl)[]_{(x|x)}="left"
451: \rule[-0.6em]{0em}{1.6em}
452: & X
453: \save
454: "left"."1,3"*[F-]\frm{} \ar@{-}"1,1" \ar@{-}"1,4"
455: \restore
456: }
457: \]
458: \caption{\label{fig:identity} The identity automaton on~$X$}
459: \end{figure}
460:
461: The identity automaton on~$X$ has two boundaries of type~$X$.
462: It has a single state,
463: and one motion for each action~$x$ of~$X$,
464: which is labelled by~$x$ on each boundary. The reflexive motion is the
465: motion corresponding to the reflexive action~$\refl \in X$. As its name suggests,
466: the identity automaton is the identity for binding on~$X$. One particular
467: use of identities is to connect similar boundaries by a single wire
468: in a composed system.
469:
470: \begin{figure}[h]
471: \[
472: \xymatrix
473: {
474: X\\
475: && \bullet
476: \ar@(ul,dl)[]_{(x|x|x)}="right"
477: \rule[-0.6em]{0em}{1.6em}
478: & X \\
479: X
480: \save
481: "right"."2,3"*[F-]\frm{} \ar@{-}"1,1"
482: \ar@{-}"1,1"
483: \ar@{-}"3,1"
484: \ar@{-}"2,4"
485: \restore
486: }
487: \]
488: \caption{\label{fig:diagonal} The diagonal automaton on~$X$}
489: \end{figure}
490:
491: The diagonal automaton on~$X$ has three boundaries of type~$X$. It
492: has a single state,
493: and one motion for each action~$x$ of~$X$,
494: which is labelled by~$x$ on each boundary. The reflexive motion is the
495: motion corresponding to the reflexive action~$\refl \in X$. The diagonal automaton
496: is useful for splitting a wire synchronously.
497:
498: \subsubsection{Binding Philosophers and Forks}
499:
500: The binding~$\bind{P}{Q}$ of a single philosopher and a single
501: fork is shown in figure~\ref{fig:phil_fork} -- we have conserved space
502: a little by abbreviating~\lock\ and~\unlock\ to \al\ and \au\ respectively.
503: The initial state of the bound system is the state~$(0,u)$.
504: \begin{figure}
505: \[
506: \xymatrix
507: {
508: && (0,l) \ar[dd]_{(\al|\refl)}="left"
509: && (0,u) \ar[dd]_{(\al|\refl)} \ar@/^/[rr]^{(\refl|\al)}="top"
510: \ar[ddrr]|(.3){(\al|\al)}
511: && (0,r) \ar[dd]^{(\al|\refl)}="right" \ar@/^/[ll]^{(\refl|\au)}
512: \ar[ddll]|(.3){(\al|\au)}
513: && \\ &&&&&&&&\\
514: && (1,l)
515: && (1,u) \ar@/^/[rr]^{(\refl|\al)} \ar[ddll]^(.3){(\refl|\refl)}
516: && (1,r) \ar@/^/[ll]^{(\refl|\au)}
517: && \\
518: L &&&&&&&& L\\
519: && (2,l) \ar[dd]_{(\au|\refl)}
520: && (2,u) \ar[dd]_{(\au|\refl)} \ar@/^/[rr]^{(\refl|\al)}
521: \ar[ddrr]|(.3){(\au|\al)}
522: && (2,r) \ar[dd]^{(\au|\refl)} \ar@/^/[ll]^{(\refl|\au)}
523: \ar[ddll]|(.3){(\au|\au)}
524: && \\ &&&&&&&&\\
525: && (3,l) \ar`r[ru]`[uuuuuurr]_(.3){(\refl|\refl)}[uuuuuurr]
526: && (3,u) \ar@/^/[rr]^{(\refl|\al)}
527: && (3,r) \ar@/^/[ll]^{(\refl|\au)}="bot"
528: &&
529: \save
530: "4,5"."top"."left"."right"."bot"*[F-]\frm{} \ar@{-}"4,1" \ar@{-}"4,9"
531: \restore
532: }
533: \]
534: \caption{\label{fig:phil_fork} The binding of a philosopher and a fork}
535: \end{figure}
536: There are several points to note about the bound system
537: \begin{itemize}
538: \item
539: Motions where the automata have synchronized have become
540: internal motions (i.e., motions that perform trivial
541: actions on both boundaries). In general, synchronizing two motions
542: which perform trivial actions on all boundaries that are
543: not being synchronized will produce an internal motion.
544: \item
545: Not all states are reachable from the initial state. Thus
546: one often considers the reachable subautomaton of a bound system.
547: \item
548: The model allows for true concurrency,
549: not just interleaving semantics. A motion of the bound system such
550: as that labelled~$(\al,\al) \colon (0,u) \to (1,r)$ is truly
551: concurrent, in that the philosopher and the fork change state
552: simultaneously.
553: \end{itemize}
554:
555: The binding~$\bind{P}{Q}$ allows a philosopher and a fork to
556: synchronize on their common boundary by \lock{}ing and \unlock{}ing.
557:
558: \subsection{Designs and Systems}
559: \label{section:designs_systems}
560:
561: The design diagrams we have given for the operations are
562: more than a guide to the intuition behind the operations.
563: These diagrams form a precise algebra for constructing designs.
564: Given a stock of variables for automata with boundaries of given type,
565: we can draw a diagram by juxtaposing automata and connecting boundaries
566: with wires for the operations of binding, feedback and product -- such a
567: diagram is an expression for an automata, which can be evaluated given
568: automata values for the variables. Such an expression is called a
569: \termdef{design}.
570:
571: \subsubsection{The Geometry of Designs}
572: \label{section:geometry}
573:
574: Considering designs as expressions in a precise algebra with the
575: operations of section~\ref{section:operations}, one
576: should ``parenthesize'' such expressions to indicate the
577: desired order of evaluation.
578:
579: Given two automata~$S \colon X \to Y$
580: and~$T \colon X \to Y$, we say they are \termdef{isomorphic} if there
581: is a bijection between states of~$S$ and states of~$T$ and a bijection
582: between motions of~$S$ and motions of~$T$ which respect the source and
583: target of motions and the labelling of motions on the boundaries.
584: One can then prove propositions justifying the diagrammatic manipulations
585: one would like to carry out, and alleviate the need to parenthesize diagrams
586: in most situations.
587:
588: \bigskip
589:
590: For example, one can easily prove that
591: binding is associative (up to isomorphism of automata). Given
592: automata~$S \colon X \to Y$,~$T \colon Y \to Z$ and~$U \colon Z \to W$,
593: we have that
594: \[
595: \xymatrix
596: {
597: X \ar@{-}[r]^{}
598: & \boxedvar{S} \ar@{-}[r] & Y \ar@{-}[r]
599: & \boxedvar{T} \ar@{-}[r]_{} & Z \ar@{-}[r]
600: & \boxedvar{U} \ar@{-}[r]
601: & W \\
602: &&& {\cong} &&& \\
603: X \ar@{-}[r]
604: & \boxedvar{S} \ar@{-}[r] & Y \ar@{-}[r]^{}
605: & \boxedvar{T} \ar@{-}[r] & Z \ar@{-}[r]
606: & \boxedvar{U} \ar@{-}[r]_{}
607: & W \\
608: \save "1,2"."1,4"*!<0.35em,0em>+<1em,1em>\frm{.} \restore
609: \save "3,4"."3,6"*!<0.35em,0em>+<1em,1em>\frm{.} \restore
610: }
611: \]
612: where the dotted boxes indicate the order of binding.
613: Symbolically, $\bind{(\bind{S}{T})}{U}$ and $\bind{S}{(\bind{T}{U})}$
614: are isomorphic.
615:
616: Thus we can draw diagrams when binding many systems with no risk of
617: confusion. Of course, binding is not the only operation we consider, and
618: one can prove propositions relating the different operations:
619: \begin{proposition}
620: Given automata with boundary~$S \colon X \to Y$ and~$T \colon Y \to Z$,
621: we have that
622: \[
623: \xymatrix
624: {
625: X \ar@{-}[r]^{}
626: & \boxedvar{S} \ar@{-}`r[r]`[rdd][dd] & \\
627: & \boxedvar{T}
628: \ar@{-}[r]_{}
629: \ar@{-}`l[ld]`[d][d]
630: & & Z \ar@{-}[l] & {\cong}
631: & X \ar@{-}[r] & \boxedvar{S} \ar@{-}[r] & \boxedvar{T} \ar@{-}[r] & Z \\
632: & Y &
633: \save "1,2"."2,2".*!<0em,-0.3em>+<1em,1em>\frm{.} \restore
634: }
635: \]
636: In symbols, the automata~$\fb{Y}{\product{S}{T}}$ and~$\bind{S}{T}$ are
637: isomorphic.
638: \end{proposition}
639:
640: The following result is termed the middle four interchange law:
641:
642: \begin{proposition}
643: Given automata with boundary~$S \colon X \to Y$, $T \colon Y \to Z$,
644: $Q \colon U \to V$, and~$R \colon V \to W$,
645: we have that
646: \[
647: \xymatrix
648: {
649: X \ar@{-}[r]^{}
650: & \boxedvar{S} \ar@{-}[r] & Y \ar@{-}[r]
651: & \boxedvar{T} \ar@{-}[r]^{} & Z
652: \\
653: U \ar@{-}[r]^{}
654: & \boxedvar{Q} \ar@{-}[r] & V \ar@{-}[r]
655: & \boxedvar{R} \ar@{-}[r]^{}="c12b" & W
656: \\
657: && {\cong} && \\
658: X \ar@{-}[r]
659: & \boxedvar{S} \ar@{-}[r] & Y \ar@{-}[r]
660: & \boxedvar{T} \ar@{-}[r] & Z
661: \\
662: U \ar@{-}[r]
663: & \boxedvar{Q} \ar@{-}[r] & V \ar@{-}[r]
664: & \boxedvar{R} \ar@{-}[r] & W
665: \save "1,2"."1,4"*!<0.4em,0em>+<1em,1em>\frm{.} \restore
666: \save "2,2"."2,4"*!<0.4em,0em>+<1em,1em>\frm{.} \restore
667: \save "1,2"."2,4"*!<0.7em,-0.5em>+<2em,2em>\frm{.} \restore
668: \save "4,2"."5,2"*!<0em,-0.3em>+<1em,1em>\frm{.} \restore
669: \save "4,4"."5,4"*!<0em,-0.3em>+<1em,1em>\frm{.} \restore
670: \save "4,2"."5,4"*!<0.7em,-0.5em>+<2em,2em>\frm{.} \restore
671: }
672: \]
673: In symbols, the automata~$\product{(\bind{S}{T})}{(\bind{Q}{R})}$
674: and~$\bind{(\product{S}{Q})}{(\product{T}{R})}$ are isomorphic.
675: \end{proposition}
676:
677: It is worth noting that the geometry of designs is a purely combinatorial
678: geometry -- the wires are a mechanism for denoting the connection between
679: boundaries, and the curvature and crossing of wires has no effect on
680: the geometry of the design.
681: A precise combinatorial model of designs in an appropriate mathematical
682: context shall be described in a forthcoming paper~\cite{GK:designs}.
683:
684: \subsubsection{Systems are designs with implementation}
685: \label{section:system}
686:
687: By a \termdef{system} we mean a design together with an assignment of
688: an automaton with boundary to each variable in the design, these assignments
689: being compatible with the operations used to evaluate designs. An instance
690: of a variable automaton occurring in a given design is termed a
691: \termdef{component} of the system. Each
692: system has an associated automaton, called the \termdef{composite automaton},
693: or the \termdef{evaluation} of the system, obtained by realising the operations
694: of the design on the assigned automata in accordance with the definition
695: of the operations in section~\ref{section:operations}.
696:
697: While the evaluation of a system may in some sense be seen as the goal
698: of design, inasmuch as the problem of design is to produce an automaton
699: with specific properties, the system itself is far more important from
700: the point of view of analysis. Retaining the design of the final automaton
701: in the system allows us to utilise facts about the construction of the
702: system in order to analyse it -- in section~\ref{section:misa} we shall
703: give an algorithm which uses design information to assist model checking.
704: Given the effort typically devoted to design of a system in real world terms,
705: it seems only rational that a theory of distributed systems retain designs
706: as an element which is both precisely represented and capable of being
707: computed with. For even though
708: the ultimate (external customer) deliverable of a development effort is
709: the compiled code (= evaluated automaton), a development effort is also
710: expected to deliver a design to maintenance engineers in a
711: usable (= analyzable) form.
712:
713: \subsubsection{Subsystems}
714: \label{section:subsystem}
715:
716: Given a system, by a \termdef{subsystem} we mean some subset of the components
717: of the system. Such a subsystem gives rise to an automaton via evaluation,
718: we shall usually abuse terminology and use the term subsystem for this
719: evaluation also.
720:
721: For both binding and product, the states of the constructed automaton are
722: pairs of states of the automata being operated upon. In the case of feedback,
723: the states are states of the fed back automaton. Hence each state of the
724: evaluation of a system gives rise to a state of the automaton associated with
725: each component. We shall refer to states of the automata associated with
726: components as \termdef{local states}, and by contrast refer to a state~$v$
727: of the evaluation of the system as a \termdef{global state} of the system.
728:
729: Further, given a subsystem of
730: some larger system, each state of the evaluation of the system gives rise
731: to a state of the subsystem in the obvious way (subsystem states are
732: tuples of the local states of the components which form the subsystem).
733: We refer to a state of a subsystem arising in this manner as a
734: \termdef{local state} of the subsystem.
735:
736: Similar remarks hold for motions and behaviours, and we shall thus use
737: the terms \termdef{local motion}, \termdef{global motion},
738: \termdef{local behaviour}, and \termdef{global behaviour} for the
739: corresponding concepts.
740:
741: \subsubsection{Dining Philosopher Systems}
742:
743: For any~$n \in \N$, we can form the composite
744: automaton~$\fb{L}{(\bind{P}{Q})^{n}}$ - this automaton has no boundaries,
745: and models a ring of~$n$ philosophers with their~$n$ intervening forks.
746: For example, figure~\ref{fig:phil_3_ring} shows a design for a ring of
747: three philosophers with their forks. This design, together with with
748: assignment of~$P$ and~$Q$ to the automata of figures~\ref{fig:phil}
749: and~\ref{fig:fork} respectively, comprise a system of dining philosophers.
750: \begin{figure}[h]
751: \[
752: \xymatrix
753: {
754: &
755: \boxedvar{P} \ar@{-}[r] & \boxedvar{Q} \ar@{-}[r] &
756: \boxedvar{P} \ar@{-}[r] & \boxedvar{Q} \ar@{-}[r] &
757: \boxedvar{P} \ar@{-}[r] & \boxedvar{Q}
758: \ar@{-}`r[r]`[d]`[dllllll]`[llllll][lllll] & \\
759: &&&&&&&
760: }
761: \]
762: \caption{\label{fig:phil_3_ring} A ring of 3 philosophers and their forks}
763: \end{figure}
764:
765: \subsection{Linear Automata}
766: \label{section:linear}
767:
768: A motion~$e$ of an automaton with boundary~$(S,(X_i,\mu_i)_{i \in I})$
769: is said to be \termdef{linear} if the action~$\mu_i(e)$ performed
770: by~$e$ on the~$i$'th boundary is nontrivial for at most one~$i \in I$.
771: The automaton~$S$ itself is said to be \termdef{linear}
772: if every motion of~$S$ is linear.
773:
774: That is, a linear automaton is an automaton that interacts with at most one
775: boundary in a given state. Linear automata have their boundaries decoupled,
776: in the sense that they never require simultaneity on distinct boundaries.
777: Another point of view is that linear automata are those modelling
778: systems for which {\em interleaving} semantics are sufficient.
779:
780: We note that even if the automata~$S$ and~$T$ are linear,
781: the binding~$\bind{S}{T}$ and the product~$\product{S}{T}$ may
782: be nonlinear. For example, the binding of a philosopher and a fork
783: (each a linear automaton) produces the nonlinear automaton of
784: figure~\ref{fig:phil_fork}.
785:
786: \subsubsection{Linearizable Automata}
787: \label{section:linearizable}
788:
789: An automaton with boundary~$(S,(X_i,\mu_i)_{i \in I})$ is
790: \termdef{linearizable} if, for each motion~$e \colon v \to w$ of~$S$
791: and given total order on~$I$, we can find a behaviour
792: \[
793: \begin{diagram}
794: v = v_0 & \rTo^{e_1} & v_1 & \rTo^{e_2} & \ldots & \rTo^{e_n} & v_n = w
795: \end{diagram}
796: \]
797: of~$S$ such that
798: \begin{enumerate}[(i)]
799: \item each~$e_k$ is linear
800: \item\label{resp_order}
801: if~$k, l \in [n]$ are such that~$\mu_i(e_k)$
802: and~$\mu_j(e_l)$ are nontrivial and~$i \leq j$ in the total order on~$I$,
803: then we have ~$k \leq l$
804: \item\label{complete}
805: if~$i \in I$ is such that~$\mu_i(e)$ is nontrivial, then
806: there exists a~$k \in [n]$ such that~$\mu_i(e) = \mu_i(e_k)$.
807: \end{enumerate}
808: where~$[n]$ denotes the set~$\{ 1, \ldots, n\}$.
809: Note that condition~(\ref{resp_order}) implies that distinct~$e_k$'s cannot
810: both perform nontrivial actions on the same boundary, i.e. that the existence
811: in~(\ref{complete}) is unique.
812:
813: Less symbolically, linearizable
814: automata are those for which any nonlinear motion~$e$ can be refined into
815: a series of linear motions with any desired ordering on the actions
816: carried out simultaneously by~$e$.
817:
818: Given linear automata~$S$ and~$T$, we observed above their binding
819: and product need not be linear. It is however the case that they
820: will be linearizable.
821: A linearizable automaton can be linearized by considering only
822: the linear motions. For example, linearizing the
823: subautomaton of figure~\ref{fig:phil_fork} reachable from
824: the initial state produces the automaton shown in
825: figure~\ref{fig:phil_fork_reachable}.
826:
827: \begin{figure}[h]
828: \[
829: \xymatrix
830: {
831: && (3,l) \ar[rr]^{(\refl|\refl)}
832: && (0,u) \ar[dd]_{(\al|\refl)} \ar@/^/[rr]^{(\refl|\al)}="top"
833: && (0,r) \ar[dd]^{(\al|\refl)}="right" \ar@/^/[ll]^{(\refl|\au)}
834: && \\ L&&&&&&&&L\\
835: && (2,l) \ar[uu]^{(\au|\refl)}="left"
836: && (1,u) \ar@/^/[rr]^{(\refl|\al)} \ar[ll]^{(\refl|\refl)}
837: && (1,r) \ar@/^/[ll]^{(\refl|\au)}="bot"
838: &&
839: \save
840: "2,5"."top"."left"."right"."bot"*[F-]\frm{} \ar@{-}"2,1" \ar@{-}"2,9"
841: \restore
842: }
843: \]
844: \caption{\label{fig:phil_fork_reachable}
845: The linearized reachable binding of a philosopher and a fork}
846: \end{figure}
847:
848: It should be noted that one cannot restrict attention solely to linear
849: automata, as the operation of feedback presented in
850: section~\ref{section:feedback} is not well suited to linear automata --
851: the only motions in a fed back linear automaton are those which are trivial on
852: the fed back boundaries. Further, the structural components described in
853: section~\ref{section:structural} are not linear automata.
854:
855: \subsubsection{Atomic Motions}
856: \label{section:atomic}
857:
858: Consider a system in which each automaton assigned to variable of the design
859: is linear. Given a global motion~$e$ of the system, we have a corresponding
860: local motions~$e_c$ for each component~$c$ of the system. We say that
861: the global motion~$e$ is an \termdef{atomic motion} if
862: \begin{enumerate}[(i)]
863: \item The local motions~$e_c$ are nontrivial for at most two components.
864: \item In the case that the local
865: motions~$e_c$ and~$e_d$ are nontrivial for distinct
866: components~$c$ and~$d$, then the components~$c$ and~$d$ have
867: boundaries~$(X,\mu_i)$ and~$(X,\mu_j)$ (respectively) which are joined
868: by a wire in the design, and for which~$\mu_i(e_c) = \mu_j(e_d)$ is
869: nontrivial.
870: \end{enumerate}
871: That is to say, the atomic motions are those for which multiple components
872: move nontrivially only in the event they are synchronizing on boundaries
873: joined by the design.
874:
875: Given a system comprised of linear automata, the subautomaton of the
876: composite automaton with all states but only atomic motions is termed the
877: \termdef{atomic core} of the system. The atomic core restricts attention
878: to those motions which are not fortuitously simultaneous. We shall use this
879: notion when discussing model checking for deadlock in
880: section~\ref{section:misa}. We simply remark at this point that when
881: considering a complete system, the atomic core allows sufficient motions to
882: fully explore the system, in the sense that any state~$w$ of the system
883: reachable from a state~$v$ is reachable via atomic motions.
884: However, we cannot restrict attention to
885: the atomic core prematurely, for feedback of systems relies on nonlocal
886: simultaneity.
887:
888: \bigskip
889:
890: We shall not investigate linearity further at present, but merely note
891: that one of the strengths of the theory presented here is that specific
892: requirements for envisaged domains (e.g. interleaving semantics) can be
893: carried as additional properties of, or structure on, the basic theory.
894: Precisely what can be done to tailor the basic theory for application to
895: a specific domain is an area for further interesting work. Further work
896: on linear automata can be found in section~4.1 of~\cite{KSW:span_graph},
897: including a connection with the process algebras of Hoare.
898: