1: %\documentclass[TR, article, PRG]{OUCLdocument}
2:
3: \documentclass{tlp}
4:
5: %\reportnumber{PRG-99}
6:
7: \bibliographystyle{acmtrans} %tlp}
8:
9: %\usepackage[all]{xy}
10: %\usepackage{epsfig}
11: \usepackage{latexsym}
12: \usepackage{bbm}
13: \usepackage{url}
14: %\usepackage{amsthm}
15:
16: \newtheorem{proposition}{Proposition}[section]
17: \newtheorem{lemma}[proposition]{Lemma}
18: \newtheorem{corollary}[proposition]{Corollary}
19: \newtheorem{theorem}[proposition]{Theorem}
20:
21: %\theoremstyle{definition}
22: \newtheorem{definition}[proposition]{Definition}
23: \newtheorem{example}[proposition]{Example}
24:
25: \newcommand{\sskip}{\mathbf{skip}}
26:
27: \newcommand{\Member}{\mathit{Member}} \newcommand{\And}{\mathit{And}}
28: \newcommand{\Diff}{\mathit{Diff}} \newcommand{\Empty}{\mathit{Empty}}
29: \newcommand{\Pre}{\mathit{Pre}} \newcommand{\pre}{\mathit{pre}}
30: \newcommand{\dom}{\mathrm{dom}}
31: \newcommand{\false}{\mathbf{false}} \newcommand{\true}{\mathbf{true}}
32:
33: \newcommand{\ext}[1]{\lceil {#1} \rceil} \newcommand{\syn}[1]{[\![
34: {#1} ]\!]} \newcommand{\syns}[2]{[\![ {#1} ]\!]_{{\cal S}, {#2}}}
35: \newcommand{\sem}[1]{\langle \! \langle {#1} \rangle \! \rangle}
36: \newcommand{\semi}[2]{\sem{#1}_{#2}}
37: \newcommand{\pfsem}[2]{\semi{#1}{#2}^*}
38: \newcommand{\switch}[2]{
39: \begin{array}{c}
40: {#1} \\[-4pt] {#2}
41: \end{array}
42: }
43:
44: \newcommand{\Epsilon}{{\cal E}}
45:
46: %\newcommand{\Array}[2]{\mbox{\bf Array }[{#1}] \mbox{ \bf of } {#2}}
47: \newcommand{\Array}[2]{{#2}[{#1}]}
48: \newcommand{\Read}[3]{\mathbf{Read}({#1}, {#2}, {#3})}
49: \newcommand{\Write}[3]{\mathbf{Write}({#1}, {#2}, {#3})}
50: %\newcommand{\Read}[3]{{#1} := {#2}[{#3}]}
51: %\newcommand{\Write}[3]{{#1}[{#2}] := {#3}}
52: \newcommand{\subst}[3]{{#1} [ ^{#2} / _{#3} ]}
53: \newcommand{\overmap}[3]{{#1} [ {#2} \mapsto {#3} ]}
54:
55: \newcommand{\restrict}[1]{\downarrow_{_{#1}}}
56: \newcommand{\TERMS}{{\it TERMS}}
57: \newcommand{\implies}{\Rightarrow}
58: \renewcommand{\iff}{\Leftrightarrow}
59: \newcommand{\pstep}[1]{\quad \{ \mbox{ #1 } \}}
60: \newcommand{\existsnext}{{\exists \! \, \bigcirc}}
61: \newcommand{\forallnext}{{\forall \! \, \bigcirc}}
62:
63: \newcommand{\code}[1]{{\tt #1}}
64:
65: \submitted{18 March 2002}
66: \revised{-}
67: \accepted{2 July 2003}
68:
69:
70:
71: \begin{document}
72: \sloppy
73:
74: \title[On model checking data-independent systems with arrays
75: without reset]{On model checking data-independent \\ systems with arrays
76: without reset \footnote{This work was funded in part by the EPSRC standard
77: research grant `Exploiting data independence', GR/M32900.
78: The first author is affiliated to the Mathematical Institute,
79: Belgrade, and was supported partly by a grant from the Intel Corporation,
80: a Junior Research Fellowship from
81: Christ Church, Oxford, and previously by a scholarship from
82: Hajrija \& Boris Vukobrat and Copechim France SA.
83: The second author was funded in part by QinetiQ Malvern.
84: The third author was funded in part by the US ONR.}
85: }
86: \author[R.S. Lazi\'c, T.C. Newcomb, and
87: A.W. Roscoe]{R.S. LAZI\'C\\
88: Department of Computer
89: Science, University of Warwick, \\ Coventry, CV4 7AL, UK\\
90: \email{ranko.lazic@dcs.warwick.ac.uk}
91: \and T.C. NEWCOMB and
92: A.W. ROSCOE\\
93: Oxford University Computing Laboratory, \\ Wolfson Buildings,
94: Parks Road, Oxford, OX1 3QD, UK\\
95: \email{tom.newcomb@comlab.ox.ac.uk} \\
96: \email{bill.roscoe@comlab.ox.ac.uk}}
97:
98: \maketitle
99:
100: \begin{abstract}
101:
102: A system is data-independent with respect to a data type $X$ iff the
103: operations it can perform on values of type $X$ are restricted to
104: just equality testing. The system may also store, input and output
105: values of type $X$.
106:
107: We study model checking of systems which are data-independent with
108: respect to two distinct type variables $X$ and $Y$, and may in
109: addition use arrays with indices from $X$ and values from $Y$. Our
110: main interest is the following {\em parameterised model-checking}
111: problem: whether a given program satisfies a given temporal-logic
112: formula for all non-empty finite instances of $X$ and $Y$.
113:
114: Initially, we consider instead the abstraction where $X$ and $Y$ are
115: infinite and where partial functions with finite domains are used to
116: model arrays. Using a translation to data-independent systems
117: without arrays, we show that the $\mu$-calculus model-checking
118: problem is decidable for these systems.
119:
120: From this result, we can deduce properties of all systems with
121: finite instances of $X$ and $Y$. We show that there is a procedure
122: for the above parameterised model-checking problem of the universal
123: fragment of the $\mu$-calculus, such that it always terminates but
124: may give false negatives. We also deduce that the parameterised
125: model-checking problem of the universal disjunction-free fragment of
126: the $\mu$-calculus is decidable.
127:
128: Practical motivations for model checking data-independent systems
129: with arrays include verification of memory and cache systems, where
130: $X$ is the type of memory addresses, and $Y$ the type of storable
131: values. As an example we verify a fault-tolerant memory interface
132: over a set of unreliable memories.
133: \end{abstract}
134:
135: \begin{keywords}
136: model checking, data independence, arrays, $\mu$-calculus.
137: \end{keywords}
138:
139: %%%%%%%%
140: Submitted: March 18, 2002; accepted: July 2, 2003.
141: %%%%%%%%
142:
143: \section{Introduction}
144:
145: A program is data-independent \cite{Wol86,LN00} with respect to a
146: data type $X$ if it can only input, output, and assign values of type
147: $X$, as well as test pairs of such values for equality. The program
148: cannot apply any other operation to values of type $X$.
149:
150: Data-independent programs are common. Communication protocols are
151: data-independent with respect to the type that is being communicated.
152: Nodes of a network protocol may be data-independent with respect to
153: the type of node identifiers.
154:
155: Given a program $\cal P$ which is data-independent with respect to a
156: type $X$, the type $X$ can be seen as a type variable, i.e.\ as a
157: parameter of $\cal P$, in the sense that it can be instantiated by any
158: set. Given a property $\varphi$ in temporal logic, the {\em
159: parameterised model-checking problem} asks whether $\cal P$
160: satisfies $\varphi$ for all instances of $X$. A variety of
161: decidability results are known for this and related problems (e.g.\
162: \cite{Wol86,HDB97,LN00,FS01}).
163:
164: In this paper, we consider programs which are data-independent with
165: respect to two types $X$ and $Y$, but which can in addition use arrays
166: indexed by $X$ and storing values of type $Y$. We focus on the case
167: where the programs may use the operations for reading and writing
168: an array component, but where array reset (i.e.\ assigning a given value
169: of type $Y$ to all array components) is not available.
170:
171: The techniques which were used to establish decidability of
172: parameterised model checking for data-independent programs cannot be
173: used when data independence is extended by arrays. An array is
174: indexed by the whole of the type $X$, and it therefore may contain an
175: unbounded number of values of type $Y$. These values may have been
176: fixed by previous actions, and although they are not all accessible in
177: the current state, they may become accessible if their indices appear
178: in variables of type $X$ in subsequent states.
179:
180: One motivation for considering data-independent programs with arrays
181: is cache-coherence protocols \cite{AG96}, more precisely the problem
182: of verifying that a memory system satisfies a memory model such as
183: sequential consistency \cite{HQR99}. Cache-coherence protocols are
184: data independent with respect to the types of memory addresses and
185: data values.
186:
187: Another application area is parameterised verification of network
188: protocols by induction, where each node of the network is
189: data-independent with respect to the type of node identities
190: \cite{CR00}. Arrays arise when each node is data-independent with
191: respect to another type, and it stores values of that type.
192:
193: Given a data-independent program $\cal P$ with arrays and a
194: temporal-logic formula $\varphi$ referring to control states of $\cal
195: P$, the main question of interest is whether $\cal P$ satisfies
196: $\varphi$ for all non-empty finite instances of $X$ and $Y$.
197:
198: In order to study decidability of this parameterised model-checking
199: problem, we first consider the abstraction where $X$ and $Y$ are
200: instantiated to infinite sets, and where arrays are modelled by
201: partial functions with finite domains. An undefined array component
202: represents nondeterminism which is still to be resolved.
203:
204: We describe a translation of such a program to a
205: bisimulation-equivalent data-independent program without arrays; it
206: follows that the $\mu$-calculus model checking problem is decidable in
207: this case \cite{BCG88,NK00}. The $\mu$-calculus is a branching-time
208: logic, more expressive than CTL or CTL$^*$ \cite{AH98}.
209:
210: For a program $\cal P$, any transition system generated by $\cal P$
211: with finite instances of $X$ and $Y$ is simulated by the transition
212: system generated by $\cal P$ with infinite instances of $X$ and $Y$.
213: It follows that there is a procedure for the parameterised
214: model-checking problem of the universal fragment of the
215: $\mu$-calculus, such that it always terminates, but may give false
216: negatives. This fragment of the $\mu$-calculus is more expressive than
217: linear-time temporal logic.
218:
219: We also deduce that the parameterised model-checking problem of the
220: universal disjunction-free fragment of the $\mu$-calculus is
221: decidable. This fragment of the $\mu$-calculus is more expressive than
222: reachability, although less expressive than linear-time temporal logic
223: \cite{HM00}. It can be used to express properties such as ``the system
224: produces an output every ten time units.'' Such a property could be
225: checked less naturally using reachability on a modified version of the
226: system.
227:
228: As an example, we model a simple fault-tolerant interface working over
229: a set of unreliable memories. The parameterised model-checking
230: procedure presented here is used to verify its correctness with
231: respect to the specification ``a read at an address always returns the
232: value of the last write to that address until a particular number of
233: faults occur,'' independently of the size of the memory and of the
234: type of storable data values. This program illustrates how our
235: procedure works, and is a simple representative from the class of
236: programs to which this paper applies. More concretely, using our
237: results it is possible to model and verify some types of
238: fault-tolerant fully-associative cache systems \cite{PH94},
239: independently of cache size, memory size, the type of data values, and
240: page replacement policies.
241:
242: Our results might be compared to \cite{HIB97}, where it is shown that
243: data-independent programs with one array, without reset, with infinite
244: instances of $X$ and $Y$, and with a slightly different modelling of
245: arrays by partial functions, have finite trace-equivalence quotients.
246: The parameterised model-checking problem is not considered. We have
247: extended this result to allow many arrays, and have shown that model
248: checking of the $\mu$-calculus is decidable in the infinite-arrays
249: case, which is a stronger logic than the linear-time temporal-logic
250: induced by finite trace-equivalence quotients. Also, the parameterised
251: model-checking problem for finite arrays is not considered in
252: \cite{HIB97}, whereas we have developed decidability results for these
253: systems.
254:
255: This paper clarifies a technique described in \cite{McM99}, which
256: promotes the use of abstract interpretation for programs with arrays.
257: The programs considered there are more general than ours as the arrays
258: may be multi-dimensional and of varying index and data types.
259: Temporal case splitting is used to consider only a finite portion of
260: the arrays; at the other locations a read operation returns a special
261: symbol $\bot$ which represents any element in the type. Datatype
262: reduction, a standard abstraction used for data-independent programs
263: \cite{ID96}, is then used to deal with the remaining values stored in
264: the arrays. This is a similar strategy to that used in the proofs in
265: this paper, although \cite{McM99} presents no decidability results
266: about the technique apart from stating that the problem is undecidable
267: in general. We have identified a smaller, yet still interesting class
268: of programs and shown that there is an automatic parameterised
269: model-checking procedure for them.
270:
271: An advantage of this paper over both these related works is that we
272: use a syntactic transformation to remove the arrays. This admits the
273: application of orthogonal state reduction techniques, such as further
274: program transformations or advanced model checking algorithms, eg.\
275: using BDDs \cite{BC+92}.
276:
277: The contributions of this paper are as follows. We describe an
278: automatic procedure for model checking a programming language useful
279: for prototyping memory systems such as caches. We extend the result
280: about infinite arrays in \cite{HIB97}, and also show how our result
281: relates to questions about finite arrays. This allows us to prove
282: properties about parameterised systems: for example, that memory
283: systems can be verified independently of memory size and data values.
284: We also identify a subclass of the programs considered in \cite{McM99}
285: and prove the decidability of model checking them. Decidability
286: results are important because they provide verification procedures
287: which are guaranteed to terminate for every instance of the problem,
288: with a correct answer.
289:
290: The rest of this paper is organised as follows. Section
291: \ref{sect:prelims} introduces some standard definitions and
292: preliminary results, and then the language of programs we will be
293: considering is defined in Section \ref{sect:lang}. Section
294: \ref{sect:infinite} considers the case that the types $X$ and $Y$ are
295: infinite, and from this we deduce results about all the cases when
296: they are finite in Section \ref{sect:finite}. We conclude with a
297: summary and discussion of future work in Section
298: \ref{sect:conclusion}.
299:
300: \section{Preliminaries}
301:
302: \label{sect:prelims}
303:
304: In this section we introduce transition systems as our modelling
305: language, and our language of specifications, the modal
306: $\mu$-calculus.
307:
308: \subsection{Transition systems}
309:
310: \begin{definition}
311: A {\em transition system} is a structure $(Q, \delta, \ext{\cdot},
312: P)$:
313: \begin{itemize}
314: \item $Q$ is the {\em state space},
315: \item $\delta : Q \rightarrow 2^Q$ is the {\em successor function},
316: giving the set of possible next states after the given state,
317: \item $P$ is a finite set of {\em observables},
318: \item $\ext{\cdot} : P \rightarrow 2^Q$ is the {\em extensions function}.
319: \end{itemize}
320: \end{definition}
321: Thus $\ext{p}$ is the set of states in $Q$ that have some observable
322: property $p$. In this paper, $p$ will typically be a boolean variable
323: of the program under consideration, and will be observed at exactly
324: the states where the value of the variable is ``true''.
325:
326: \begin{definition}
327: A {\em trace} $\pi$ of a transition system is a finite sequence of
328: observables $p_1 p_2 ... p_l$ such that there exists a sequence of
329: states $s_1 s_2 ... s_l$ from $Q$ where $s_{i+1} \in \delta(s_i)$
330: (for $i = 1 ... l-1$) and $s_i \in \ext{p_i}$ (for $i = 1 ... l$).
331: We will write $\pi(i)$ to mean $p_i$, the $i$th observable in the
332: trace $\pi$.
333: \end{definition}
334:
335: Given two transition systems ${\cal S}_1 = (Q_1, \delta_1,
336: \ext{\cdot}_1, P)$ and ${\cal S}_2 = (Q_2, \delta_2, \ext{\cdot}_2,
337: P)$ over the same observables $P$, it is possible to compare them in
338: the following ways.
339:
340: \begin{definition}
341: A relation $\preceq\ \subseteq Q_1 \times Q_2$ is a {\em simulation} if
342: $s \preceq t$ implies the following two conditions:
343: \begin{itemize}
344: \item[1.] For all observables $p$, $s \in \ext{p}_1$ if and only if $t \in
345: \ext{p}_2$.
346: \item[2.] For each state $s' \in \delta_1(s)$, there is a state $t' \in
347: \delta_2(t)$ such that $s' \preceq t'$.
348: \end{itemize}
349: \end{definition}
350:
351: \begin{definition}
352: A relation $\approx\ \subseteq Q_1 \times Q_2$ is a {\em bisimulation} if
353: it is a simulation and $s \approx t$ also implies the following condition:
354: \begin{itemize}
355: \item[3.] For each state $t' \in \delta_2(t)$, there is a state $s' \in
356: \delta_1(s)$ such that $s' \approx t'$.
357: \end{itemize}
358: \end{definition}
359:
360: \subsection{The $\mu$-calculus}
361:
362: The following presentation of the $\mu$-calculus and some of its
363: fragments is taken from \cite{HM00}.
364:
365: \begin{definition}
366: The formulas of the {\em $\mu$-calculus} over a set of
367: observables $P$ are generated by the grammar
368: $$
369: \varphi ::= p \mid \overline{p} \mid h \mid \varphi \vee \varphi \mid \varphi
370: \wedge \varphi \mid \existsnext \varphi \mid \forallnext \varphi \mid
371: (\mu h : \varphi) \mid (\nu h : \varphi)
372: $$
373: for $p \in P$ and variables $h$ from some fixed set.
374: \end{definition}
375:
376: For functions $\Epsilon$, we write $\Epsilon [ h \mapsto \tau ]$ for
377: the mapping that agrees on $\Epsilon$ on all values in its domain,
378: except that $h$ is instead mapped to $\tau$. Given a transition system
379: ${\cal S} = (Q, \delta, \ext{\cdot}, P)$, and a mapping from the
380: variables to sets of states $\Epsilon$, any formula $\varphi$ of
381: the $\mu$-calculus over $P$ defines a set $\syns{\varphi}{\Epsilon}
382: \subseteq Q$ of states:
383: $$
384: \begin{array}{l}
385: \syns{p}{\Epsilon} = \ext{p} \\
386: \syns{\overline{p}}{\Epsilon} = Q \setminus \ext{p} \\
387: \syns{h}{\Epsilon} = \Epsilon(h) \\
388: \syns{\varphi_1 \switch{\vee}{\wedge} \varphi_2}{\Epsilon} =
389: \syns{\varphi_1}{\Epsilon} \switch{\cup}{\cap} \syns{\varphi_2}{\Epsilon} \\
390: \syns{\switch{\exists}{\forall} \bigcirc \varphi}{\Epsilon} = \{ s \in Q
391: \mid \switch{\exists}{\forall} s' \in \delta(s) : s' \in
392: \syns{\varphi}{\Epsilon} \} \\
393: \syns{\switch{\mu}{\nu} h : \varphi}{\Epsilon} = \switch{\cap}{\cup} \{
394: \tau \subseteq Q \mid \tau = \syns{\varphi}{\Epsilon[h \mapsto \tau]} \}.
395: \end{array}
396: $$
397:
398: The logic $L_1^\mu$ over a set of observables $P$ is the set of closed
399: formulas of the $\mu$-calculus over $P$. We will write ${\cal S}, s
400: \models \varphi$ when $s \in \syns{\varphi}{\Epsilon}$ for any
401: $\Epsilon$. (As an $L^\mu_1$ formula $\varphi$ is closed, the initial
402: mappings in $\Epsilon$ are never used and the validity is therefore
403: independent of $\Epsilon$.)
404:
405: Usually we are not interested in which states satisfy a given formula,
406: rather we want to know whether the set of initial states of a system
407: satisfy it or not. We therefore introduce a notion of satisfaction and
408: write ${\cal S}, b_0 \models \varphi$, where $b_0$ is a boolean
409: variable of $\cal P$, to mean that for all states $s \in \ext{b_0}$,
410: we have ${\cal S}, s \models \varphi$.
411:
412: We will also use the following fragments of the $\mu$-calculus:
413:
414: \begin{definition}
415: The logic $L_2^\mu$ (the {\em existential fragment of the
416: $\mu$-calculus}) is the subset of $L_1^\mu$ without the
417: constructors $\overline{p}$ or $\forallnext$.
418: %The logic $L_3^\mu$ (the {\em
419: % linear-time $\mu$-calculus}) contains the closed formulas from the
420: %grammar
421: %$$
422: %\varphi ::= c \mid p \mid \varphi \vee \varphi \mid c \wedge \varphi
423: %\mid \existsnext \varphi \mid (\mu p : \varphi)
424: %\mid (\nu p : \varphi).
425: %$$
426: \end{definition}
427:
428: \begin{definition}
429: The logic $L_4^\mu$ (the {\em existential conjunction-free fragment of
430: the $\mu$-calculus}) is the subset of $L_2^\mu$ without the
431: constructors $\wedge$ or $\nu$.
432: \end{definition}
433:
434: $L^\mu_1$ is strictly more expressive than $L^\mu_2$, which is
435: strictly more expressive than $L^\mu_4$ \cite{HM00}.\footnote{The
436: logics $L^\mu_3$ (linear-time $\mu$-calculus) and $L^\mu_5$
437: (reachability) are not required in this paper.}
438:
439: For any logic $L^\mu_i$, there is a {\em dual logic} $\overline{L^\mu_i}$
440: obtained by replacing the constructors $p, \overline{p}, \vee, \wedge,
441: \existsnext, \forallnext, \mu, \nu$ in formulas $\varphi$ by
442: $\overline{p}, p, \wedge, \vee, \forallnext,\existsnext,
443: \nu, \mu$ respectively to form formulas $\overline{\varphi}$. The
444: satisfaction of an $\overline{L^\mu_i}$ formula $\overline{\varphi}$
445: by a state $s \in Q$ is complementary to the satisfaction of the
446: formula $\varphi$ in the logic $L^\mu_i$ by $s$, ie.\ ${\cal S}, s
447: \models \varphi$ iff ${\cal S}, s \not \models \overline{\varphi}$.
448:
449: \section{Language of programs}
450:
451: \label{sect:lang}
452:
453: Here we define the syntax of our programs, which is based on that of
454: UNITY \cite{CM88}. It is a language of guarded multiple assignments,
455: extended with simple array operations. We give semantics to these
456: programs in terms of transition systems.
457:
458: Our programs are data-independent with respect to a set of type
459: symbols, as the only operations they allow on values of these types
460: are non-deterministic selection (with no assumption of fairness),
461: copying between variables, and equality testing. In addition, they may
462: read and write these values to arrays indexed by other such type
463: symbols.
464:
465: We then describe the subclass of these programs we will be considering
466: in this paper and the problem we will be addressing.
467:
468: \subsection{Syntax}
469:
470: We assume the existance of a set of symbols called {\em type symbols}.
471:
472: A {\em program} $\cal P$ is:
473: \begin{itemize}
474: \item A finite set of {\em variables} together with their {\em types},
475: partitioned into three sets:
476: \begin{itemize} \item boolean variables, of type $\mathbbm{B}$,
477: \item data variables, of type $Z$ where $Z$ is some type symbol,
478: \item array variables, of type $\Array{X}{Y}$ where $X$ and $Y$ are
479: type symbols.
480: \end{itemize}
481: \item A finite set of guarded commands $e \longrightarrow I$,
482: where:
483: \begin{itemize}
484: \item The {\em boolean expression} $e$ is taken from the grammar
485: $$
486: e ::= \true \mid \false \mid b \mid z = z' \mid \neg e \mid e \vee e,
487: $$
488: where $b$ ranges over the boolean variables, and $z$ and $z'$ are
489: data variables of the same type.
490: \item The {\em command} $I$, representing a simultaneous multiple
491: assignment, is a set containing at most:
492: \begin{itemize}
493: \item for each boolean variable $b$, an assignment $b := e$, where
494: $e$ is a boolean expression,
495: \item for each data variable $z$ of type $Z$, at most one of $z :=
496: z'$, $z :=\ ?$, or $\Read{z}{a}{x}$, where $z'$, $a$, and $x$
497: are any variables with types $Z$, $\Array{X}{Z}$, and $X$
498: respectively for some type symbol $X$,
499: \item for each array $a$ of type $\Array{X}{Y}$, an operation
500: $\Write{a}{x}{y}$, where $x$ and $y$ are variables of type $X$
501: and $Y$ respectively.
502: \end{itemize}
503: \end{itemize}
504: \end{itemize}
505:
506: {\bf Notation:} We may write multiple assignments as two lists of
507: equal length separated by $:=$, eg.\ $x, y := y, x$ repesents the
508: multiple assignment consisting of both $x := y$ and $y := x$. We may
509: also denote the array operations $\Read{y}{a}{x}$ and
510: $\Write{a}{x}{y}$ with the C-like syntaxes $y := a[x]$ and $a[x] := y$
511: respectively.
512:
513: \subsection{Semantics}
514:
515: A {\em type instantiation} ${\cal I}$ for a program $\cal P$ is a
516: function from the type symbols in $\cal P$ to non-empty sets upon
517: which equality is decidable.
518:
519: The semantics of a program $\cal P$ together with a type
520: instantiation ${\cal I}$ for it, denoted $\semi{\cal P}{\cal I}$, is the
521: transition system $(Q, \delta, \ext{\cdot}, P)$, where:
522: \begin{itemize}
523: \item The state space $Q$ is the set of all total functions from the
524: variables of $\cal P$ into
525: \begin{itemize}
526: \item for boolean variables, the set $\mathbbm{B} = \{ \true, \false \}$,
527: \item for data variables of type $Z$, the set ${\cal I}(Z)$,
528: \item for array variables of type $\Array{X}{Y}$, the total-functions
529: space ${\cal I}(X) \rightarrow {\cal I}(Y)$.
530: \end{itemize}
531: \item $s' \in \delta(s)$ if and only if there is some guarded command
532: $e \longrightarrow I$ in $\cal P$ such that $E_s(e) = \true$ and $s
533: \Delta_I s'$ where:
534: \begin{itemize}
535: \item The evaluating function $E$ for a boolean expression in a state $s$ is
536: defined as follows:
537: $$
538: \begin{array}{lcl}
539: E_s(\true) &=& \true, \\
540: E_s(\false) &=& \false, \\
541: E_s(e_1 \vee e_2) &=& E_s(e_1) \mbox{ `or' } E_s(e_2), \\
542: E_s(\neg e_1) &=& \mbox{`not' } E_s(e_1), \\
543: E_s(b) &=& s(b), \\
544: E_s(z = z') &=& ( s(z) = s(z') ),
545: \end{array}
546: $$
547: for boolean variables $b$ and data variables $z$ and $z'$.
548: \item The relation $\Delta_I$ on pairs of states for a multiple
549: assignment $I$ is defined as $s \Delta_I s'$ if and only if all
550: of the following:
551: \begin{itemize}
552: \item for each boolean variable $b$, if $b := e$ is in $I$, then
553: $s'(b) = E_s(e)$, else $s'(b) = s(b)$,
554: \item for each data variable $z$, \\
555: \begin{tabular}{l}
556: if $z := z'$ is in $I$, then $s'(z) = s(z')$, \\
557: else if $\Read{z}{a}{x}$ is in $I$, then $s'(z) = s(a)(s(x))$, \\
558: else either $z :=\ ?$ is in $I$ or $s'(z) = s(z)$,
559: \end{tabular}
560: \item for each array variable $a$ of type $\Array{X}{Y}$, and for
561: each $v \in {\cal I}(X)$,\\
562: \begin{tabular}{l}
563: if there are $x$ and $y$ variables such that \\ \quad
564: $\Write{a}{x}{y}$ is in $I$ and $s(x) = v$, then $s'(a)(v) = s(y)$, \\
565: else $s'(a)(v) = s(a)(v)$.
566: \end{tabular}
567: \end{itemize}
568: \end{itemize}
569: \item the observables $P$ is the set of boolean variables,
570: \item the extensions function is defined as
571: $$
572: \ext{b} = \{ s \in Q \mid s(b) = \true \}.
573: $$
574: \end{itemize}
575:
576: {\bf Notation:} We may write $s(a[x])$ to mean $s(a)(s(x))$ for
577: states $s$, array variables $a$, and data variables $x$.
578:
579: It can be noticed that it is only the {\em cardinalities} of the type
580: instances which affect the observable semantics. Formally, given two
581: type instantiations ${\cal I}_1$ and ${\cal I}_2$ for a program $\cal
582: P$, where $|{\cal I}_1(Z)| = |{\cal I}_2(Z)|$ for all type symbols $Z$
583: in $\cal P$, there exists a bisimulation $\rightleftharpoons$ between
584: ${\cal S}_1 = \semi{\cal P}{{\cal I}_1}$ and ${\cal S}_2 = \semi{\cal
585: P}{{\cal I}_2}$. This is because the observable semantics depend on
586: the equality relationships on values of these types, and bijections
587: preserve equality. If ${\cal I}_1(Z)$ and ${\cal I}_2(Z)$ have the
588: same cardinality, then there exists a bijection $f_Z$ between them;
589: the bisimulation $\rightleftharpoons$ uses these bijections to
590: translate values between ${\cal S}_1$ and ${\cal S}_2$.
591:
592: It follows that, for the results in this paper, any type instantiation
593: $\cal I$ can be replace by $\cal I'$ which maps onto an initial
594: portion of the cardinal numbers, ie.\ ${\cal I}'(Z) = \{1, \ldots,
595: |{\cal I}(Z)| \}$.
596:
597: \subsection{This paper}
598:
599: For simplicity, in this paper we consider programs with only two type
600: symbols $X$ and $Y$, and array variables only of type $\Array{X}{Y}$.
601: We will write $\semi{\cal P}{A, B}$ as shorthand for $\semi{\cal
602: P}{\cal I}$ where $\cal I$ maps $X$ and $Y$ to the sets $A$ and $B$
603: respectively.
604:
605: In particular we do not consider the extension of this language to
606: include the array reset operation, which assigns a given value of type
607: $Y$ to all array components. The operational semantics of such an
608: operation would dictate that the successor state maps the array
609: variable to the constant function returning the $Y$ value. Array reset
610: is too expressive to obtain results as powerful as we do here
611: \cite{RL01}.
612:
613: We will use variables $b$, $b'$, $b_i$, ... to denote variables of
614: type $\mathbbm{B}$, and similarly $x$, $y$ and $a$ for variables of
615: type $X$, $Y$ and $\Array{X}{Y}$ respectively. We will also use $z$
616: for variables of either type $X$ or $Y$, and $e$ for boolean
617: expressions.
618:
619: The main problem of interest is the following {\em parameterised
620: model-checking problem}: given a data-independent program $\cal P$
621: with arrays , a boolean variable $b_0$ of $\cal P$, and a temporal
622: logic formula $\varphi$ referring to control states of $\cal P$, is it
623: true that $\semi{\cal P}{\cal I}, b_0 \models \varphi$ for all type
624: instantiations $\cal I$ which map $X$ and $Y$ to non-empty finite
625: sets.
626:
627: \begin{example}
628: \label{ex:singleCache}
629: Our example programs will use variables that range over finite
630: datatypes, such as program counters, even though these are not part of
631: our formally considered language. This is because such values can be
632: coded as tuples of booleans, which are allowed. Similarly we will use
633: familiar programming constructs such as if-then-else, goto, and
634: nondeterministic choice \verb$|~|$ because the effects of these can be
635: achieved using guarded commands and booleans.
636:
637: Figure \ref{fig:singleCache1} shows a fault-tolerant interface over a
638: set of unreliable memories, which we expect to work provided there is
639: no more than one error. It is parameterised by two types \code{ADDR}
640: and \code{DATA} representing the types of addresses and data values
641: respectively, and the program is data independent with arrays without
642: reset with respect to these types. The memories are represented by
643: arrays called \code{mem1}, \code{mem2} and \code{mem3}, and the
644: address and data busses are represented by the variables
645: \code{addrBus} and \code{dataBus}.
646:
647: In \code{LOOP}, values appear on the address and data busses and are
648: used to write to or read from memory. When writing to memory, the data
649: value is written to all three arrays at the appropriate place. When
650: reading from memory, the program takes the majority value of all three
651: memories at that location if such a value exists.
652:
653: We have incorporated the faulty behaviour of the memories into our
654: program. Of course this would not be present in the final code, but
655: our arrays are not naturally faulty so we need to simulate that
656: behaviour in order to do any interesting analysis on our program. So,
657: in between reads and writes, a fault may occur which writes a
658: nondeterministic value to one of the memories at any location.
659:
660: A property we would usually desire of a memory system is that a read
661: from an arbitrary location will always return the value of the last
662: write to that location, provided there has been one. Because of the
663: possibility of faults in this system, we would expect this to be true
664: until two faults have occurred.
665:
666: Figure \ref{fig:singleCache2} shows the code again, annotated with
667: ``checking code'' marked with \verb$#$'s. This code unobtrusively
668: monitors the progress of the system and moves it to a special
669: \code{ERROR} state when it detects that the program's specification
670: has been broken. The new code requires its own variables:
671: \code{testAddr} holds the arbitrary memory location which is being
672: monitored and \code{testData} contains the last value written there,
673: provided that \code{testWritten} is true. The variable \code{faults}
674: records whether the number of faults so far is none, one, or more than
675: one. The annotations in the code maintain these invariants.
676:
677: \begin{figure}
678: {\footnotesize
679: \begin{verbatim}
680: VARIABLES:
681: addrBus: ADDR
682: dataBus: DATA
683: data1, data2, data3: DATA
684: mem1, mem2, mem3: DATA[ADDR]
685:
686: START:
687: goto LOOP
688:
689: LOOP:
690: addrBus, dataBus := ?, ?
691: goto READ |~| goto WRITE |~| goto FAULT
692:
693: READ:
694: data1, data2, data3 := mem1[addrBus], mem2[addrBus], mem3[addrBus]
695: if data1 != data2 then dataBus := data3 else dataBus := data1
696: goto LOOP
697:
698: WRITE:
699: mem1[addrBus], mem2[addrBus], mem3[addrBus] := dataBus, dataBus, dataBus
700: goto LOOP
701:
702: FAULT:
703: mem1[addrBus] := dataBus |~| mem2[addrBus] := dataBus
704: |~| mem3[addrBus] := dataBus
705: goto LOOP
706: \end{verbatim}}
707: \caption{Fault-tolerant memory.
708: \label{fig:singleCache1}}
709: \end{figure}
710:
711: \begin{figure}
712: {\footnotesize
713: \begin{verbatim}
714: VARIABLES:
715: 1 addrBus: ADDR
716: 2 dataBus: DATA
717: 3 data1, data2, data3: DATA
718: 4 mem1, mem2, mem3: DATA[ADDR]
719: 5# testAddr: ADDR
720: 6# testData: DATA
721: 7# testWritten: BOOL
722: 8# faults: {0..2}
723:
724: START:
725: 1# faults, testWritten := 0, false
726: 2 goto LOOP
727:
728: LOOP:
729: 1 addrBus, dataBus := ?, ?
730: 2 goto READ |~| goto WRITE |~| goto FAULT
731:
732: READ:
733: 1 data1, data2, data3 := mem1[addrBus], mem2[addrBus], mem3[addrBus]
734: 2 if data1 != data2 then dataBus := data3 else dataBus := data1
735: 3# if addrBus = testAddr and testWritten and faults < 2 and dataBus != testData
736: then goto ERROR
737: 4 goto LOOP
738:
739: WRITE:
740: 1 mem1[addrBus], mem2[addrBus], mem3[addrBus] := dataBus, dataBus, dataBus
741: 2# if addrBus = testAddr then testData, testWritten := dataBus, true
742: 3 goto LOOP
743:
744: FAULT:
745: 1 mem1[addrBus] := dataBus |~| mem2[addrBus] := dataBus
746: |~| mem3[addrBus] := dataBus
747: 2# if faults < 2 then faults := faults + 1
748: 3 goto LOOP
749:
750: ERROR:
751: 1# goto ERROR
752: \end{verbatim}}
753: \caption{Fault-tolerant memory composed with specification.
754: \label{fig:singleCache2}}
755: \end{figure}
756:
757: In order to test that the system satisfies its specification, we need
758: to check that the \code{ERROR} state is never reachable from the start,
759: whatever finite non-empty sets $A$ and $B$ are used as instances of
760: \code{ADDR} and \code{DATA}. This can be expressed using
761: $\overline{L^\mu_4}$ as
762: $$\forall A, B \cdot \semi{\cal P}{A, B}, b_0 \models \nu h:
763: \forallnext (\overline{b_E} \wedge h),
764: $$ where $b_0$ is a special boolean variable of the program that must be
765: true for the program line \code{START} to be executed, where it is set
766: to false, and must be false for all other guarded instructions;
767: similarly, $b_E$ must be false for all instructions, and is set to
768: true at the line \code{ERROR}.
769: \end{example}
770:
771: \section{Infinite arrays}
772:
773: \label{sect:infinite}
774:
775: In this section we consider the class of systems where $X$ and $Y$ are
776: both instantiated to infinite sets.
777:
778: We provide a syntactic translation from programs with arrays to
779: programs without arrays. We show that there exists a bisimulation
780: between the former with semantics that use partial functions with
781: finite domains to model arrays, and the latter with normal semantics.
782: From this, we deduce that the $\mu$-calculus model-checking problem is
783: decidable for this class of systems.
784:
785: This section is organised into the following subsections. The
786: partial-functions semantics is introduced in \ref{sub:partial}; the
787: translation is described in \ref{sub:translation}; the bisimulation
788: and its proof are in \ref{sub:connection}; the model-checking result
789: is deduced in \ref{sub:conclusion}.
790:
791: \subsection{Partial-functions semantics}
792:
793: \label{sub:partial}
794:
795: For infinite instantiations for $X$ and $Y$, the semantic values for
796: arrays are finite partial functions. An undefined location in an
797: array represent nondeterminism which is yet to be resolved; this
798: nondeterminism is resolved exactly when the system inputs the
799: corresponding index value into one of its variables. These semantics
800: are formalised here.
801:
802: The {\em partial-functions semantics} of a program $\cal P$ together
803: with a type instantiation ${\cal I}$ for it, denoted $\pfsem{\cal
804: P}{\cal I}$, is the transition system $(Q^*, \delta^*,
805: \ext{\cdot}^*, P)$, which differs from the normal semantics as follows:
806: \begin{itemize}
807: \item A state $s \in Q^*$ maps array variables to {\em finite partial}
808: functions (ie.\ defined only on a finite subset of their domains)
809: instead of total functions, but we insist that, for all array
810: variables $a$ with type $\Array{X}{Y}$, the partial function $s(a)$ is
811: defined at $s(x)$ for all variables $x$ of type $X$.
812: \item The relation $\Delta_I$ is amended to $\Delta^*_I$ so that
813: $s \Delta^*_I s'$ imposes a different condition for array variables:
814: \begin{itemize}
815: \item for each array variable $a$, and for each $v \in {\cal I}(X)$,\\
816: \begin{tabular}{l}
817: if there are variable $x$ and $y$ such that \\ \quad
818: $\Write{a}{x}{y}$ is in $I$ and $s(x) = v$, then $s'(a)(v) = s(y)$, \\
819: else if there does not exist an $x$ variables such that \\
820: \quad $x :=\ ?$ is in $I$ and $s'(x) = v$ and $s(a)(v) = \bot$, \\
821: \quad then $s'(a)(v) = s(a)(v)$.
822: \end{tabular}
823: \end{itemize}
824: \end{itemize}
825: (Note that the final ``if'' has no ``else'' case --- ie.\ the
826: statement holds when the ``if'' condition is false.) The ``else''
827: clause of the arrays case above could be read as follows: if there is
828: a variable $x$ which is non-deterministically selected to $v$ during
829: the transition, where $a$ was undefined at $v$ before, then the new
830: value of $a$ at $v$ is unspecified; otherwise it must remain the same.
831:
832: {\bf Notation:} We write $f(v) = \bot$ to mean $f$ is undefined at
833: $v$, and use the conventions that $\bot = \bot$ and $\bot \neq w$ for
834: any value $w$.
835:
836: \subsection{Equivalent programs without arrays}
837:
838: \label{sub:translation}
839:
840: Here we provide a syntactic translation from programs with arrays to
841: programs without arrays.
842:
843: We begin by extending our language slightly to allow sequences of
844: guarded commands to be executed in one atomic transition. Note we say
845: {\em command} to mean the multiple assignment $I$ in a guarded command
846: $e \longrightarrow I$.
847:
848: \begin{definition}
849: We can {\em append} a guarded command $e_2 \longrightarrow I_2$ onto a
850: command $I_1$, to form a single command $I_1 : e \longrightarrow I_2$.
851: The semantics of the new command are $s \Delta_{I_1 : e
852: \longrightarrow I_2} s''$ if and only if either
853: \begin{itemize}
854: \item there exists $s'$ such that $s \Delta_{I_1} s'$ and $s'
855: \Delta_{I_2} s''$ and $E_{s'}(e) = \true$, or
856: \item $s \Delta_{I_1} s''$ and $E_{s''}(e) = \false$.
857: \end{itemize}
858: \end{definition}
859: Note it is possible to append many guarded commands onto a single
860: command.
861:
862: We will also need to split commands into two as follows: a command $I$
863: can be split into its $X$-type assignments $I_X$ and $Y$-type and
864: boolean assignments $I_Y$ as follows:
865: \begin{itemize}
866: \item $I_X$ contains exactly all the assignments of the form $x :=
867: x'$ and $x :=\ ?$ from $I$.
868: \item $I_Y$ contains exactly all the assignments of the form $y :=
869: y'$, $y :=\ ?$, $\Write{a}{x}{y}$, $\Read{y}{a}{x}$, $b := e$ from $I$.
870: \end{itemize}
871:
872: We now provide the syntactic translation from programs with arrays to
873: programs without arrays. From a program ${\cal P}$, we can form its
874: {\em array-free abstraction} $\cal P^\sharp$ as follows.
875: \begin{itemize}
876: \item For each array $a$ and each variable $x$ of type $X$, we add a
877: new variable of type $Y$, which we will call $ax$.
878: \item $\cal P^\sharp$ contains no arrays.
879: \item Perform a translation on each command $I$ to form a
880: new command $I^\sharp_Y : \true \longrightarrow I^\sharp_X$ as follows:
881: \begin{enumerate}
882: \item The multiple assignment $I^\sharp_Y$ is the same as $I_Y$ except:
883: \begin{itemize}
884: \item for each $\Read{y}{a}{x}$ appearing in $I$, we instead
885: have $y := ax$ in $I^\sharp_Y$;
886: \item for each $\Write{a}{x}{y}$ appearing in $I$, we instead
887: have $ax := y$ in $I^\sharp_Y$.
888: \end{itemize}
889: For each $\Write{a}{x}{y}$ appearing in $I$, append onto
890: $I^\sharp_Y$ the following guarded command for each other variable
891: $x'$ (in any order):
892: $$
893: x = x' \longrightarrow ax' := ax.
894: $$
895: \item The multiple assignment $I^\sharp_X$ is the same as $I_X$ except:
896: \begin{itemize}
897: \item for each $x := x'$ appearing in $I$, we also have $ax :=
898: ax'$ in $I^\sharp_X$ for all arrays $a$.
899: \item for each $x :=\ ?$ appearing in $I$, we also have $ax :=\ ?$
900: in $I^\sharp_X$ for all arrays $a$.
901: \end{itemize}
902: For each $x :=\ ?$ appearing in $I$, append onto $I^\sharp_X$ the
903: following guarded command for each other variable $x'$ of type $X$
904: such that $x' :=\ ?$ is not in $I$ (in any order):
905: $$
906: x = x' \longrightarrow a_1 x, ..., a_l x := a_1 x', ..., a_l x'
907: $$
908: for all the arrays $a_1, ..., a_l$.
909:
910: Let $x_1, \ldots, x_n$ be any enumeration of all the variables of
911: type $X$ such that $x :=\ ?$ appears in $I$. Append further onto
912: $I^\sharp_X$, for each pair $i$ and $j$ both from $1$ to $n$ such
913: that $i > j$, in lexicographical order of $(i, j)$, the guarded
914: command:
915: $$
916: x_i = x_j \longrightarrow a_1 x_i, ..., a_l x_i := a_1 x_j, ..., a_l x_j
917: $$
918: for all the arrays $a_1, ..., a_l$.
919: \end{enumerate}
920: \end{itemize}
921:
922: %\begin{example}
923: %The guarded command
924: %$$
925: %x = x' \ \longrightarrow\ \{ \Write{a}{x}{y}, \Read{y}{a}{x}, x :=\
926: %?, x' :=\ x \}
927: %$$
928: %in a program with two variables $x$ and $x'$ of type $X$, would be
929: %converted to the following guarded command:
930: %$$
931: %\begin{array}{rrrcl}
932: %x = x' &\longrightarrow (&
933: %&& \{ ax := y, y := ax \}: \\
934: %&& x = x' &\longrightarrow& ax' := ax: \\
935: %&& \true &\longrightarrow& \{ x :=\ ?, x' :=\ x, ax :=\ ?, ax' :=\ ax \}: \\
936: %&& x = x' &\longrightarrow& ax := ax' \\
937: %&).&&& \\
938: %\end{array}
939: %$$
940: %\end{example}
941:
942: \begin{figure}
943: {\footnotesize
944: \begin{verbatim}
945: VARIABLES:
946: 1 addrBus: ADDR
947: 2 dataBus: DATA
948: 3 data1, data2, data3: DATA
949: 4 mem1_addrBus, mem1_testAddr, mem2_addrBus, mem2_testAddr, mem3_addrBus,
950: mem3_testAddr: DATA
951: 5# testAddr: ADDR
952: 6# testData: DATA
953: 7# testWritten: BOOL
954: 8# faults: {0..2}
955:
956: START:
957: 1# faults, testWritten := 0, false
958: 2 goto LOOP
959:
960: LOOP:
961: 1 dataBus := ?
962: : addrBus, mem1_addrBus, mem2_addrBus, mem3_addrBus := ?, ?, ?, ?
963: : if addrBus = testAddr then mem1_addrBus, mem2_addrBus, mem3_addrBus :=
964: mem1_testAddr, mem2_testAddr, mem3_testAddr
965: 2 goto READ |~| goto WRITE |~| goto FAULT
966:
967: READ:
968: 1 data1, data2, data3 := mem1_addrBus, mem2_addrBus, mem3_addrBus
969: 2 if data1 != data2 then dataBus := data3 else dataBus := data1
970: 3# if addrBus = testAddr and testWritten and faults < 2 and dataBus != testData
971: then goto ERROR
972: 4 goto LOOP
973:
974: WRITE:
975: 1 mem1_addrBus, mem2_addrBus, mem3_addrBus := dataBus, dataBus, dataBus
976: : if addrBus = testAddr then mem1_testAddr := mem1_addrBus
977: : if addrBus = testAddr then mem2_testAddr := mem2_addrBus
978: : if addrBus = testAddr then mem3_testAddr := mem3_addrBus
979: 2# if addrBus = testAddr then testData, testWritten := dataBus, true
980: 3 goto LOOP
981:
982: FAULT:
983: 1 mem1_addrBus := dataBus
984: : if addrBus = testAddr then mem1_testAddr := mem1_addrBus
985: |~|
986: mem2_addrBus := dataBus
987: : if addrBus = testAddr then mem2_testAddr := mem2_addrBus
988: |~|
989: mem3_addrBus := dataBus
990: : if addrBus = testAddr then mem3_testAddr := mem3_addrBus
991: 2# if faults < 2 then faults := faults + 1
992: 3 goto LOOP
993:
994: ERROR:
995: 1# goto ERROR
996: \end{verbatim}}
997: \caption{Array-free abstraction of fault-tolerant memory composed with
998: specification.
999: \label{fig:singleCacheTransl}}
1000: \end{figure}
1001:
1002: \begin{example}
1003: \label{ex:singleCacheTransl}
1004: The array-free abstraction of Example \ref{ex:singleCache} is shown in
1005: Figure \ref{fig:singleCacheTransl}. Note the use of the append
1006: operator \verb$:$ to group together instructions into one atomic
1007: transition.
1008: \end{example}
1009:
1010: \subsection{The connection}
1011:
1012: \label{sub:connection}
1013:
1014: We now identify the relationship between a program $\cal P$ and its
1015: array-free abstraction $\cal P^\sharp$. We show that, for infinite
1016: instantiations for the types $X$ and $Y$, there exists a bisimulation
1017: between the transition system produced using partial-functions
1018: semantics on $\cal P$ and the transition system produced using normal
1019: semantics on $\cal P^\sharp$. We first present some auxiliary
1020: definitions.
1021:
1022: \begin{definition}
1023: The set $\TERMS_X$ is the set of variables of type $X$, and if we
1024: write $s(\TERMS_X)$, it means the set $\{ s(x) \mid x \in \TERMS_X
1025: \}$. An {\em $X$-bijection} $\alpha$ on two states $s$ and $t$ is a
1026: bijection $\alpha : s(\TERMS_X) \rightarrow t(\TERMS_X)$ such that
1027: $\alpha(s(x)) = t(x)$ for all variables $x$ of type $X$.
1028: \end{definition}
1029:
1030: Given a program ${\cal P}$ and two infinite sets $A^*$ and
1031: $B^*$, let
1032: $$
1033: \begin{array}{rlcl}
1034: & \pfsem{\cal P}{A^*, B^*} &=& (Q^*, \delta^*,
1035: \ext{\cdot}^*, P) \\
1036: \mbox{ and } & \semi{\cal P^\sharp}{A^*, B^*} &=&
1037: (Q, \delta, \ext{\cdot}, P).
1038: \end{array}
1039: $$
1040:
1041: \begin{definition}
1042: \label{def:approx}
1043: We define the relation $\approx \: \subseteq Q \times Q^*$ as $s \approx
1044: t$ exactly when
1045: \begin{itemize}
1046: \item $s(b) = t(b)$ for boolean variables $b$,
1047: \item there exists a $X$-bijection on $s$ and $t$,
1048: \item $s(y) = t(y)$, for all variables $y$ of type $Y$, and
1049: \item $s(ax) = t(a[x])$, for all arrays $a$ and $X$-variables $x$.
1050: \end{itemize}
1051: Note that the range of $\approx$ is the whole of $Q^*$, while the
1052: domain of $\approx$ is only the states $s$ in $Q$ that satisfy the
1053: {\em array-consistency formula}
1054: $$
1055: \Sigma \quad \equiv \quad \forall x, x' \cdot x = x' \implies
1056: \forall a \cdot ax = ax'.
1057: $$
1058: \end{definition}
1059:
1060: Our aim is to prove that $\approx$ is a bisimulation. The proof relies
1061: on the following observation about $\pfsem{\cal P}{A^*, B^*}$: when a
1062: value $v$ of type $X$ is forgotten by the program (ie.\ it is
1063: overwritten in one of the variables of type $X$), the program's
1064: behaviour is unaffected if it never sees $v$ again, and so the
1065: corresponding $Y$-values in the arrays may also be forgotten. It
1066: therefore only needs to remember the parts of the array currently in
1067: view --- a finite number of values.
1068:
1069: This may appear to cause problems, because in reality that value could
1070: later be reintroduced (using $x :=\ ?$), and values from the arrays at
1071: $v$ then read. For an accurate model, these values would have to
1072: equal those originally written into the array, which the abstraction
1073: $\cal P^\sharp$ has forgotten. However, as the arrays are always
1074: undefined at places, an indistinguishable behaviour could happen
1075: anyway if a brand new $X$-value was chosen and the non-determinism was
1076: resolved in an appropriate way. Because the program is
1077: data-independent with respect to $X$, it has no way of telling that
1078: the new value is not the forgotten $v$.
1079:
1080: It is the $X$-bijection in the relation above that allows us to switch
1081: this forgotten value for a brand new one. The data independence of $Y$
1082: is not actually required here, but is used later to model check $\cal
1083: P^\sharp$.
1084:
1085: First, we present a result which allows us to break a command up into
1086: more manageable pieces.
1087:
1088: \begin{lemma}
1089: \label{lem:comp}
1090: For $s_1, s_3 \in Q^*$, we have $s_1 \Delta^*_I s_3$ if and only if
1091: there exists a state $s_2 \in Q^*$ such that $s_1 \Delta^*_{I_Y}
1092: s_2$ and $s_2 \Delta^*_{I_X} s_3$.
1093: \end{lemma}
1094: \begin{proof*} $\Rightarrow$:
1095: Define $s_2$ as follows:
1096: $$
1097: \begin{array}{rcl}
1098: s_2(b) &=& s_3(b), \mbox{ for $b$ of type $\mathbbm B$},\\
1099: s_2(x) &=& s_1(x), \mbox{ for $x$ of type $X$},\\
1100: s_2(y) &=& s_3(y), \mbox{ for $y$ of type $Y$},\\
1101: s_2(a)(v) &=& s_1(y), \mbox{ if $\Write{a}{x}{y}$ is in $I$ and
1102: $s_1(x) = v$},\\
1103: &=& s_1(a)(v), \mbox{ otherwise}.
1104: \end{array}
1105: $$
1106: Now we prove that $s_1 \Delta^*_{I_Y} s_2$:
1107: \begin{itemize}
1108: \item $b := e$ in $I_Y$ implies it's also in $I$, so $s_2(b) = s_3(b)
1109: = s_1(e)$; else $s_2(b) = s_3(b) = s_1(b)$.
1110: \item There are no $x := x'$ or $x :=\ ?$ in $I$, and $s_2(x) =
1111: s_1(x)$ by definition.
1112: \item If $y := y'$ in $I_Y$ then it's also in $I$, so $s_2(y) = s_3(y) =
1113: s_1(y)$; else $\Read{y}{a}{x}$ in $I_Y$ implies it's also in $I$, so
1114: $s_2(y) = s_3(y) = s_1(a)(s_1(x))$; else, if $y :=\ ?$ is not in $I_Y$
1115: then it's not in $I$ either, so $s_2(y) = s_3(y) = s_1(y)$.
1116: \item For each array $a$ and $v \in A^*$
1117: \begin{itemize}
1118: \item If $\Write{a}{x}{y}$ is in $I$ and $s_1(x) = v$, then
1119: $s_2(a)(v) = s_1(y)$ by definition.
1120: \item Else $s_2(a)(v) = s_1(a)(v)$ as there is no $x :=\ ?$ in
1121: $I_Y$.
1122: \end{itemize}
1123: \end{itemize}
1124: Now we prove that $s_2 \Delta^*_{I_X} s_3$:
1125: \begin{itemize}
1126: \item There is no $b := e$ in $I_X$, and $s_3(b) = s_2(b)$ by
1127: definition of $s_2$.
1128: \item If $x := x'$ in $I_X$ then it's in $I$, and so $s_3(x) =
1129: s_1(x') = s_2(x')$; else if $x :=\ ?$ is not in $I_X$, then it's
1130: not in $I$, so $s_3(x) = s_1(x) = s_2(x)$.
1131: \item For each array $a$ and $v \in A^*$
1132: \begin{itemize}
1133: \item There is no $\Write{a}{x}{y}$ in $I_X$.
1134: \item so assume there does not exist an $x :=\ ?$ in $I_X$ such
1135: that $s_3(x) = v$ and $s_2(a)(v) = \bot$. Then there does not
1136: exist such an $x :=\ ?$ in $I$ such that $s_3(x) = v$ and
1137: $s_1(a)(v) = s_2(a)(v) = \bot$ (by definition of $s_2$), so
1138: $s_3(a)(v) = s_1(a)(v) = s_2(a)(v)$ (again by definition of
1139: $s_2$).
1140: \end{itemize}
1141: \end{itemize}
1142:
1143: $\Leftarrow$: Assume $s_1 \Delta^*_{I_Y} s_2$ and $s_2 \Delta^*_{I_X}
1144: s_3$. We will now prove $s_1 \Delta^*_I s_3$:
1145: \begin{itemize}
1146: \item If $b := e$ is in $I$ then $b := e$ is in $I_Y$, so $s_2(b) =
1147: E_{s_1}(e)$. There are no boolean assignments in $I_X$ so $s_3(b)
1148: = s_2(b)$; if $b := e$ is not in $I$, then there are no boolean
1149: assignments in either $I_Y$ or $I_X$, so $s_3(b) = s_1(b)$.
1150: \item The cases for data variables are very similar to those for
1151: boolean variables.
1152: \item For each array variable $a$ and each $v \in A^*$,
1153: \begin{itemize}
1154: \item If there are $x$ and $y$ variables such that
1155: $\Write{a}{x}{y}$ is in $I$ and $s_1(x) = v$, then
1156: $\Write{a}{x}{y}$ will also appear in $I_Y$. There are no
1157: writes in $I_X$, and $s_2(a)(s_2(x))$ can not be $\bot$ so
1158: $s_3(a)(v) = s_2(a)(v)$. We get $s_3(a)(v) = s_2(a)(v) = y$.
1159: \item Otherwise assume there does not exist an $x :=\ ?$ in $I$
1160: such that $s_3(x) = v$ and $s_1(a)(v) = \bot$. Then there cannot
1161: exists an $x :=\ ?$ in $I_X$ such that $s_3(x) = v$ and
1162: $s_2(a)(v) = \bot$, because $s_2(a)(v) = s_1(a)(v)$ (no
1163: $\Write{a}{x}{y}$ in $I_Y$). Therefore, we have $s_3(a)(v) =
1164: s_2(a)(v) = s_1(a)(v)$. \mathproofbox
1165: \end{itemize}
1166: \end{itemize}
1167: \end{proof*}
1168:
1169: In the following five lemmas, which all have $s \approx t$ as a premise,
1170: let $\alpha$ be the $X$-bijection from $s$ to $t$.
1171:
1172: \begin{lemma}
1173: \label{lem:E}
1174: If $s \approx t$, then $E_s(e) = E_t(e)$ for any boolean expression $e$.
1175: \end{lemma}
1176: \begin{proof}
1177: From $s \approx t$, we know
1178: \begin{itemize}
1179: \item $E_s(b) = E_t(b)$, because $s(b) = t(b)$ for all booleans
1180: variables $b$,
1181: \item $E_s(y = y') = E_t(y = y')$, because $s(y) = t(y)$ for all
1182: variables $y$ of type $Y$,
1183: \item and also,
1184: $$
1185: \begin{array}{rl}
1186: & E_t(x = x')\\
1187: =& (t(x) = t(x'))\\
1188: =& (\alpha(s(x)) = \alpha(s(x')))\\
1189: =& \pstep{$\alpha$ is a bijection}\\
1190: & (s(x) = s(x'))\\
1191: =& E_s(x = x').
1192: \end{array}
1193: $$
1194: \end{itemize}
1195: By structural induction on $e$, using the above as base cases, it
1196: can easily be shown that $E_s(e) = E_t(e)$.
1197: \end{proof}
1198:
1199: \begin{lemma}
1200: \label{lem:Y1}
1201: If $s \approx t$ and $s \Delta_{I^\sharp_Y} s'$, then there exists $t'$
1202: such that $s' \approx t'$ and $t \Delta^*_{I_Y} t'$.
1203: \end{lemma}
1204: \begin{proof*}
1205: Define $t'$ as follows:
1206: $$
1207: \begin{array}{rcl}
1208: t'(b) &=& s'(b),\\
1209: t'(x) &=& \alpha(s'(x)),\\
1210: t'(y) &=& s'(y),\\
1211: t'(a)(v) &=& s'(ax), \mbox{ if there is such an $x$ where $t'(x)
1212: = v$},\\
1213: &=& t(y), \mbox{ (else) if $\Write{a}{x}{y}$ is in $I_Y$ and
1214: $t(x) = v$},\\
1215: &=& t(a)(v), \mbox{ otherwise}.\\
1216: \end{array}
1217: $$
1218: We need to show that the first case for arrays is well-defined, that
1219: is: if $t'(x) = t'(x')$, then $s'(ax) = s'(ax')$. First notice:
1220: $$
1221: \begin{array}{rrcl}
1222: & t'(x) &=& t'(x')\\
1223: \implies & \alpha(s'(x)) &=& \alpha(s'(x'))\\
1224: \implies & && \pstep{$\alpha$ is a bijection}\\
1225: & s'(x) &=& s'(x').
1226: \end{array}
1227: $$
1228: Assuming $s'(x) = s'(x')$, it can be seen that if there is some
1229: $y$ such that $\Write{a}{x}{y}$ or $\Write{a}{x'}{y}$ are in $I_Y$,
1230: then the appendages on $I^\sharp_Y$ will make sure that $s'(ax) =
1231: s'(ax')$. If there are no writes to $a[x]$ nor $a[x']$ then both
1232: $ax$ and $ax'$ are unaffected between $s$ and $s'$, and we get
1233: $$
1234: \begin{array}{rrcl}
1235: & t'(x) &=& t'(x')\\
1236: \implies & && \pstep{$x$ and $x'$ not affected in $I_Y$}\\
1237: & t(x) &=& t(x')\\
1238: \implies & t(a)(t(x)) &=& t(a)(t(x'))\\
1239: \implies & t(a[x]) &=& t(a[x'])\\
1240: \implies & && \pstep{$s \approx t$}\\
1241: & s(ax) &=& s(ax')\\
1242: \implies & && \pstep{$ax$ and $ax'$ unaffected in $I^\sharp_Y$}\\
1243: & s'(ax) &=& s'(ax')
1244: \end{array}
1245: $$
1246:
1247: From the definition of $t'$, notice that $t'(a[x]) = s'(ax)$ for all
1248: $x$. Notice further that $s' \approx t'$.
1249:
1250: We now wish to show that $t \Delta^*_{I_Y} t'$. We will run through the
1251: cases from the definition of $\Delta^*$.
1252: \begin{itemize}
1253: \item For any boolean variables $b$, either we have (a) $b := e$ in
1254: $I_Y$, in which case $b := e$ also appears in $I^\sharp_Y$ as the
1255: only assignment to $b$, so $t'(b) = s'(b) = E_{s}(e) = E_{t}(e)$
1256: (the last step by Lemma \ref{lem:E}); otherwise (b) there is no
1257: assignment to $b$ in $I_Y$, so $t'(b) = s'(b) = s(b) = t(b)$ (last
1258: step by $s \approx t$).
1259: \item There are no assignments to variables of type $X$ in $I_Y$,
1260: and
1261: $$
1262: \begin{array}{rl}
1263: & t'(x)\\
1264: =& \pstep{definition}\\
1265: & \alpha(s'(x))\\
1266: =& \pstep{no assignments to $x$ in $I^\sharp_Y$}\\
1267: & \alpha(s(x))\\
1268: =& \pstep{$\alpha$ is $X$-bijection}\\
1269: & t(x).
1270: \end{array}
1271: $$
1272: \item If $y := y'$ is in $I_Y$, then
1273: $$
1274: \begin{array}{rl}
1275: & t'(y)\\
1276: =& s'(y)\\
1277: =& \pstep{$y := y'$ is in $I^\sharp_Y$}\\
1278: & s(y')\\
1279: =& \pstep{$s \approx t$}\\
1280: & t(y').
1281: \end{array}
1282: $$
1283: If $\Read{y}{a}{x}$ is in $I_Y$ then
1284: $$
1285: \begin{array}{rl}
1286: & t'(y)\\
1287: =& s'(y)\\
1288: =& \pstep{$y := ax$ is in $I^\sharp_Y$}\\
1289: & s(ax)\\
1290: =& \pstep{$s \approx t$}\\
1291: & t(a[x]).\\
1292: \end{array}
1293: $$
1294: Otherwise, assume $y :=\ ?$ is not in $I_Y$. Therefore it's not
1295: in $I^\sharp_Y$, so $t'(y) = s'(y) = s(y) = t(y)$.
1296: \item For an array $a$ and $v \in A^*$, cases arising from the
1297: definition of $\Delta^*$ are:
1298: \begin{itemize}
1299: \item If $\Write{a}{x}{y}$ is in $I_Y$ and $t(x) = v$, then one of
1300: the following cases from the definition of $t'$ applies.
1301: \begin{itemize}
1302: \item There is an $x$ such that $t'(x) = v$. In this case $ax :=
1303: y$ is in the first command of $I^\sharp_Y$, and there are no
1304: appendages on $I^\sharp_Y$ that change $ax$. So $t'(a)(v) =
1305: s'(ax) = s(y) = t(y)$.
1306: \item Or, as $\Write{a}{x}{y}$ and $t(x) = v$, we get $t'(a)(v)
1307: = t(y)$ by definition.
1308: \end{itemize}
1309: \item Else, one of the following applies (taking cases from the
1310: definition of $t'$).
1311: \begin{itemize}
1312: \item Suppose there is some $X$-variables such that $t'(x) = v$
1313: (and hence $t(x) = v$ as there are no $X$-type assignments in
1314: $I_Y$), then notice there is no $ax := y$ in $I^\sharp_Y$.
1315: Also, the appendages on $I^\sharp_Y$ do not affect $ax$,
1316: because if they did, it would mean there exists an $x'$ such
1317: that $t'(x') = t'(x) = v$ and $\Write{a}{x'}{y}$ is in $I_Y$,
1318: and we would be in the case above. So we get $t'(a)(v) =
1319: s'(ax) = s(ax) = t(a[x]) = t(a)(v)$.
1320: \item The $\Write{a}{x}{y}$ case of the definition of $t'(a)(v)$
1321: cannot hold here, as it would be dealt with above.
1322: \item Otherwise $t'(a)(v) = t(a)(v)$ by definition. \mathproofbox
1323: \end{itemize}
1324: \end{itemize}
1325: \end{itemize}
1326: \end{proof*}
1327:
1328: \begin{lemma}
1329: \label{lem:X1}
1330: If $s \approx t$ and $s \Delta_{I^\sharp_X} s'$, then there exists $t'$
1331: such that $s' \approx t'$ and $t \Delta^*_{I_X} t'$.
1332: \end{lemma}
1333: \begin{proof*}
1334: Define a function $\alpha'$ on $s'(\TERMS_X)$ as follows:
1335: $$
1336: \begin{array}{rcll}
1337: \alpha'(v) &=& F(v), & \mbox{if for all $X$-type variables $x$,}\\
1338: &&& \mbox{ $s'(x) = v$ implies $x :=\ ?$ is in $I_X$,}\\
1339: &=& \alpha(v), & \mbox{otherwise,}
1340: \end{array}
1341: $$
1342: where $F$ is any injection from $s'(\TERMS_X)$ to $A^*
1343: \setminus t(\TERMS_X)$ (fresh values for $t'$ from the type $X$). We
1344: also restrict the range of $F$ to values which are undefined in all
1345: of the functions $t(a)$ for all arrays $a$. This still leaves an
1346: infinite number of values as the finite number of arrays are each
1347: finite partial functions.
1348:
1349: We need to show that $\alpha'$ is well-defined, specifically that
1350: $\alpha(v)$ is defined in the second case for $v$ equal to some
1351: $s'(x)$. So assume there exists an $x$ such that $s'(x) = v$ and
1352: $x :=\ ?$ is not in $I_X$. So $x' :=\ ?$ cannot be in $I^\sharp_X$
1353: either.
1354: \begin{itemize}
1355: \item If there are no assignments to $x$ in $I^\sharp_X$ then
1356: $s'(x) = s(x)$. Therefore $v = s(x) \in s(\TERMS_X) =
1357: \dom(\alpha)$.
1358: \item If there is an assignment $x := x'$ in $I^\sharp_X$, then
1359: $s'(x) = s(x')$, so $v \in \dom(\alpha)$.
1360: \end{itemize}
1361:
1362: Now we can define $t'$ as follows:
1363: $$
1364: \begin{array}{rcl}
1365: t'(b) &=& s'(b),\\
1366: t'(x) &=& \alpha'(s'(x)),\\
1367: t'(y) &=& s'(y),\\
1368: t'(a)(v) &=& s'(ax), \mbox{ if there is such an $x$ where $t'(x)
1369: = v$},\\
1370: &=& t(a)(v), \mbox{ otherwise}.\\
1371: \end{array}
1372: $$
1373: Once more we need to prove that this is well-defined for the
1374: first case for arrays: we must have $t'(x) = t'(x')$ implies $s'(ax)
1375: = s'(ax')$. Notice that $\alpha'$ is injective because $\alpha$ and
1376: $F$ are injections with non-overlapping ranges. Therefore
1377: $$
1378: \begin{array}{rrcl}
1379: & t'(x) &=& t'(x')\\
1380: \implies& \alpha'(s'(x)) &=& \alpha'(s'(x'))\\
1381: \implies & && \pstep{$\alpha'$ is injective}\\
1382: & s'(x) &=& s'(x').
1383: \end{array}
1384: $$
1385: By look at the appendages on $I^\sharp_X$, it can be seen that
1386: $s'(x) = s'(x')$ implies $s'(ax) = s'(ax')$ when either of $x :=\ ?$
1387: or $x' :=\ ?$ are in $I^\sharp_X$. In more detail: if only $x :=\ ?$
1388: is in $I^\sharp_X$, then the first set of appendages will execute
1389: $ax :=\ ?$; similarly for $x'$; if both $x :=\ ?$ and $x' :=\ ?$ are
1390: in $I^\sharp_X$, the second set of appendages will ensure they are
1391: both eventually set to the least (see definition of $I^\sharp_X$ for
1392: this ordering) $ax_i$ such that $s'(x_i) = s'(x) = s'(x')$.
1393:
1394: When the appendages do not affect either $ax$ or $ax'$, we are left
1395: with the following cases:
1396: \begin{itemize}
1397: \item There are no assignments to either $x$ or $x'$ in
1398: $I^\sharp_X$. In which case there are no assignments to $ax$ or
1399: $ax'$ in $I^\sharp_X$ either, and the argument runs the same as
1400: the proof that $t'(x) = t'(x') \longrightarrow s'(ax) = s'(ax')$
1401: in the corresponding part of in Lemma \ref{lem:Y1}.
1402: \item There is no assignment to $x'$, but there is an assignment $x
1403: := x''$ in $I^\sharp_X$, in which case there is also an assignment
1404: $ax := ax''$ by construction of $I^\sharp_X$. We get:
1405: $$
1406: \begin{array}{rrcl}
1407: & t'(x) &=& t'(x')\\
1408: \implies & && \pstep{$x'$ not affected, $x := x''$ in $I_X$}\\
1409: & t(x'') &=& t(x')\\
1410: \implies & t(a)(t(x'')) &=& t(a)(t(x'))\\
1411: \implies & t(a[x'']) &=& t(a[x'])\\
1412: \implies & && \pstep{$s \approx t$}\\
1413: & s(ax'') &=& s(ax')\\
1414: \implies & && \pstep{$ax'$ unaffected, $ax := ax''$ in $I^\sharp_X$}\\
1415: & s'(ax) &=& s'(ax')
1416: \end{array}
1417: $$
1418: \item The cases for an assignment to only $x'$, or to both $x$ and
1419: $x'$, run similarly.
1420: \end{itemize}
1421:
1422: Notice that $\alpha'$ forms an $X$-bijection from $s$ to $t$.
1423: Notice further from the definition of $t'$ that $s' \approx t'$.
1424:
1425: We now wish to show that $t \Delta^*_{I_X} t'$.
1426: \begin{itemize}
1427: \item There are no boolean assignments in either $I^\sharp_X$ or
1428: $I_X$, so $t'(b) = s'(b) = s(b) = t(b)$.
1429: \item There are no assignments to variables of type $Y$ either.
1430: \item If $x := x'$ is in $I_X$ then
1431: $$
1432: \begin{array}{rl}
1433: & t'(x)\\
1434: & \pstep{definition of $t'$}\\
1435: =& \alpha'(s'(x))\\
1436: =& \pstep{$x := x'$ is in $I^\sharp_X$}\\
1437: & \alpha'(s(x'))\\
1438: =& \pstep{$s(x') = s'(x)$ and $x :=\ ?$ not in $I_X$}\\
1439: & \alpha(s(x'))\\
1440: =& \pstep{$s \approx t$}\\
1441: & t(x').
1442: \end{array}
1443: $$
1444: Otherwise, assume neither $x :=\ ?$ nor $x := x'$ in $I_X$.
1445: Therefore neither are in $I^\sharp_X$, so $t'(x) = \alpha'(s'(x))
1446: = \alpha'(s(x)) = \alpha(s(x)) = t(x)$, similarly to above.
1447: \item For an array $a$ and $v \in A^*$, taking cases from the
1448: definition of $\Delta^*$ for arrays.
1449: \begin{itemize}
1450: \item There is no $\Write{a}{x}{y}$ in $I_X$.
1451: \item Assume that there are no $X$-type variables $x$ such that $x
1452: :=\ ?$ is in $I_X$ and $t'(x) = v$ and $t(a)(v) = \bot$. It
1453: remains to show that $t'(a)(v) = t(a)(v)$.
1454:
1455: If the second case in the definition of $t'$ is invoked, then we
1456: get $t'(a)(v) = t(a)(v)$ immediately. So suppose instead that
1457: there is an $x$ where $t'(x) = v$. We will now proceed by cases
1458: on the command $I_X$.
1459: \begin{itemize}
1460: \item Suppose there is no assignment to $x$ in $I_X$. Then there
1461: are no assignments to $x$ or $ax$ in $I^\sharp_X$. (There
1462: will be no assignments to $ax$ in the appendages on
1463: $I^\sharp_X$ because $x :=\ ?$ is not in $I$.) Starting with
1464: the definition of $t'$, we get $t'(a)(v) = s'(ax) = s(ax) =
1465: t(a[x]) = t(a)(t(x))$. Also note $t(x) = t'(x) = v$ because
1466: there's no assignment to $x$ in $I_X$.
1467: \item Suppose there is some $x'$ such that $x := x'$ is in
1468: $I_X$, so that $ax := ax'$ is in $I^\sharp_X$. There will be
1469: no assignment to $ax$ in the appendages on $I^\sharp_X$
1470: because $x :=\ ?$ cannot be in $I$. We get
1471: $$
1472: \begin{array}{rl}
1473: & t'(a)(v)\\
1474: =& \pstep{by definition}\\
1475: & s'(ax)\\
1476: =& \pstep{$ax := ax'$ is in $I^\sharp_X$}\\
1477: & s(ax')\\
1478: =& \pstep{$s \approx t$}\\
1479: & t(a[x'])\\
1480: =& t(a)(t(x'))\\
1481: =& \pstep{$x := x'$ is in $I_X$}\\
1482: & t(a)(t'(x))\\
1483: =& t(a)(v)\\
1484: \end{array}
1485: $$
1486: \item We are left with the case that $x :=\ ?$ is in $I_X$. We
1487: will split this case further:
1488:
1489: (a) If there is no $x'$ such that $x' :=\ ?$ is not in $I_X$
1490: and $s'(x') = s'(x)$, then
1491: $$
1492: \begin{array}{rl}
1493: & t(a)(v)\\
1494: =& \pstep{how $v$ was introduced}\\
1495: & t(a)(t'(x))\\
1496: =& \pstep{definition of $t'$}\\
1497: & t(a)(\alpha'(s'(x)))\\
1498: =& \pstep{definition of $\alpha'$}\\
1499: & t(a)(F(s'(x)))\\
1500: =& \pstep{definition of $F$}\\
1501: & \bot.
1502: \end{array}
1503: $$
1504: By assumption above we are finished with this case. This
1505: is because the semantics of $\Delta^*$ make no requirements
1506: for $t'(a)(v)$ when $x :=\ ?$ is in $I_X$ and $t'(x) = v$
1507: and $t(a)(v) = \bot$.
1508:
1509: (b) Otherwise, there does exist an $x'$ such that $x' :=\ ?$
1510: is not in $I_X$ and $s'(x') = s'(x)$. Notice that $s'(x')
1511: \in s(\TERMS_X) = \dom(\alpha)$ because $x' :=\ ?$ is not in
1512: $I_X$, and we can show
1513: $$
1514: \begin{array}{rl}
1515: & v\\
1516: =& t'(x)\\
1517: =& \pstep{definition of $t'$}\\
1518: & \alpha'(s'(x))\\
1519: =& \pstep{definition of $\alpha'$}\\
1520: & \alpha(s'(x))\\
1521: =& \pstep{$s'(x') = s'(x)$}\\
1522: & \alpha(s'(x'))\\
1523: =& t(x').\\
1524: \end{array}
1525: $$
1526: As $x' :=\ ?$ is not in $I_X$, we know that $t'(a)(t(x')) =
1527: t(a)(t(x'))$ because of the cases we've done already.
1528: Therefore $t'(a)(v) = t(a)(v)$. \mathproofbox
1529: \end{itemize}
1530: \end{itemize}
1531: \end{itemize}
1532: \end{proof*}
1533:
1534: \begin{lemma}
1535: \label{lem:Y2}
1536: If $s \approx t$ and $t \Delta^*_{I_Y} t'$, then there exists $s'$ such
1537: that $s' \approx t'$ and $s \Delta_{I^\sharp_Y} s'$.
1538: \end{lemma}
1539: \begin{proof*}
1540: Define
1541: $$
1542: \begin{array}{rcl}
1543: s'(b) &=& t'(b)\\
1544: s'(x) &=& \alpha^{-1}(t'(x))\\
1545: s'(y) &=& t'(y)\\
1546: s'(ax) &=& t'(a[x])\\
1547: \end{array}
1548: $$
1549: Clearly $s' \approx t'$ (using $\alpha$ as the $X$-bijection). We now
1550: wish to show that $s \Delta_{I^\sharp_Y} s'$.
1551: \begin{itemize}
1552: \item For boolean variables $b$, if $b := e$ is in $I^\sharp_Y$ then
1553: $b := e$ appears in $I_Y$ as the only assignment to $b$. We get
1554: $s'(b) = t'(b) = E_t(e) = E_s(e)$ by Lemma \ref{lem:E}. Otherwise
1555: $s'(b) = t'(b) = t(b) = s(b)$ by $s \approx t$.
1556: \item There are no assignments to variables of type $X$ in
1557: $I^\sharp_Y$ or $I_Y$ so $s'(x) = \alpha^{-1}(t'(x)) = \alpha^{-1}(t(x)) =
1558: s(x)$.
1559: \item
1560: \begin{itemize}
1561: \item If $y := y'$ is in $I^\sharp_Y$ then it must also be in $I_Y$,
1562: so $s'(y) = t'(y) = t(y') = s(y')$.
1563: \item if $y := ax$ is in $I^\sharp_Y$, then there must be
1564: $\Read{a}{x}{y}$ in $I_Y$. So $s'(y) = t'(y) = t(a[x]) = s(ax)$.
1565: \item else if there is no assignment to $y$ in $I^\sharp_Y$ then
1566: there's none in $I_Y$, so $s'(y) = t'(y) = t(y) = s(y)$.
1567: \end{itemize}
1568: \item For arrays $a$ and variables $x$ of type $X$,
1569: \begin{itemize}
1570: \item If there is an assignment $ax := y$ in the first multiple
1571: assignment of $I^\sharp_Y$, then the appendages on $I^\sharp_Y$
1572: should not affect $ax$ (see definition of $I^\sharp_Y$). Therefore
1573: we should have $s'(ax) = s(y)$. It also means $\Write{a}{x}{y}$
1574: in $I_Y$.
1575: $$
1576: \begin{array}{rl}
1577: & s'(ax)\\
1578: =& \pstep{definition of $s'$}\\
1579: & t'(a[x])\\
1580: =& \pstep{$\Write{a}{x}{y}$ in $I_Y$}\\
1581: & t(y)\\
1582: =& \pstep{$s \approx t$}\\
1583: & s(y).\\
1584: \end{array}
1585: $$
1586: \item Now assume there is no assignment $ax := y$ in the first
1587: multiple assignment. Splitting cases further:
1588: \begin{itemize}
1589: \item Assume there is no $x'$ such that $ax' := y'$ is in the
1590: first multiple assignment in $I^\sharp_Y$, where $s(x) =
1591: s(x')$. This ensures that the appendages on $I^\sharp_Y$ do
1592: not affect $ax$, because the condition $x' = x$ is never met,
1593: and we should get $s'(ax) = s(ax)$. By definition of
1594: $I^\sharp_Y$, this means that there is no $\Write{a}{x'}{y}$
1595: in $I_Y$ where $t(x) = t(x')$, so $t'(a)(t(x)) = t(a)(t(x))$.
1596: We now get:
1597: $$
1598: \begin{array}{rl}
1599: & s'(ax)\\
1600: =& \pstep{definition of $s'$}\\
1601: & t'(a[x])\\
1602: =& t'(a)(t'(x))\\
1603: =& \pstep{no assignments to $x$ in $I_Y$}\\
1604: & t'(a)(t(x))\\
1605: =& \pstep{no $\Write{a}{x'}{y}$ where $t(x) = t(x')$}\\
1606: & \pstep{and no $x :=\ ?$ in $I_Y$}\\
1607: & t(a)(t(x))\\
1608: =& t(a[x])\\
1609: & \pstep{$s \approx t$}\\
1610: =& s(ax)\\
1611: \end{array}
1612: $$
1613: \item Now assume there is an $x'$ such that $ax' := y'$ is in
1614: the first multiple assignment in $I^\sharp_Y$, where $s(x) =
1615: s(x')$. This means that the appendage $x' = x \longrightarrow
1616: ax := ax'$ should affect $ax$, and so we need to show that
1617: $s'(ax) = s(y')$.
1618:
1619: From the existence of $ax' := y'$ in $I^\sharp_Y$, we deduce
1620: $\Write{a}{x'}{y'}$ is in $I_Y$.
1621: \[
1622: \begin{array}{rl}
1623: & s'(ax)\\
1624: =& t'(a[x])\\
1625: =& t'(a)(t'(x))\\
1626: =& \pstep{no assignments to $x$ in $I_Y$}\\
1627: & t'(a)(t(x))\\
1628: =& \pstep{$s(x) = s(x')$ and $s \approx t$}\\
1629: & t'(a)(t(x'))\\
1630: =& \pstep{$\Write{a}{x'}{y'}$ in $I_Y$}\\
1631: & y'. \mathproofbox
1632: \end{array}
1633: \]
1634: \end{itemize}
1635: \end{itemize}
1636: \end{itemize}
1637: \end{proof*}
1638:
1639: \begin{lemma}
1640: \label{lem:X2}
1641: If $s \approx t$ and $t \Delta^*_{I_X} t'$, then there exists $s'$ such
1642: that $s' \approx t'$ and $s \Delta_{I^\sharp_X} s'$.
1643: \end{lemma}
1644: \begin{proof*}
1645: Define
1646: \[
1647: \begin{array}{rcl}
1648: s'(b) &=& t'(b)\\
1649: s'(x) &=& \alpha^{-1}(t'(x))\\
1650: s'(y) &=& t'(y)\\
1651: s'(ax) &=& t'(a[x])
1652: \end{array}
1653: \]
1654: Clearly $s' \approx t'$. Now to show $s \Delta_{I^\sharp_X} s'$:
1655: \begin{itemize}
1656: \item No boolean assignments in either $I_X$ or $I^\sharp_X$. So
1657: $s'(b) = t'(b) = t(b) = s(b)$.
1658: \item No assignments to any variable $y$ of type $Y$ either.
1659: \item For each $X$-type variable $x$,
1660: \begin{itemize}
1661: \item if $x := x'$ is in $I^\sharp_X$, then it's also in $I_X$. We
1662: get $s'(x) = \alpha^{-1}(t'(x)) = \alpha^{-1}(t(x')) = s(x')$;
1663: \item else if $x :=\ ?$ is not in $I^\sharp_X$, then it's not in
1664: $I_X$, so $s'(x) = s(x)$.
1665: \end{itemize}
1666: \item For each array $a$ and $X$-type variables $x$,
1667: \begin{itemize}
1668: \item Suppose there's no assignment to $ax$ in the first multiple
1669: assignment of $I^\sharp_X$. This means there is no assignment to
1670: $x$ in $I_X$, in which case $ax$ should not be affected by the
1671: appendages on $I^\sharp_X$ (because $x :=\ ?$ can not be in
1672: $I_X$). We therefore need to show $s'(ax) = s(ax)$, which can be
1673: done as follows:
1674: \[
1675: \begin{array}{rl}
1676: & s'(ax)\\
1677: =& t'(a[x])\\
1678: =& t'(a)(t'(x))\\
1679: =& \pstep{no assignment to $x$ in $I_X$}\\
1680: & t'(a)(t(x))\\
1681: =& \pstep{no $\Write{a}{x}{y}$ in $I_X$}\\
1682: & t(a)(t(x))\\
1683: =& t(a[x])\\
1684: =& \pstep{$s \approx t$}\\
1685: & s(ax).\\
1686: \end{array}
1687: \]
1688: \item Suppose there's an assignment $ax := ax'$ in $I^\sharp_X$,
1689: which means there's an assignment $x := x'$ in $I_X$. Again, the
1690: appendages should not affect $ax$, so we expect that $s'(ax) =
1691: s(ax')$. The proof runs similarly to the previous case, except
1692: that $t'(x) = t(x')$: $s'(ax) = t'(a[x]) = t'(a)(t'(x)) =
1693: t'(a)(t(x')) = t(a)(t(x')) = t(a[x']) = s(ax')$.
1694: \item We are left with the case that $ax :=\ ?$ is in
1695: $I^\sharp_X$, in which case $x :=\ ?$ is in $I_X$.
1696: \begin{itemize}
1697: \item Suppose $s'(x) \neq s'(x')$ for all other variables $x'$
1698: of type $X$. Then non of the appendages should affect $ax$,
1699: and the only assignment to $ax$ is the $ax :=\ ?$. In this
1700: case, $\Delta$ makes no demands on the value of $s'(ax)$.
1701: \item Suppose $s'(x) = s'(x')$ for some variables $x'$ where $x'
1702: :=\ ?$ is not in $I_X$. In this case, the first set of
1703: appendages should ensure that the command $ax := ax'$ is
1704: executed.
1705:
1706: The second set of appendages should not change $ax$. For
1707: suppose there is another $x''$ such that $s'(x) = s'(x'')$ and
1708: $x'' :=\ ?$ in $I_X$, then the assignment $ax := ax''$ will
1709: have no effect because the first set of appendages will also
1710: have performed $ax'' := ax'$.
1711:
1712: We can prove $s'(ax) = s'(ax')$ as follows:
1713: \[
1714: \begin{array}{rl}
1715: & s'(ax)\\
1716: =& \pstep{definition $t'$}\\
1717: & t'(a[x])\\
1718: =& t'(a)(t'(x))\\
1719: =& \pstep{$s'(x) = s'(x')$ and $s' \approx t'$}\\
1720: & t'(a)(t'(x'))\\
1721: =& t'(a[x'])\\
1722: =& s'(ax').
1723: \end{array}
1724: \]
1725: We have already established that $s'(ax')$ is correct with
1726: respect to the definition of $\Delta$ in one of the cases
1727: above, so $s'(ax)$ must also be correct.
1728: \item Suppose $s'(x) = s'(x')$ only for variables $x'$ where $x'
1729: :=\ ?$ is in $I_X$. In this case, the first set of appendages
1730: should not change $ax$, and the second set should ensure
1731: $s'(ax) = s'(ax')$, although this is all we need to show
1732: because one of these variables is nondeterministically
1733: selected in the first multiple assignment in $I^\sharp_X$.
1734: It can be shown as follows: $s'(ax) = t'(a[x]) =
1735: t'(a)(t'(x)) = t'(a)(t'(x')) = t'(a[x']) = s'(ax')$. \mathproofbox
1736: \end{itemize}
1737: \end{itemize}
1738: \end{itemize}
1739: \end{proof*}
1740:
1741: \begin{proposition}
1742: \label{prop:bisim}
1743: For any program $\cal P$, and any infinite sets $A^*$ and $B^*$, the
1744: relation $\approx$ forms a bisimulation between $\semi{\cal
1745: P^\sharp}{A^*, B^*}$ and $\pfsem{\cal P}{A^*, B^*}$.
1746: \end{proposition}
1747: \begin{proof*}
1748:
1749: The proof is presented in three parts: first the base condition,
1750: followed by the two successor conditions.
1751:
1752: \begin{enumerate}
1753: \item Assume $s \in Q$ and $t \in Q^*$ and $s \approx t$. Note
1754: $$
1755: \begin{array}{rl}
1756: & s \in \ext{b} \\
1757: \iff & \\
1758: & s(b) = \true \\
1759: \iff & \quad \{ s \approx t \} \\
1760: & t(b) = \true \\
1761: \iff & \\
1762: & t \in \ext{b}^*.
1763: \end{array}
1764: $$
1765: So for observables $p$, we have $s \in \ext{p}$ if and
1766: only if $t \in \ext{p}^*$.
1767:
1768: %The case for $t \approx s$ runs identically, swapping $s$ and $t$ above.
1769: \item Take any $s, s' \in Q$ and any $t \in Q^*$ such that $s \approx t$
1770: and $s' \in \delta(s)$. So there exists some $e \longrightarrow
1771: I^\sharp$ from $\cal P$ such that $E_s(e) = \true$ and $s
1772: \Delta_{I^\sharp} s'$.
1773:
1774: By Lemma \ref{lem:E}, we can shown $E_t(e) =
1775: \true$.
1776:
1777: By construction of $I^\sharp$, we know there exists $s''$ such that
1778: $s \Delta_{I^\sharp_Y} s''$ and $s'' \Delta_{I^\sharp_X} s$.
1779:
1780: By Lemma \ref{lem:Y1}, we know there exists $t''$ such that $t
1781: \Delta^*_{I_Y} t''$ and $s'' \approx t''$. By Lemma \ref{lem:X1}, we know
1782: there exists $t'$ such that $t'' \Delta^*_{I_X} t'$ and $s' \approx t'$.
1783: By Lemma \ref{lem:comp}, $t \Delta^*_I t'$.
1784: \item This case runs symmetrically to the above case. Use Lemma
1785: \ref{lem:comp} to show $t \Delta^*_I t'$ is equivalent to $t
1786: \Delta^*_{I_Y} t''$ and $t'' \Delta^*_{I_X} t'$ for some $t'' \in
1787: Q^*$. Use Lemmas \ref{lem:Y2} and \ref{lem:X2} instead where
1788: appropriate, and the last step should be replaced with the
1789: observation that $s \Delta_{I^\sharp_Y} s''$ and $s''
1790: \Delta_{I^\sharp_X} s'$ implies
1791: \[
1792: s \Delta_{I^\sharp_Y : \true \longrightarrow I^\sharp_X} s'
1793: \]
1794: by definition of $:$ the append operator. \mathproofbox
1795: \end{enumerate}
1796: \end{proof*}
1797:
1798: \subsection{Main theorem}
1799:
1800: \label{sub:conclusion}
1801:
1802: We are now ready to present our first main result: that the
1803: $\mu$-calculus model-checking problem is decidable for the class of
1804: systems generated from programs using partial-functions semantics and
1805: infinite instantiations for $X$ and $Y$.
1806:
1807: \begin{theorem}
1808: \label{thm:infinite}
1809: Given
1810: \begin{itemize}
1811: \item a program $\cal P$,
1812: \item a boolean variable $b_0$ of $\cal P$,
1813: \item a $\mu$-calculus formula $\varphi$ over the boolean variables
1814: of $\cal P$,
1815: \end{itemize}
1816: for any infinite sets $A^*$ and $B^*$ (over which equality
1817: is decidable), the model-checking problem $\pfsem{P}{A^*,
1818: B^*}, b_0 \models \varphi$ is decidable. Moreover, the answer
1819: is independent of which infinite sets $A^*$ and $B^*$ are
1820: used.
1821: \end{theorem}
1822: \begin{proof}
1823: The array-free abstraction ${\cal P}^\sharp$ of $\cal P$ is a
1824: data-independent program without arrays, and the array-consistency
1825: formula $\Sigma$ from Definition \ref{def:approx} uses only equality
1826: on the variables of ${\cal P}^\sharp$. Therefore, it is possible to
1827: generate a finite transition system $M$ which has the same
1828: observables as, and is bisimulation-equivalent to, the transition
1829: system $\semi{\cal P^\sharp}{A^*, B^*}$ using the algorithm in
1830: \cite{NK00} with $\Sigma$ as the initial condition\footnote{ The
1831: syntax of programs used in \cite{NK00} is almost identical to
1832: ours. The semantics are given in terms of weakest liberal
1833: precondition laws, which can be related to our operational
1834: semantics in the standard way \cite{Hoa69}. The append operator
1835: used here is easily integrated into \cite{NK00} using the weakest
1836: liberal precondition law $$\{\mathit{wlp}_{I_1} (\psi \wedge \neg
1837: e) \vee \mathit{wlp}_{I_1} (\mathit{wlp}_{I_2} (\psi) \wedge e) \}
1838: \quad I_1 : e \longrightarrow I_2 \quad \{ \psi \}.$$}.
1839:
1840: Also note that states related by some bisimulation have exactly the
1841: same true $\mu$-calculus formulas \cite{BCG88}.
1842:
1843: Using these facts we proceed as follows:
1844: \[
1845: \begin{array}{rl}
1846: & \pfsem{\cal P}{A^*, B^*}, b_0 \models \varphi\\
1847: \iff
1848: & \forall t \in \ext{b_0}^* \cdot \pfsem{\cal P}{A^*, B^*}, t
1849: \models \varphi\\
1850: \iff & \pstep{Proposition \ref{prop:bisim}
1851: and Definition \ref{def:approx}}\\
1852: & \forall s \in \ext{b_0}^\sharp \cdot \Sigma(s) \implies
1853: \semi{\cal P^\sharp}{A^*, B^*}, s \models \varphi\\
1854: \iff & \pstep{\cite{NK00}}\\
1855: & \forall u \in \ext{b_0} \cdot M, u \models \varphi\\
1856: \iff
1857: & M, b_0 \models \varphi.
1858: \end{array}
1859: \]
1860: Hence the problem can be solved by $\mu$-calculus finite-model
1861: checking, for example \cite{BC+92}.
1862:
1863: The independence of $A^*$ and $B^*$ comes from the fact that these
1864: sets are not actually used by \cite{NK00} in the construction of the
1865: finite transition system $M$.
1866: \end{proof}
1867:
1868: The above proof suggests the following procedure for model checking
1869: data-independent systems with arrays. Suppose a program $\cal P$ has
1870: $n_b$ boolean variables, $n_x$ variables of type $X$, $n_y$ variables
1871: of type $Y$, $n_a$ array variables, and $n_i$ guarded commands.
1872: \begin{enumerate}
1873: \item {\bf Translate $\cal P$ to its array-free abstraction $\cal
1874: P^\sharp$ using the procedure in Section \ref{sub:translation}.}
1875: The translation procedure will produce a program with the same
1876: number of boolean variables, $n_x$ variables of type $X$, $n_y + n_a
1877: n_x$ variables of type $Y$, and no array variables. The complexity
1878: of commands is increased due to the append operator and we will
1879: count each one as a separate command. There are a maximum of
1880: $\frac{1}{4} n_a n_x^2$ appendages added onto each $I^\sharp_Y$, and
1881: a maximum of $\frac{1}{2} n_a n_x^2$ added onto each $I^\sharp_X$.
1882: The total number of guarded commands in $\cal P^\sharp$ could be as
1883: high as
1884: \[
1885: n_i ( \frac{3 n_a n_x^2}{4} + 2 ).
1886: \]
1887: As this translation can be done instruction by instruction, its time
1888: complexity is equivalent to the above bound on the number of guarded
1889: commands that may appear in $\cal P^\sharp$.
1890: \item {\bf Translate $\cal P^\sharp$, under the initial condition of
1891: the array-consistency formula $\Sigma$, to the finite state
1892: transition system $M$ using the syntactic transformation procedure
1893: in \cite{NK00}.} This procedure would generate at most $n_x^2 +
1894: (n_y + n_a n_x)^2 + n_b$ predicates, and therefore would terminate
1895: in at most that number of steps\footnote{The complexity of each step
1896: of the algorithm in \cite{NK00} is not given, although it appears
1897: that the total complexity of the algorithm is at least in $\Omega(
1898: p^2 l )$, where $p$ is the number of predicates generated and $l$
1899: is the number of guarded commands.}. The number of states in $M$
1900: would be at most
1901: \[
1902: n_b n_x^{n_x} (n_y + n_a n_x)^{(n_y + n_a n_x)}.
1903: \]
1904: \item {\bf Model check $M$ using any finite-model-checking algorithm,
1905: eg \cite{BC+92}.} Finite-model checking of the $\mu$-calculus in
1906: general is {\em EXP\-SPACE} in the size of the model.
1907: \end{enumerate}
1908:
1909: Instead of steps 2 and 3 above, there are other ways we might solve
1910: $$\semi{P^\sharp}{A^*, B^*}, b_0 \models \varphi.$$
1911: One way would be
1912: to use a finite instantiation theorem \cite{LN00}. A more efficient
1913: way would be to design a region algebra and use the model-checking
1914: algorithm in \cite{HM00}. However, the syntactic translation in
1915: \cite{NK00} first generates a bisimulation-equivalent program with
1916: just boolean variables, and orthogonal techniques could be applied to
1917: that program before using it to generate the transition system $M$.
1918:
1919: \begin{figure}
1920: {\footnotesize
1921: \begin{verbatim}
1922: INITIALLY:
1923: addrBus = testData => (mem1_addrBus = mem1_testData /\
1924: mem2_addrBus = mem2_testData /\ mem3_addrBus = mem3_testData)
1925: \end{verbatim}}
1926: \caption{Initial condition for array-free abstraction of the
1927: fault-tolerant memory composed with specification.
1928: \label{fig:singleCacheInitially}}
1929: \end{figure}
1930:
1931: \begin{example}
1932: \label{ex:singleCacheInfinite}
1933: We will now begin to show how to check that the program in Example
1934: \ref{ex:singleCache} satisfies its specification.
1935:
1936: Following the steps outlined above:
1937: \begin{enumerate}
1938: \item The translation of the program $\cal P$ to its array-free
1939: abstraction $\cal P^\sharp$ is shown in Figure
1940: \ref{fig:singleCacheTransl}.
1941: \item The array-free abstraction $\cal P^\sharp$, together with the
1942: initial condition shown in Figure \ref{fig:singleCacheInitially}, can be
1943: converted to a finite state transition system $M$ as described in
1944: \cite{NK00}.
1945: \item We can now perform the check $M, b_0 \models \nu h: \varphi$, where
1946: $\varphi$ is $\forallnext (\overline{b_E} \wedge h)$.
1947: \end{enumerate}
1948: The proof of Theorem \ref{thm:infinite} tells us that the answer given
1949: by this check will be equivalent to the answer of $\pfsem{\cal
1950: P}{A^*, B^*}, b_0 \models \varphi$ for any infinite sets
1951: $A^*$ and $B^*$.
1952: \end{example}
1953:
1954: \section{Finite arrays}
1955:
1956: \label{sect:finite}
1957:
1958: In this section we present results about the class of programs with
1959: arbitrary non-empty finite sets as instantiations for their types. By
1960: showing the relationship between one transition system generated using
1961: infinite sets and all systems generated using finite sets, we are able
1962: to deduce how fragments of the $\mu$-calculus are preserved between
1963: them.
1964:
1965: \begin{proposition}
1966: \label{prop:simulation}
1967: For any non-empty finite sets $A$ and $B$, and infinite respective
1968: supersets $A^*$ and $B^*$, there exists a total simulation of
1969: $\semi{\cal P}{A, B}$ by $\pfsem{\cal P}{A^*, B^*}$.
1970: \end{proposition}
1971: \begin{proof*}
1972: Let
1973: $$
1974: \begin{array}{rlcl}
1975: & \semi{\cal P}{A, B} &=& (Q, \delta, \ext{\cdot}, P) \\
1976: \mbox{ and } & \pfsem{\cal P}{A^*, B^*} &=&
1977: (Q^*, \delta^*, \ext{\cdot}^*,
1978: P).
1979: \end{array}
1980: $$
1981:
1982: Define a total relation $\lhd \subseteq Q \times Q^*$ as $s \lhd t$ if and
1983: only if $s$ and $t$ are identical, except that for arrays $a$,
1984: we have $t(a)(v)$ is equal to $s(a)(v)$ if $v \in A$, and $\bot$ if $v
1985: \in A^* \setminus A$.
1986:
1987: For the first condition of simulation, observe that
1988: $$
1989: \begin{array}{rl}
1990: & s \in \ext{b} \\
1991: \iff & \\
1992: & s(b) = \true \\
1993: \iff & \quad \{ s \lhd t \} \\
1994: & t(b) = \true \\
1995: \iff & \\
1996: & t \in \ext{b}^*.
1997: \end{array}
1998: $$
1999: So for observables $p$, we have $s \in \ext{p}$ if
2000: and only if $t \in \ext{p}^*$.
2001:
2002: For the second condition, assume that $s \lhd t$ and $s' \in
2003: \delta(s)$. We need to show that there exists $t' \in Q^*$ such that
2004: $t' \in \delta(t)$ and $s' \lhd t'$.
2005:
2006: Define $t'$ by $s' \lhd t'$. As $s' \in \delta(s)$, there must exist a
2007: guarded command $e \longrightarrow I$ in ${\cal P}$ such that
2008: $E_{s}(e) = \true$ and $s \Delta_I s'$.
2009: \begin{itemize}
2010: \item $E_{t}(e) = E_{s}(e)$ by (an easy variation of) Lemma \ref{lem:E}.
2011: \item It remains to show $t \Delta^*_I t'$. We do only the case for
2012: arrays.
2013: \begin{itemize}
2014: \item for each array variable $a$, and for each $v \in A^*$,\\
2015: \begin{tabular}{l}
2016: if there are $x$ and $y$ variables such that \\
2017: \quad $\Write{a}{x}{y} \in I$ and $t(x) = v$, then \\
2018: \quad $t'(a)(v) = s'(a)(v) = s(y) = t(y)$. \\
2019: else either $t'(a)(v) = \bot = t(a)(v)$, \\
2020: \quad or $t'(a)(v) = s'(a)(v) = s(a)(v) = t(a)(v)$. \mathproofbox
2021: \end{tabular}
2022: \end{itemize}
2023: \end{itemize}
2024: \end{proof*}
2025:
2026: \begin{proposition}
2027: \label{prop:traces}
2028: For any infinite sets $A^*$ and $B^*$, if $\pi$ is a trace
2029: of $\pfsem{\cal P}{A^*, B^*}$, then there exist non-empty
2030: finite respective subsets $A$ and $B$ such that $\pi$ is a trace of
2031: $\semi{\cal P}{A, B}$.
2032: \end{proposition}
2033: \begin{proof}
2034: Let
2035: $$
2036: \pfsem{\cal P}{A^*, B^*} = (Q^*, \delta^*,
2037: \ext{\cdot}^*, P).
2038: $$
2039: If $\pi$ is a trace of $\pfsem{\cal P}{A^*, B^*}$, then
2040: there exists a sequence $t_1 t_2 ... t_l$ of states from $Q^*$ such
2041: that $t_{i+1} \in \delta^*(t_i)$ for $i = 1...l-1$, and $t_i \in
2042: \ext{ \pi(i) }$ for $i = 1...l$.
2043:
2044: As the functions representing arrays in these states are finite
2045: partial functions, they contain only finite subsets $A$ and $B$ of
2046: $A^*$ and $B^*$. We can now form the transition system
2047: $$
2048: \semi{\cal P}{A, B} = (Q, \delta, \ext{\cdot}, P).
2049: $$
2050:
2051: Form a state $s_l \in Q$ from $t_l$ as follows. Extending the
2052: partial functions in $t_l$ to total functions on $A$ by picking any
2053: $B$ values for the undefined locations. Now, working backwards from
2054: $i = l-1$ down to $i = 1$, form states $s_i \in Q$ by extending the
2055: partial functions in $t_i$ to total functions using the same values
2056: used for $s_{i+1}$.
2057:
2058: Formally,
2059: $$
2060: \begin{array}{rcl}
2061: s_i(b) &=& t_i(b), \\
2062: s_i(z) &=& t_i(z), \\
2063: s_i(a)(v) &=& t_i(a)(v), \mbox{ if defined, else} \\
2064: &=& \mbox{ anything, if } i = l, \\
2065: &=& s_{i+1}(a)(v), \mbox{ otherwise,} \\
2066: \end{array}
2067: $$
2068: for boolean variables $b$, data variables $z$, arrays variables
2069: $a$ and values $v$ from $A$.
2070:
2071: We now wish to show that $s_{i+1} \in \delta(s_i)$ for $i =
2072: 1...l-1$. As $t_{i+1} \in \delta^*(t_i)$, there must exist a
2073: guarded command $e \longrightarrow I$ in ${\cal P}$ such that
2074: $E_{t_i}(e) = \true$ and $t_i \Delta_I t_{i+1}$.
2075: \begin{itemize}
2076: \item $E_{t}(e) = E_{s}(e)$ by (an easy variation of) Lemma \ref{lem:E}.
2077: \item It remains to show $s_i \Delta^*_I s_{i+1}$. We do only the
2078: case for arrays.
2079: \begin{itemize}
2080: \item For each array $a$ and each $v \in A$,
2081: \begin{itemize}
2082: \item If $\Write{a}{x}{y} \in I$ and $s(x) = v$, then
2083: $s_{i+1}(a)(v) = t_{i+1}(a)(v)$, which must be defined because
2084: $t_i(x) = v$. From $t_i \Delta^*_I t_{i+1}$ we know
2085: $t_{i+1}(a)(v) = t_i(y)$, and by definition $s_i(y) = t_i(y)$.
2086: So $s_{i+1}(a)(v) = s_i(y)$.
2087: \item Else, if $t_{i+1}(a)(v)$ is defined anyway, $s_{i+1}(a)(v)
2088: = t_{i+1}(a)(v)$. Two cases arise from the definition of
2089: $\Delta^*$.
2090: \begin{itemize}
2091: \item Either there is an $x :=\ ?$ in $I$ and $t_{i+1}(x) = v$
2092: and $t_i(a)(v) = \bot$. The last of these means that
2093: $s_i(a)(v) = s_{i+1}(a)(v)$ by definition.
2094: \item Or $t_{i+1}(a)(v) = t_i(a)(v)$. Whether this is a value
2095: from $A$ or it is $\bot$, by definition $s_i(a)(v) =
2096: s_{i+1}(a)(v)$.
2097: \end{itemize}
2098: \end{itemize}
2099: \end{itemize}
2100: This is enough to show $s_i \Delta^*_I s_{i+1}$ for the arrays case.
2101: \end{itemize}
2102: This shows that the sequence $s_1...s_l$ is an execution sequence in
2103: $\semi{\cal P}{A, B}$. Notice also that $\ext{s_i} = \ext{t_i}$
2104: because they are equivalent at the boolean variables, so $\pi$ is a
2105: trace of $\semi{\cal P}{A, B}$.
2106: \end{proof}
2107:
2108: \begin{definition}
2109: The open formulas of the logic $L^\infty_4$ over a set of observables
2110: $P$ are generated by the grammar $\psi$:
2111: \[
2112: \psi ::= \bigvee_i \psi'_i\ ; \quad \psi' ::= p \mid h \mid \existsnext \psi',
2113: \]
2114: for $p \in P$ and variables $h$, where $\bigvee_i \psi'_i$ represents
2115: any countable disjunction of formulas from the grammar $\psi'$.
2116: \end{definition}
2117:
2118: Given a transition system ${\cal S} = (Q, \delta, \ext{\cdot}, P)$
2119: and a mapping from the variables to sets of states $\Epsilon$, any
2120: open formula $\varphi$ of $L^\infty_4$ over $P$ defines a set
2121: $\syns{\varphi}{\Epsilon} \subseteq Q$ of states:
2122: $$
2123: \begin{array}{l}
2124: \syns{p}{\Epsilon} = \ext{p} \\
2125: \syns{h}{\Epsilon} = \Epsilon(h) \\
2126: \syns{\existsnext \psi}{\Epsilon} = \{ s \in Q
2127: \mid \exists s' \in \delta(s) : s' \in
2128: \syns{\psi}{\Epsilon} \} \\
2129: \syns{\bigvee_i \psi_i}{\Epsilon} =
2130: \bigcup_i \syns{\psi_i}{\Epsilon}.
2131: \end{array}
2132: $$
2133:
2134: \begin{proposition}
2135: \label{prop:l4}
2136: Any closed $\mu$-calculus formula $\varphi \in L^\mu_4$ is semantically
2137: equivalent to a closed formula $\psi \in L^\infty_4$.
2138: \end{proposition}
2139: \begin{proof*}
2140: Define a function $F$ from open $L^\mu_4$ formulas to open $L^\infty_4$
2141: formulas. For ease of presentation, we will write disjunction as sets
2142: in the target language.
2143: \[
2144: \begin{array}{rcl}
2145: F(p) &=& \{ p \} \\
2146: F(h) &=& \{ h \} \\
2147: F(\varphi_1 \vee \varphi_2) &=& F(\varphi_1) \cup F(\varphi_2) \\
2148: F(\existsnext \varphi) &=& \mathrm{map} \ \existsnext \ F(\varphi) \\
2149: F(\mu h : \varphi) &=& \bigcup_{i \in \mathbbm{N}} \psi_i \\
2150: && \begin{array}{rcl}
2151: \mbox{where } \psi_0 &=& \{ \} \\
2152: \psi_{i+1} &=& N( \subst{F(\varphi)}{\psi_i}{h} ).
2153: \end{array}
2154: \end{array}
2155: \]
2156: The function $N$ is a function which normalises formulas from the
2157: grammar
2158: \[
2159: \psi'' ::= p \mid h \mid \bigvee_i \psi''_i \mid \existsnext \psi''
2160: \]
2161: to formulas from $L^\infty_4$, and is defined as follows:
2162: \[
2163: \begin{array}{rcl}
2164: N(p) &=& \{ p \} \\
2165: N(h) &=& \{ h \} \\
2166: N( \bigvee_i \psi_i ) &=& \bigcup_i \psi_i \\
2167: N( \existsnext \psi) &=& \{ \}, \mbox{ if } N(\psi) = \{ \} \\
2168: && \mathrm{map} \ \existsnext \ N(\psi), \mbox{ otherwise.}
2169: \end{array}
2170: \]
2171: Note that these functions are well defined as their definitions are
2172: inductive.
2173:
2174: It can be shown by structural induction that the function $N$
2175: preserves the semantics of formulas because $\existsnext$ distributes
2176: over disjunction and $\existsnext \false$ is equivalent to $\false$.
2177:
2178: It can further be shown that $F$ also preserves the semantics of
2179: formulas. We will do only the $\mu$ case, using a result from
2180: \cite{Sti92} due to the fixed-point theorem for continuous functions
2181: over complete partial orders which allows us to replace occurrences of
2182: $\mu$ in formulas with infinite disjunction.
2183: \[
2184: \begin{array}{rl}
2185: & \syns{\mu h : \varphi}{\Epsilon} \\
2186: =& \pstep{ \cite{Sti92} } \\
2187: & \begin{array}{l}
2188: \syns{\bigcup_{i \in \mathbbm{N}} \psi_i}{\Epsilon} \\
2189: \begin{array}{rcl}
2190: \mbox{ where } \psi_0 &=& \{\} \\
2191: \psi_{i+1} &=& \subst{\varphi}{\psi_i}{h} \\
2192: &=& \pstep{ induction hypothesis} \\
2193: && \subst{F(\varphi)}{\psi_i}{h} \\
2194: &=& \pstep{ $N$ preserves semantics} \\
2195: && N( \subst{F(\varphi)}{\psi_i}{h} ) \\
2196: \end{array}
2197: \end{array} \\
2198: =& \pstep { definition of $F$ } \\
2199: & \syns{ F( \mu h : \varphi) }{\Epsilon} \mathproofbox
2200: \end{array}
2201: \]
2202: \end{proof*}
2203:
2204: We now present our second main result, which relates the
2205: model-checking procedure for systems with infinite arrays presented in
2206: Section \ref{sect:infinite} to the parameterised model-checking
2207: problem for systems with finite arrays.
2208: \begin{theorem}
2209: \label{thm:finite}
2210: For
2211: \begin{itemize}
2212: \item a program $\cal P$,
2213: \item a boolean variable $b_0$ of $\cal P$,
2214: \item a $\mu$-calculus formula $\overline{\varphi}$ over the boolean variables
2215: of $\cal P$,
2216: \item infinite sets $A^*$ and $B^*$ (over which equality
2217: is decidable),
2218: \end{itemize}
2219: we have, for $A$ and $B$ necessarily finite non-empty subsets of
2220: $A^*$ and $B^*$ respectively:
2221: \begin{enumerate}
2222: \item For $\overline{\varphi}$ in the universal fragment of the $\mu$-calculus
2223: $\overline{L^\mu_2}$,
2224: \[
2225: \pfsem{\cal P}{A^*, B^*}, b_0 \models \overline{\varphi} \quad
2226: \Longrightarrow \quad \forall A, B \cdot \semi{\cal P}{A, B}, b_0
2227: \models \overline{\varphi}.
2228: \]
2229: \item For $\overline{\varphi}$ in the universal disjunction-free fragment of
2230: the $\mu$-calculus $\overline{L^\mu_4}$,
2231: \[
2232: \pfsem{\cal P}{A^*, B^*}, b_0 \models \overline{\varphi}
2233: \quad \Longleftrightarrow \quad
2234: \forall A, B \cdot \semi{\cal P}{A, B}, b_0 \models \overline{\varphi}.
2235: \]
2236: \end{enumerate}
2237: \end{theorem}
2238: \begin{proof}
2239: For Part 1, Notice:
2240: \[
2241: \begin{array}{rrcl}
2242: & \pfsem{\cal P}{A^*, B^*}, b_0 \models \overline{\varphi}
2243: & \Longrightarrow &
2244: \forall A, B \cdot \semi{\cal P}{A, B}, b_0 \models \overline{\varphi}\\
2245: \iff &&& \pstep{definition of $\models$}\\
2246: & \forall t \in \ext{b_0}^* \cdot \pfsem{\cal P}{A^*,
2247: B^*}, t \models \overline{\varphi}
2248: & \Longrightarrow &
2249: \forall A, B \cdot \forall s \in \ext{b_0} \cdot \semi{\cal P}{A,
2250: B}, s \models \overline{\varphi}.\\
2251: \end{array}
2252: \]
2253: So assuming the left-hand side, take any finite non-empty subsets
2254: $A$ and $B$ of $A^*$ and $B^*$ respectively, and any state
2255: $s \in \ext{b_0}$.
2256:
2257: By Proposition \ref{prop:simulation}, there exists a total simulation of
2258: $\semi{\cal P}{A, B}$ by $\pfsem{\cal P}{A^*, B^*}$, so there must
2259: exist a state $t \in \ext{b_0}^*$ such that $t$ simulates $s$. By
2260: \cite{GL94}\footnote{For any $\overline{L^\mu_2}$ formula
2261: $\overline{\varphi}$, if $t$ simulates $s$ then $M, t \models
2262: \overline{\varphi}$ implies $M, s \models \overline{\varphi}$.},
2263: we can conclude the right-hand side.
2264:
2265: The forward direction of Part 2 follows from the first result
2266: because $\overline{L^\mu_4} \subseteq \overline{L^\mu_2}$. For the
2267: reverse direction, notice, for $\varphi \in L^\mu_4$ the dual formula
2268: of $\overline{\varphi} \in \overline{L^\mu_4}$:
2269: \[
2270: \begin{array}{rrcl}
2271: &
2272: \pfsem{\cal P}{A^*, B^*}, b_0 \models \overline{\varphi} &
2273: \Longleftarrow &
2274: \forall A, B \cdot \semi{\cal P}{A, B}, b_0 \models \overline{\varphi}\\
2275: \iff &&& \pstep{definition of $\models$}\\
2276: &
2277: \forall t \in \ext{b_0}^* \cdot \pfsem{\cal P}{A^*,
2278: B^*}, t \models \overline{\varphi} &
2279: \Longleftarrow &
2280: \forall A, B \cdot \forall s \in \ext{b_0} \cdot \semi{\cal P}{A,
2281: B}, s \models \overline{\varphi}\\
2282: \iff &&& \pstep{definition of $\overline{L^\mu_i}$}\\
2283: &
2284: \forall t \in \ext{b_0}^* \cdot \pfsem{\cal P}{A^*,
2285: B^*}, t \not \models \varphi &
2286: \Longleftarrow &
2287: \forall A, B \cdot \forall s \in \ext{b_0} \cdot \semi{\cal P}{A,
2288: B}, s \not \models \varphi\\
2289: \iff &&& \pstep{contrapositive}\\
2290: &
2291: \exists t \in \ext{b_0}^* \cdot \pfsem{\cal P}{A^*,
2292: B^*}, t \models \varphi &
2293: \Longrightarrow &
2294: \exists A, B \cdot \exists s \in \ext{b_0} \cdot \semi{\cal P}{A,
2295: B}, s \models \varphi.
2296: \end{array}
2297: \]
2298: We will prove this equivalent statement instead.
2299:
2300: Suppose there exists a state $t \in \ext{b_0}^*$ such that
2301: $\pfsem{\cal P}{A^*, B^*}, t \models \varphi$. Using Proposition
2302: \ref{prop:l4}, it can be seen that $\varphi$ is semantically
2303: equivalent to a formula $\psi$, which is the infinite
2304: disjunction of formulas in the form $( \existsnext )^i \, b$.
2305:
2306: As $\pfsem{\cal P}{A^*, B^*}, t \models \varphi$ by
2307: assumption, it must satisfy at least one of the disjuncts of $\psi$
2308: in the form $( \existsnext )^i b$. That means there is a trace
2309: $\pi$ of $\pfsem{\cal P}{A^*, B^*}$ such that $\pi(1) =
2310: \ext{b_0}$ and $\pi(i) = \ext{b}$.
2311:
2312: By Proposition \ref{prop:traces}, $\pi$ is also a trace of
2313: $\semi{\cal P}{A, B}$ for some finite non-empty subsets $A$ and $B$
2314: of $A^*$ and $B^*$ respectively. Therefore, there exists
2315: some $s \in \ext{b_0}$ such that $\semi{\cal P}{A, B}, s \models (
2316: \existsnext )^i b$, and hence $\semi{\cal P}{A, B}, s \models
2317: \varphi$.
2318: \end{proof}
2319:
2320: \begin{example}
2321: \label{ex:singleCacheFinite}
2322: We now show how to check that the program in Example
2323: \ref{ex:singleCache} satisfies its specification for all finite
2324: non-empty sets $A$ and $B$ as instances of \code{ADDR} and
2325: \code{DATA}, carrying on directly from Example
2326: \ref{ex:singleCacheInfinite}.
2327:
2328: We have shown already how to solve $\pfsem{\cal P}{A^*,
2329: B^*}, b_0 \models \varphi$, where $\varphi$ is $\forallnext
2330: (\overline{b_E} \wedge h)$, for any infinite sets $A^*$ and
2331: $B^*$. Because $\varphi$ is an $\overline{L^\mu_4}$ formula,
2332: Theorem \ref{thm:finite} further shows us that this answer is
2333: equivalent to the answer of $\semi{\cal P}{A, B}, b_0 \models
2334: \varphi$ for all non-empty finite sets $A$ and $B$. This is the
2335: original specification that we decided the program should satisfy
2336: back in Example \ref{ex:singleCache}.
2337: \end{example}
2338:
2339: \begin{example}
2340: We have checked the running example in this paper using the model
2341: checker Mur$\phi$ \cite{DDH92}, which accepts UNITY-like programs as
2342: input and performs reachability analysis on them.
2343:
2344: We used finite instantiation theorems \cite{LN00} to show that it
2345: was necessary to check all sizes of \verb$ADDR$ and \verb$DATA$ less
2346: than and equal to 2 and 11 respectively, in order to show that the
2347: program works for any type instantiation. We also declared these
2348: types as ``scalarsets'' \cite{ID96}, so that Mur$\phi$ only checks a
2349: representative state from each set of symmetry equivalent states.
2350: The property $\varphi$ is actually a non-reachability property, and
2351: so Mur$\phi$ could be used to check it.
2352:
2353: The tool reported that the state was not reachable. Using the
2354: theorems as explained in Examples \ref{ex:singleCacheInfinite} and
2355: \ref{ex:singleCacheFinite}, this shows that the program in Figure
2356: \ref{fig:singleCache1} does in fact satisfy its specification that a
2357: read from an arbitrary location will always return the value of the
2358: last write to that location, provided there has been one, for all
2359: sizes of memory and for all types of data values.
2360:
2361: % We have model checked the running example in this paper using the
2362: % CSP \cite{Ros98} refinement checker FDR \cite{FDR}. We implemented
2363: % the code in Figure \ref{ex:singleCacheTransl} using a compiler
2364: % similar to \cite{Ros00} that takes UNITY-like programs and allows
2365: % them to be accepted as input to FDR.
2366:
2367: % FDR does not currently exploit data independence during checks. It
2368: % was therefore necessary to use finite instantiation theorems
2369: % \cite{LN00} to deal with the data types\footnote{In fact the finite
2370: % instances as given by the theorems turned out to be too large for
2371: % FDR, so some heuristics were used to reduce them.}. The property
2372: % $\varphi$ is actually a non-reachability property, and so FDR could
2373: % be used to verify the non-existence of an event corresponding to the
2374: % \verb$ERROR$ state in the program.
2375:
2376: % FDR reported that the state was not reachable. Using the theorems as
2377: % explained in Examples \ref{ex:singleCacheInfinite} and
2378: % \ref{ex:singleCacheFinite}, this shows that the program in Figure
2379: % \ref{fig:singleCache1} does in fact satisfy its specification that a
2380: % read from an arbitrary location will always return the value of the
2381: % last write to that location, provided there has been one, for all
2382: % sizes of memory and for all types of data values.
2383: \end{example}
2384:
2385: \section{Conclusions}
2386:
2387: \label{sect:conclusion}
2388:
2389: In this paper, we have considered the class of programs
2390: data-independent with equality with respect to two distinct type
2391: variables $X$ and $Y$, which may also use arrays indexed by values of
2392: type $X$ and storing values from the type $Y$.
2393:
2394: We have shown that there is a procedure for the parameterised
2395: model-checking problem of the universal fragment of the
2396: $\mu$-calculus, such that it always terminates, but may give false
2397: negatives. We have also shown that the parameterised model-checking
2398: problem of the universal disjunction-free fragment of the
2399: $\mu$-calculus is decidable.
2400:
2401: These results were obtained using, as an abstraction, programs with
2402: any infinite instances of $X$ and $Y$ where arrays are modelled by
2403: partial functions: it was shown that the $\mu$-calculus model-checking
2404: problem is decidable for the resulting transition systems. A method
2405: for doing this was presented, which uses a translation to
2406: bisimulation-equivalent data-independent programs without arrays for
2407: which the $\mu$-calculus model-checking problem is already known to be
2408: decidable.
2409:
2410: This procedure was demonstrated on a fault-tolerant interface over a
2411: set of unreliable memories. It was shown how one could check whether
2412: the system satisfies the property that a read at an address always
2413: returns the value of the last write to that address until a particular
2414: number of faults occur, independently of the size of the memory and of
2415: the type of storable data values.
2416:
2417: We have extended the result in \cite{HIB97} by allowing many arrays
2418: instead of just one, and also by strengthening the model checking
2419: decidability result from linear-time temporal logic to the
2420: $\mu$-calculus. We have clarified a technique used in \cite{McM99} by
2421: developing decidability results for a subclass of the programs
2422: considered there.
2423:
2424: Related work \cite{RL01} includes the addition of a reset operation
2425: which sets every element of an array to a particular value. There, it
2426: is shown that adding reset to the language used in this paper makes
2427: even reachability undecidable for programs with at least two arrays.
2428: However, useful decidability results for reachability are obtained in
2429: the case where the content type of the array is finite and fixed.
2430:
2431: Work in progress and future work include investigating the effect on
2432: these results of adding more array operations to the programs, for
2433: example array assignment, as well as generalising the language to have
2434: many types and multi-dimensional arrays. Another direction for
2435: further work is investigating the applicability of this work to model
2436: checking memory systems such as single processor caches \cite{PH94}
2437: and cache-coherence protocols \cite{Qad01}, as well as parameterised
2438: networks \cite{CR00}.
2439:
2440: %\small
2441:
2442: \bibliography{tom}
2443:
2444: \end{document}
2445: