A theory of normed simulations.
In existing simulation proof techniques, a single step in a lower-level specification may be simulated by an extended execution fragment in a higher-level one. As a result, it is cumbersome to mechanize these techniques using general-purpose theorem provers. Moreover, it is undecidable whether a given relation is a simulation, even if tautology checking is decidable for the underlying specification logic. This article studies various types of <i>normed simulations</i>. In a normed simulation, each step in a lower-level specification can be simulated by at most one step in the higher-level one, for any related pair of states. In earlier work we demonstrated that normed simulations are quite useful as a vehicle for the formalization of refinement proofs via theorem provers. Here we show that normed simulations also have pleasant theoretical properties: (1) under some reasonable assumptions, it is decidable whether a given relation is a normed forward simulation, provided tautology checking is decidable for the underlying logic; (2) at the semantic level, normed forward and backward simulations together form a complete proof method for establishing behavior inclusion, provided that the higher-level specification has finite invisible nondeterminism.
Introduction
Simulation relations and renement functions are widely used to prove that a lower-level specica-
tion of a reactive system correctly implements a higher-level one; see [AL91, LV95, Lyn96, RE98]
for overviews and numerous references to applications. Technically, a simulation (or renement)
is a relation (or function) R between the states of a lower-level specication A and a higher-level
specication B, that satises a condition like
(If lower-level state s and higher-level state u are related, and in A there is a transition from s to
t, then there is a matching transition in B from u to a state v that relates to t; see also Figure 1.)
The existence of a simulation implies that any behavior of A can also be exhibited by B.
a
a

Figure

1: Transfer condition (1).
The main reason why simulations are useful is that they reduce global reasoning about behaviors
and executions to local reasoning about states and transitions. However, to the best of our
knowledge, all complete simulation proof methods that appear in the literature fall back on some
form of global reasoning in the case of specications containing internal (or stuttering) transitions.
The usual transfer condition for forward simulations [LV95], for instance, says
(Each lower-level transition can be simulated by a sequence of higher-level transitions which, apart
from the action that has to be matched, may also contain an arbitrary number of internal \"
transitions; see also Figure 2.) Thus the research program to reduce global reasoning to local
reasoning has not been carried out to its completion. In manual proofs of simulation relations,
a
a
a

Figure

2: Transfer condition (2).
this is usually not a problem: in practice lower-level transitions are typically matched by at most
one higher-level transition; moreover humans tend to be quite good in reasoning about sequences,
and move eortlessly from transitions to executions and back. In contrast, it turns out to be
rather cumbersome to formalize arguments involving sequences using existing theorem provers (see
[DGM97] for a comparative study). In fact, in several papers in which formalizations of simulation
proofs are described, the authors only consider a restricted type of simulation in which each
lower-level transition is matched by at most one higher-level transition [HSV94, NS95, DGRV00].
However, there are many examples of situations where these restricted types of simulations cannot
be applied. In approaches, such as [SAGG + 93], where the full transfer condition (2) is formalized,
the user has to supply the simulating execution fragments  to the prover explicitly, which makes
the verication process highly interactive.
In this paper, we introduce a simulation proof method which remedies the above problems.
The idea is to dene a function n that assigns a norm n(s a ! t; u), in some well-founded domain,
to each pair of a transition in A and a state of B. If u has to simulate transition s a ! t then it
may either do nothing (if a is internal and t is related to u), or it may do a matching a-transition,
or it may perform an internal transition such that the norm decreases, i.e.,
We establish that normed forward simulations and normed backward simulations together constitute
a complete proof method for establishing trace inclusion. In addition we show how history
and prophecy relations (which are closely related to the history and prophecy variables of [AL91])
can be enriched with a norm function, to obtain another complete proof method in combination
with a simple notion of renement mapping.
The preorders generated by normed forward simulations are strictly ner than the preorders
induced by the forward simulations of [LV95]. In fact, we will characterize normed forward simulations
in terms of branching forward simulations [GW96], and present a similar characterization
for the backward case. It is possible to come up with a variant of normed forward simulation that
induces the same preorder as forward simulations, but technically this is somewhat more involved
(see [Gri00][Section 6.5.10]).
When proving invariance properties of programs, one is faced with two problems. The rst
problem is related to the necessity of proving tautologies of the assertion logic, whereas the second
manifests in the need of nding suciently strong invariants. In order to address the rst problem,
powerful decision procedures have been incorporated in theorem provers such as PVS [ORSH95].
If tautology checking is decidable then it is decidable whether a given state predicate is valid for
the initial states and preserved by all transitions. The task of nding such a predicate, i.e. solving
the second problem, is the responsibility of the user, even though some very powerful heuristics
have been devised to automate this search [BLS96, MBSU98]. Analogously, if specications A and
B, a conjectured forward simulation relation R and norm function n can all be expressed within a
decidable assertion logic, and if the specication of B only contains a nite number of deterministic
transition predicates, then it is decidable whether the pair (R; n) is a normed forward simulation.
This result, which does not hold for earlier approaches such as [LV95], is a distinct advantage of
normed forward simulations.
The idea of using norm functions to prove simulation relations also occurs in [GS95], where it
is used to prove branching bisimilarity in the context of the process algebra CRL. However, in
[GS95] the norm function is dened on the states of B only and does not involve the transitions of
A. As a consequence, the method of [GS95] does not always apply to diverging processes. Norm
functions very similar to ours were also studied by Namjoshi [Nam97]. He uses them to obtain a
characterization of the stuttering bisimulation of [BCG88], which is the equivalent of branching
bisimulation in a setting where states rather than actions are labeled (see [DNV95]). Both [GS95]
and [Nam97] do not address eectiveness issues. Although we present normed simulations in a
setting of labeled transition systems, it should not be dicult to transfer our results to a process
algebraic setting such as [GS95] or a state based setting such as [Nam97]. Inspired by our approach,
norm functions have been used in [BS00] to dene a new bisimulation equivalence for probabilistic
systems.
In this paper, we only present maximally simple examples to illustrate the various deni-
tions and results. In [Gri00][Chapter 6], normed simulations have been applied in a substantial
case study, namely the verication of the leader election protocol that is part of the IEEE 1394
\Firewire" standard. This verication has been mechanically checked using PVS. 1
In the presentation of our results, we will closely follow [LV95] and stick to the notations
introduced in that paper. In fact, our aim will be (amongst others) to derive analogous results as in
[LV95], only for dierent types of simulations. However, we decided not to present normed versions
of the forward-backward and backward-forward simulations of [LV95], since these simulations have
thus far not been used in practice and technically this would bring nothing new. Apart from the
notion of a norm function, a major technical innovation in the present paper is a new, simple
denition of execution correspondence [GSSL93, SALL93], and the systematic use of this concept
in the technical development.
Preliminaries
In this section, we brie
y recall some basic concurrency theory denitions, taken from [LV95]. An
automaton (or labeled transition system) A consists of
a (possibly innite) set states(A) of states,
a nonempty set start(A)  states(A) of start states,
a set acts(A) of actions that includes the internal (or stuttering) action  , and
a set steps(A)  states(A)  acts(A)  states(A) of steps.
Write s a
!A t as a shorthand for (s; a; t) 2 steps(A). We let ext(A), the external actions, denote
fg. An execution fragment of A is a nite or innite alternating sequence, s 0 a 1 s 1 a 2 s 2   ,
of states and actions of A, beginning with a state, and if it is nite also ending with a state, such
that for all i > 0, s
a i
An execution of A is an execution fragment that begins with a start
state. We denote by execs  (A) and execs(A) the sets of nite and all executions of A, respectively.
A state s of A is reachable if s occurs as the last state in some nite execution  of A. In this case
we write reachable(A; s). Also, we write reachable(A) for the set of reachable states of A.
The trace of an execution fragment , notation trace(), is the subsequence of non- actions
occurring in . A nite or innite sequence  of external actions is a trace of A if A has an execution
with trace(). Write traces  (A) and traces(A) for the sets of nite and all traces of A,
respectively. Write A  T B if traces  (A)  traces  (B), and A T B if traces(A)  traces(B).
Suppose A is an automaton, s and t are states of A, and  is a nite sequence over ext(A).
We say that is a move of A, and write s
=)A t, or just s
when A is clear, if A has a
nite execution fragment  that starts in s, has trace  and ends in t.
Three restricted kinds of automata play an important role in this paper:
1. A is deterministic if for any state s and any nite sequence  over ext(A),
there is at most one state t such that s
t. A deterministic automaton is characterized
uniquely by the properties that every -step is of the form (s; ; s) for some
s, and for each state s and each action a there is at most one state t such that s a
t.
2. A has nite invisible nondeterminism (n) if start(A) is nite, and for any state s and any
nite sequence  over ext(A), there are only nitely many states t such that s
t.
3. A is a forest if, for each state s of A, there is exactly one execution that leads to s. A forest
is characterized uniquely by the property that all states of A are reachable, start states have
no incoming steps, and each of the other states has exactly one incoming step.
1 Actually, we discovered the notion of a normed simulation while formalizing the correctness proof of this leader
election protocol.
The relation after (A) consists of the pairs (; s) for which there is a nite execution of A with
trace  and last state s:
(Here last denotes the function that returns the last element of a nite, nonempty sequence.) We
dene past(A) to be the inverse of after(A), past(A)
relates a state s of A
to the traces of nite executions of A that lead to s.
The following elementary lemma from [LV95] states that for the restricted kinds of automata
dened above, the relations after and past satisfy certain nice properties.
Lemma 2.1
1. If A is deterministic then after (A) is a function from traces  (A) to states(A).
2. If A has n then after (A) is image-nite, i.e., each trace in the domain of after(A) is only
related to nitely many states.
3. If A is a forest then past(A) is a function from states(A) to traces  (A).
3 Step Renements and Execution Correspondence
In this section, we present step renements, the simplest notion of simulation that we consider in
this paper. In order to prove soundness of step renements, we also introduce the auxiliary notion
of execution correspondence. This notion plays a key role in this paper; the technical lemmas that
we prove in this section will also be used repeatedly in subsequent sections.
3.1 Step Renements
Let A and B be automata. A step renement from A to B is a partial function r from states(A)
to states(B) that satises the following two conditions:
1. If s 2 start(A) then s 2 domain(r) and r(s) 2 start(B ).
2. If s a
(a)
(b) r(s) a
!B r(t).
Note that, by a trivial inductive argument, the set of states for which r is dened contains all the
reachable states of A (and is thus an invariant of this automaton). We write A R B if there
exists a step renement from A to B.
As far as we know, the notion of step renements was rst proposed in [NS95]. However, if
we insist on the presence of stuttering steps s  ! s for each state s (a common assumption in
models of reactive systems) then clause (2a) in the above denition becomes super
uous and the
notion of a step renement reduces to that of a homomorphism between reachable subautomata
[Gin68]. Step renements are slightly more restrictive than the possibility mappings from [LT87]
(called weak renements in [LV95]). In the case of a possibility mapping each (reachable) step of
A may be matched by a sequence of steps in B with the same trace. This means that in the above
denition condition (2) is replaced by:
2. If s a
has an execution fragment  with
a b
a
u2

Figure

3: A step renement.
Observe that, unlike step renements, possibility mappings do not reduce global reasoning to local
reasoning.
Example 3.1 Figure 3 illustrates the notion of a step renement. Note that the -steps in A are
not matched by any step in B. Also the c-step in A is not matched by any step in B: both source
and target states of this step are outside the domain of the step renement. This is allowed since
both states are unreachable. Observe that there is no step renement from B to A, but that there
exists a possibility mapping from B to A.

Figure

4 gives another example. In this case there is a step renement from A 0 to B 0 but not
from B 0 to A 0 . There is not even a possibility mapping from B 0 to A 0 .
a
a
a
a

Figure

4: Another step renement.
The following proposition states a basic sanity property of step renements.
Proposition 3.2 R is a preorder (i.e., is transitive and re
exive).
Proof: The identity function from states(A) to itself trivially is a step renement from A to itself.
Hence R is re
exive. Transitivity follows from the observation that if r is a step renement from
A to B and r 0 is a step renement from B to C, then the function composition r 0  r is a step
renement from A to C.
3.2 Execution Correspondence
If there exists a step renement from A to B then we can construct, for each execution fragment
of A, a corresponding execution fragment of B with the same trace. The notion of 'corresponding'
is formalized below.
Suppose A and B are automata, R  states(A)  states(B ), and
are execution fragments of A and B, respectively. Let index () and index ( 0 )
denote the index sets of  and  0 . Then  and  0 correspond via R and are R-related, notation
there exists an index relation over R, i.e., a relation I  index ()  index ( 0 ) such
that (1) if two indices are related by I then the corresponding states are related by R; (2) I is
monotone; (3) each index of  is related to an index of  0 and vice versa; (4) sides of \squares"
always have the same label and sides of \triangles" are labeled with  . Formally we require, for
1. (i;
2. (i;
3. I and I 1 are total
4. (i; I ) a
We write (A; B) 2 R if for every execution  of A there is an execution  0 of B such that
if for every nite execution  of A there is a nite execution  0 of B
with

Figure

5 illustrates the correspondence between two executions of automata A
and B from Figure 3.
u0 u2 u2 u2 u2

Figure

5: Execution correspondence.
Another notion of correspondence has been presented in [GSSL93, SALL93] and formalized
in [Mue98]. Within the theory of I/O automata, execution correspondence plays a crucial role
in proofs of preservation of both safety and liveness properties. Our notion is more restrictive
than the one of [GSSL93, SALL93], but technically simpler. Moreover it has the advantage that
it preserves until properties. In this paper, we only study safety properties and it suces to know
that corresponding executions have the same trace. The latter fact is established in the next
lemma.
Lemma 3.3 (Corresponding execution fragments have the same trace)
1. Suppose I is an index relation as above and (i;
2. If (;
Proof: For (1), suppose (i; I . By induction on
trace(s
are 0. Clearly, trace(s 0
For the induction step, suppose For reasons of symmetry we may assume w.l.o.g.
that i > 0. Let j 0 be the largest index with j 0  j and (i
can only be related to indices less than or equal to j, and by totality there is at least one such an
index.) We distinguish between three cases:
1. j. Then by condition (4b), a By induction hypothesis,
trace(s
Hence trace(s 0 a
2. 1. Then by condition (4a), a . By induction hypothesis,
trace(s
Hence trace(s 0 a
3. j 0 < j 1. Then by conditions (2) and (3), (i; j 1) 2 I . By condition (4c), this implies
. By induction hypothesis,
trace(s
Hence trace(s 0 a
This completes the proof of the induction step.
For (2), suppose that (;  0 there exists an index relation I that relates  and  0 .
Using (1) and the fact that both I and I 1 are total, it follows that each nite prex of trace()
is also a nite prex of trace( 0 ), and vice versa. This implies
The next corollary will be used repeatedly in the rest of this paper. It states that in order
to prove trace inclusion between automata A and B it suces to nd for each execution of A a
corresponding execution of B. Depending on whether one wants to prove inclusion of all traces or
of nite traces only, a stronger resp. weaker type of execution correspondence is required.
Corollary 3.4 (Execution correspondence implies trace inclusion)
1. If (A; B) 2 R then [A; B] 2 R.
2. If [A; B] 2 R then A  T B.
3. If (A; B) 2 R then A T B.
Proof: Statement (1) follows from the denitions. Statements (2) and (3) follow immediately
from Lemma 3.3 and the denitions.
3.3 Soundness and Partial Completeness
The next theorem states that if there is a step renement from A to B, it is possible to construct,
for each execution of A, a corresponding execution of B. Using Corollary 3.4, this implies that
step renements constitute a sound technique for proving trace inclusion. In addition, the next
theorem also allows us to use step renements as a sound technique for proving implementation
relations between live automata, as in [GSSL93, SALL93, Mue98].
Theorem 3.5 (Soundness of step renements)
If r is a step renement from A to B then (A; B) 2 r.
Suppose r is a step renement from A to B. Let  be an execution of A.
Inductively, we dene an execution  and an index relation I such that  and
0 are r-related via I .
To start with, dene u declare (0; 0) to be an element of I .
Now suppose (i; I and i is a nonnal index of . We distinguish between two cases:
1. If r(s i ) a i+1
to be
an element of I ;
2. otherwise, declare (i to be an element of I .
By construction, using the dening properties of a step renement, it follows that I is an index
relation. This implies (A; B) 2 r.
Step renements alone do not provide a complete method for proving trace inclusion. There
is a partial completeness result, however.
Theorem 3.6 (Partial completeness of step renements)
Suppose A is a forest, B is deterministic and A  T B. Then A R B.
Proof: The relation r
is a step renement from A to B.
Actually, we can even slightly strengthen the above theorem. It suces to assume that A
restricted to its reachable states is a forest, and that B restricted to its reachable states is deter-
ministic. In Figure 3, automaton A restricted to its reachable states is a forest and automaton
B is deterministic. As we observed already, there is a step renement from A to B. Even if we
restrict to reachable states, automaton B is not a forest and automaton A is not deterministic.
As we observed, there is no step renement from B to A.
In practice, the preconditions of Theorem 3.6 are seldom met. The higher-level specication
often is deterministic, but it rarely occurs that the lower-level specication is a forest. Nevertheless,
step renements have been used in several substantial case studies, see for instance [HSV94, NS95,
DGRV00].
4 Normed Forward Simulations
Even though there exists no step renement from automaton B 0 to automaton A 0 in Figure 4, these
automata do have the same traces. By moving from functions to relations it becomes possible to
prove that each trace of B 0 is also a trace of A 0 . This idea is formalized in the following denition.
A normed forward simulation from A to B consists of a relation f  states(A) states(B) and
a function n : steps(A)  states(B) ! S, for some well-founded set S, such that (here f [s] denotes
the set fu j (s; u) 2 fg):
1. If s 2 start(A) then f [s] \ start(B) 6= ;.
2. If s a
(a)
!B v, or
(c)
Write A F B if there exists a normed forward simulation from A to B.
The intuition behind this denition is that if s a
!A t and (s; u) 2 f , then either (a) the
transition in A is a stuttering step that does not have to be matched, or (b) there is a matching
step in B, or (c) B can do a stuttering step which decreases the norm. Since the norm decreases at
each application of clause (c), this clause can only be applied a nite number of times. In general,
the norm function may depend both on the transitions in A and on the states of B. However,
if B is convergent, i.e., there are no innite -paths, then one can simplify the type of the norm
function (though not necessarily the denition of the norm function itself) to
In fact, in the approach of [GS95], which not always applies to divergent processes, the norm
function is required to be of this restricted type.
Example 4.1 In Figure 4, the relation indicated by the dashed lines, together with an arbitrary
norm function, is a normed forward simulation from B 0 to A 0 .
Consider automata A and B in Figure 3. Let n be the function that assigns norm 1 to state
s0 and norm 0 to all other states of A. Then n together with the relation indicated by the dashed
lines constitutes a normed forward simulation from B to A.
u2 u3
a
a

Figure

must take steps of C into account.
Now consider the automata C and D in Figure 6. Let m be a norm function satisfying
together with the relation indicated by the dashed lines constitutes a normed forward
simulation from C to D. It is not hard to see that in this example, where D is not convergent,
the norm necessarily depends on the selected step in C.
The next proposition asserts that normed forward simulations indeed generalize step rene-
ments.
Proposition 4.2 A R B
Proof: Together with an arbitrary norm function, any step renement (viewed as a relation) is
a normed forward simulation.
The soundness of normed forward simulations is trivially implied by the following lemma and
Corollary 3.4.
Lemma 4.3 Suppose (f; n) is a normed forward simulation from A to B, A has an execution
fragment  with rst state s, and u is a state of B with u 2 f [s]. Then B has an execution
fragment  0 that starts in u such that (;  0
be a function such that c(s a ! t;
1. If
2. If
v.
3. If x
The existence of c, which chooses between a left move (L) of A, a common move (C) of A and B,
or a right move (R) of B, is guaranteed by the fact that (f; n) is a normed forward simulation.
Inductively, we dene a sequence
4-tuples in N  N  acts(B)  states(B ). The rst element in the sequence is z
is an element of the sequence, and i is a nonnal index of , then we dene z k+1
as follows
1. If c(s i
a
2. If c(s i
a
3. If c(s i
a
Suppose that both (i; j; b; u) and (i occur in sequence . We claim that
To see why this is true assume w.l.o.g. that (i; j; b; u) occurs before (i Now observe that
the values of both the rst and second component of elements in  increase monotonically. This
means that each successor of (i; j; b; u) up to and including (i been obtained from its
predecessor by applying rule (1). This implies that the the second resp. third components of all
elements in the sequence from (i; j; b; u) until (i
Using this property, we can dene for each element (i; j; b; u) in , b
occurs in g. By construction of , using
the properties of c, it follows that  0 is an execution fragment of B that starts in u, and that I is
an index relation over f . This implies (;  0
Theorem 4.4 (Soundness of normed forward simulations)
If f is a normed forward simulation from A to B then (A; B) 2 f .
Proof: Immediate from the denitions and Lemma 4.3.
Example 4.5 Consider automata C and E in Figure 7. There does not exist a normed forward
a t
a
u2
u3

Figure

7: Dierence between forward simulations and normed forward simulations.
simulation from C to E. Such a simulation would have to relate states s0 and u0. But in order
for E to simulate the step s0 b
would also have to relates states s0 and u2. But this is
impossible since from state u2 there is no way to simulate the step s0 a ! s1.
It turns out that there does exist a forward simulation in the sense of [LV95] from C to E. In
the case of a forward simulation, a step of A may be matched by a sequence of steps in B with
the same trace. This means that in the denition of a normed forward simulation condition (2) is
replaced by:
2. If s a
has an execution fragment  with
trace(a) and last() 2 f [t].
The dashed lines in Figure 7 indicate a forward simulation from C to E.
The automata A and B in Figure 3 provide us with a similar example: there exists a forward
simulation from B to A, but no normed forward simulation.
The dierence between forward simulations and normed forward simulations is very similar to
the dierence between Milner's observation equivalence [Mil89] and the branching bisimulation of
Glabbeek and Weijland [GW96]. In fact, we can characterize normed forward simulations in
terms of \branching forward simulations", a notion that is inspired by the branching bisimulations
of [GW96]. A similar characterization has been obtained by Namjoshi [Nam97] in the setting of
stuttering bisimulations.
Formally, a branching forward simulation from A to B is a relation f  states(A)  states(B)
such that
1. If s 2 start(A) then f [s] \ start(B) 6= ;.
2. If s a
!A t and u 2 f [s] then B has an execution fragment that starts in u and that is
f-related to s a ! t.
The following theorem implies that there exists a normed forward simulation between two
automata if and only if there is a branching forward simulation between them.
Theorem 4.6
1. Suppose (f; n) is a normed forward simulation from A to B. Then f is a branching forward
simulation from A to B.
2. Suppose f is a branching forward simulation from A to B. Let n(s a ! t; u) be 0 if u 62 f [s]
and otherwise be equal to the length of the shortest execution fragment that starts in u and
that is f-related to s a ! t. Then (f; n) is a normed forward simulation from A to B.
Proof: Part (1) follows by Lemma 4.3. The proof of part (2) is routine.
An interesting corollary of Theorem 4.6 is that if there exists a normed forward simulation
between two automata, there is in fact a normed forward simulation with a norm that has the
natural numbers as its range.
The proof that branching bisimilarity is an equivalence is known to be tricky [Bas96]. Likewise,
the proof that branching forward simulations induce a preorder is nontrivial. We rst need to dene
the auxiliary concept of a reduced index relation and to prove a lemma about it.
Suppose that  and  0 are R-related via index relation I . We say that I is reduced if the
following two conditions are satised:
1. If  is nite then I relates the nal index of  only to the nal index of  0 .
2. I is N-free: (i; I .
Observe that if  is nite and I is reduced, then  0 is also nite. The following technical lemma
states that index relations can always be reduced.
Lemma 4.7 Suppose that  and  0 are R-related via index relation I. Then  0 has a prex  00
that is R-related to  via a reduced index relation J  I.
Proof: If  is innite then let  If  is nite then let  00 be the nite prex of  0 up to
and including the rst state whose index is related by I to the nal index of .
Inductively we dene a sequence of pairs in N  N. The rst element of the
sequence is z is an element of the sequence and i is a nonnal index then
we dene z k+1 as follows:
1. (i
2. (i
3.
Note that since I is an index relation, z k+1 is properly dened. Let occurs in g.
It is routine to check that J  I , that  and  00 are R-related via J , and that J is reduced. A
point is the totality of J and J 1 . We prove that J is total by contradiction. Suppose that
J is not total. Let i be the smallest index of  with J be the smallest index of  0
with (i; (j exists since index relation I is total). Let l be the maximal index of  0 with
(i (there is a maximal index since (i I , which implies
l  j by monotonicity of index relation I). Let z
Hence (i . But this contradicts the fact that l be the maximal index of  0 with
(i
In a similar way also the totality of J 1 and N-freeness can be proved by contradiction.
We are now prepared to prove that branching forward simulations (and hence also normed
forward simulations) induce a preorder.
Proposition 4.8 F is a preorder.
Proof: For re
exivity, observe that the identity function from states(A) to itself is a branching
forward simulation from A to itself.
For transitivity, suppose f and g are branching forward simulations from A to B and from B
to C, respectively. We claim that g f is a branching forward simulation from A to C. It is trivial
to check that g  f satises condition (1) in the denition of a branching forward simulation. For
condition (2), suppose that s a
there exists a state w of B such that
Hence there is an execution fragment  starting in w such that s a ! t and
are f-related via some index relation I . By Lemma 4.7, we may assume that I is reduced. Also,
there is an execution fragment  0 starting in u such that  and  0 are g-related via some index
relation J . Again by Lemma 4.7, we may assume that J is reduced. Using the fact that both I
and J are reduced, it is routine to check that s a ! t and  0 are g  f-related via index relation
J  I . Thus g  f satises condition (2) in the denition of a branching forward simulation.
Variants of the partial completeness result below appear in several papers, see for instance
[Jon87, LV95]. Since higher-level specications are often deterministic, this result explains why in
practice (normed) forward simulations can so often be used to prove behavior inclusion.
Theorem 4.9 (Partial completeness of normed/branching forward simulations)
If B is deterministic and A  T B then A F B.
Proof: The relation f
is a branching forward simulation from A to B.
It is interesting to note that there is one result from [LV95] concerning forward simulations that
does not carry over to the normed/branching simulations of this paper. This result, Proposition
3.12, states that if A is a forest and A F B then A R B. The automata C and D of Figure 6
constitute a counterexample. Actually, the same Proposition 3.12 also does not carry over to the
setting of timed automata studied in [LV96].
5 Normed Backward Simulations
As we observed, there exists no normed forward simulation from automaton B to automaton A in

Figure

3, even though both automata have the same traces. Also, there does not exist a normed
forward simulation from automaton C to the trace equivalent automaton E in Figure 7. In both
cases a forward simulation in the sense of [LV95] exists. However, the example in Figure 8 below
shows that also forward simulations do not yet provide us with a complete method for proving
trace inclusion. It is well-known from the literature that completeness can be obtained by adding
some form of backward simulation.
Example 5.1 There exists no (normed/branching) forward simulation from automaton C to
automaton F in Figure 8. The relation indicated by the dashed lines fails since from state u0 the
b-step from s0 can not be simulated, whereas from u2 the a-step from s0 can not be simulated.
a
u2
u3
a b

Figure

8: The need for backward simulations.
In many respects, backward simulations are the dual of forward simulations. Whereas a forward
simulation requires that some state in the image of each start state should be a start state, a
backward simulation essentially requires that all states in the image of a start state be start
states. Also, a forward simulation requires that forward steps in the source automaton can be
simulated from related states in the target automaton, whereas the corresponding condition for a
backward simulations requires that backward steps can be simulated. However, the two notions are
not completely dual: the denition of a backward simulation contains a nonemptiness condition,
and also, in order to obtain soundness for general trace inclusion, backward simulations also require
a nite image condition. The mismatch is due to the asymmetry in our automata between the
future and the past: from any given state, all the possible histories are nite executions, whereas
the possible futures can be innite.
Formally, we dene a normed backward simulation from A to B to be a pair of a total relation
b  states(A)  states(B) and a function
well-founded set S, satisfying
1. If s
(a)
2. If t a
(a)
!B u, or
(c) 9v
there is a normed backward simulation from A to B, and A  iB B if there is a
normed backward simulation from A to B that is image-nite.
Example 5.2 In Figure 8, the relation indicated by the dashed lines is a normed backward
simulation from C to E, for arbitrary norm functions. It is not dicult to construct normed
backward simulations from automaton B to automaton A in Figure 3, and from automaton C to
automaton E in Figure 7.
a
a a a
a a a
u0 u1 u2 u3 u4
G

Figure

normed backward simulation.

Figure

9 illustrates the dierence between B and  iB . Relation states(G)states(H ) together
with an arbitrary norm function constitutes a normed backward simulation from G to H . We claim
that no image-nite normed backward simulation exist. Because suppose that b is such a relation.
Then, for all
This implies that
Since each state si is related to at least one state sj, it follows that state s0 is related to innitely
many states, which is a contradiction.
The following proposition states some trivial connections between the preorders induced by
normed backward simulations and step renements.
Proposition 5.3
1. If all states of A are reachable and A R B then A  iB B.
2. If A  iB B then A B B.
Proof: Trivial.
The next lemma is required to prove soundness of normed backward simulations.
Lemma 5.4 Suppose (b; n) is a normed backward simulation from A to B, A has a nite execution
fragment  with last state s, and u is a state of B with u 2 b[s]. Then B has a nite execution
fragment  0 that ends in u such that (;  0 ) 2 b. Moreover, if  is an execution then  0 can be
chosen to be an execution as well.
Proof: Similar to the proof of Lemma 4.3.
By Lemma 5.4 and Corollary 3.4, the existence of a normed backward simulation implies
inclusion of nite traces. Normed backward simulations, however, are in general not a sound
method for proving inclusion of innite traces. As a counterexample, consider automata G and
H from

Figure

9. There exists a normed backward simulation from G to H , but the innite trace
a ! of G is not a trace of H . As is well-known from the literature, a sound method for proving
inclusion of innite traces can be obtained by requiring image niteness of the simulation relation.
Theorem 5.5 (Soundness of normed backward simulations)
1. If b is a normed backward simulation from A to B then [A; B] 2 b.
2. If moreover b is image-nite then (A; B) 2 b.
Proof: Statement (1) follows immediately by Lemma 5.4 and the totality of b. In order to prove
(2), suppose that b is image-nite. Let  be an execution of A. We have to establish the existence
of an execution  0 of B with (;  0 ) 2 b. If  is nite then this follows by Lemma 5.4 and the
totality of b. So assume that  is innite. We use a minor variation of K}onig's Lemma [Knu97]
that occurs in [LV95]:
Let G be an innite digraph such that (1) G has nitely many roots, i.e., nodes without
incoming edges, (2) each node of G has nite outdegree, and (3) each node of G is
reachable from some root. Then there is an innite path in G starting from some root.
The nodes of the graph G that we consider are pairs
is a nite execution of B
and I is an index relation that relates
to some nite prex of . There is an edge from a node
) to a node (I
is a prex of
0 and I 0 extends I with precisely one element. It is
straightforward to check that G satises the conditions of K}onig's Lemma. Hence G has an innite
path. Let J be the union of all the index relations occurring on nodes in this path, and let  0 be
the limit of the nite executions of the nodes in this path. Observe that, by image-niteness of b,
each index of  occurs in the domain of J . Hence (;  0
The following Proposition 5.6 is in a sense the converse of Proposition 5.3. The proof is similar
to that of the corresponding result in [LV95].
Proposition 5.6
1. If B is deterministic and A B B then A R B.
2. If all states of A are reachable, B has n and A B B, then A  iB B.
Proof: For (1), suppose that B is deterministic and that b is a normed backward simulation
from A to B. Suppose that s is a reachable state of A. We will prove that b[s] contains exactly
one element. Since any normed backward simulation that is functional on the reachable states
trivially induces a step renement, this gives us A R B.
Because b is a normed backward simulation it is a total relation, so we know b[s] contains
at least one element. Suppose that both u
reachable, A has an execution  that ends in s. By Lemma 5.4, B has executions  1 and  2
which end in u 1 and u 2 , respectively, such that (;  1
using the fact the B is
deterministic.
For (2), suppose that all states of A are reachable, B has n, and b is a normed backward
simulation from A to B. Suppose that s is a state of A. Since s is reachable, there is an execution
that ends in s. Let  be trace of . By Lemma 5.4 there exists, for each u 2 b[s], an execution  u
of B that ends in u such that (;  u Hence b[s]  after (B)[].
But since B has n, after (B)[] is nite by Lemma 2.1(2). Hence b is image-nite.
As in the forward case, we will now characterize normed backward simulations in terms of
\branching backward simulations", and use this characterization to establish that B and  iB are
preorders.
A branching backward simulation from A to B is a total relation b  states(A)  states(B)
such that
1. If s 2 start(A) and u 2 b[s] then B has an execution that ends in u and is b-related to s.
2. If t a
!A s and u 2 f [s] then B has an execution fragment that ends in u and is b-related to
Theorem 5.7
1. Suppose (b; n) is a normed backward simulation from A to B. Then b is a branching backward
simulation from A to B.
2. Suppose b is a branching backward simulation from A to B. Let n(s; u) be 0 if s is not a start
state or u 62 b[s] and otherwise be equal to the length of the shortest execution that ends in
u and is b-related to s. Furthermore, let n(t a ! s; u) be 0 if u 62 f [s] and otherwise equal to
the length of the shortest execution fragment ending in u that is b-related to t a
!A s. Then
(b; n) is a normed forward simulation from A to B.
Proof: Statement (1) follows by Lemma 5.4. The proof of statement (2) is routine.
As in the forward case, we see that if there exists a normed backward simulation between
two automata, there is in fact a normed backward simulation with a norm that has the natural
numbers as its range.
Proposition 5.8 B and  iB are preorders.
Proof: Similar to the proof of Proposition 4.8.
The following partial completeness result is a variation of results of [Jon90, LV95].
Theorem 5.9 (Partial completeness of normed backward simulations)
If A is a forest and A  T B then A B B.
Proof: The relation b
after (B)  past(A) is a branching backward simulation from A to B.
Note that by Proposition 5.6 we can strengthen the conclusion of Theorem 5.9 to A  iB B in
case B has nite invisible nondeterminism.
Example 5.10 Consider the automata A 0 and B 0 in Figure 4. There exists no normed backward
simulation from B 0 to A 0 . The relation indicated by the dashed lines fails since the backward
transition from state u0 cannot be simulated from the related state s0. By consequence, also
normed backward simulations do not provide a complete proof method for establishing trace
inclusion. In the next section, we will see that completeness can be obtained by combining normed
forward and backward simulations.
6 Normed History Relations
In this section we dene normed history relations. These provide an abstract view of the history
variables of Abadi and Lamport [AL91], which in turn are abstractions of the auxiliary variables
of Owicki and Gries [OG76].
A pair (r; n) is a normed history relation from A to B if r is a step renement from B to A,
and (r 1 ; n) is a normed forward simulation from A to B. Write A H B if there exists a normed
history relation from A to B.
A. Through these implications, the preorder
and soundness results for normed forward simulations and step renements carry over to normed
history relations. In fact, if (r; n) is a normed history relation from A to B then r is just a functional
branching bisimulation from B to A in the sense of Van Glabbeek and Weijland [GW96]. Hence,
history relations preserve behavior of automata in a very strong sense. Intuitively, there is a
history relation from A to B if B can be obtained from A by adding an extra state variable that
records information about the history of an execution.
Example 6.1 Consider again the automata A 0 and B 0 in Figure 4. Together with an arbitrary
norm function, the dashed lines constitute a normed history relation from B 0 to A 0 . Because, as
we observed, there is no step renement from B 0 to A 0 , there exists no normed history relation
from A 0 to B 0 .
An important example of a history relation is provided by the \unfolding" construction. The
unfolding of an automaton A, notation unfold(A), is the automaton obtained from A by recording
the complete history of an execution. Formally, unfold(A) is the automaton B dened by
the set of executions of A that consist of a single start state,
for
The next proposition relates an automaton to its unfolding.
Proposition 6.2 unfold(A) is a forest and A H unfold(A).
Proof: Clearly, unfold(A) is a forest. The function last which maps each nite execution of A
to its last state is a step renement from unfold(A) to A, and the relation last 1 , together with
an arbitrary norm function, is a normed forward simulation from A to unfold(A).
The following completeness theorem, a variation of a result due to Sistla [Sis91], asserts that
normed history relations together with normed backward simulations constitute a complete proof
method for establishing trace inclusion. By consequence, also normed forward simulations together
with normed backward simulations constitute a complete proof method.
Theorem 6.3 (Completeness of normed history relations and normed backward simulations)
If A  T B then there exists an automaton C such that A H C B B.
Proof: Take unfold(A). By Proposition 6.2, C is a forest and A H C. Since A  T B,
also C  T B by soundness of history relations. Next apply the partial completeness result for
backward simulations (Theorem 5.9) to conclude C B B.
Observe that if we can assume in addition that B has n, we may replace B by  iB in the
conclusion using Proposition 5.6.
Normed forward simulations are equivalent to normed history variables combined with step
renements: whenever there is a normed forward simulation from A to B, we can nd an intermediate
automaton C such that there is a normed history relation from A to C and a step renement
from C to B. The converse implication trivially holds since normed history relations and step
renements are special cases of normed forward simulations. In order to prove the existence of
automaton C, we need to dene a notion of \superposition" of automata and to prove a technical
lemma.
Let R  states(A)  states(B) be a relation with R \ (start(A)  start(B)) 6= ;. The superposition
of A and B via R is the automaton C dened by
for (s; u); (t; v) 2 states(C ) and a 2 acts(C ), (s; u) a
_ s a
Essentially, the superposition is just the usual parallel composition of A and B with
the set of states restricted to R.
Lemma 6.4 Suppose (f; n) is a normed forward simulation from A to B. Let
and let  1 and  2 be the projection functions that map states of C to their rst and second
components, respectively. Let n 0 be the norm function given by n 0 (;
history relation from A to C, and  2 is a step renement from C to B.
Proof: Straightforward from the denitions.
Theorem 6.5 A F B ,
Proof: Implication \)" follows by Lemma 6.4. For implication \(", suppose A H C R B.
Then A F C by the denition of history relations, and C F B because any step renement is a
normed forward simulation. Now A F B follows by the fact that F is a preorder.
In [AK96][Intermezzo 3.23], Klop and Ariola state a remarkable result: on a domain of of
nitely branching process graphs (i.e., automata considered modulo isomorphism) the preorder
induced by functional bisimulations (i.e., history relations) is in fact a partial order: A H B
B. The authors also present a counterexample to show that the nite
branching property is needed to prove this result. Below we present a slight generalization of the
result of [AK96] in the setting of our paper. It turns out to be sucient to assume that automata
have nite invisible nondeterminism (n).
Theorem 6.6 Suppose A and B have n, A. Then the reachable subautomata
of A and B are isomorphic.
Proof: Suppose that (f; n) is a normed history relation from A to B, and (g; m) is a normed
history relation from B to A. Because A and B have n, both start(A) and start(B) are nite.
Since f is a step renement, it maps start states of B to start states of A. Using that f 1 is a
forward simulation, we infer that f is surjective on start states. Hence j start(B) j  j start(A) j.
By a similar argument, using that (g; m) is a normed history relation from B to A, we obtain
j. This means that f is also injective on start states.
Let  be an arbitrary trace of A and B. Using a similar argument as above, we infer
Since, by Lemma 2.1(2), both after (A)[] and after (B)[] are nite, it follows that
This means that f and g are injective on the sets after(B)[] and after (A)[], respectively. But
since each reachable state is in a set after (B)[] or after(A)[], for some , it follows that f and
are injective on all states. Now the required isomorphism property follows from the fact that f
and g are step renements.
Intuitively, one may interpret the above result as follows: if A H B then B contains more
history information than A. If B contains more history information than A, and A contains more
history information than B, then they are equal.
7 Normed Prophecy Relations
In this section, we will dene normed prophecy relations and show that they correspond to normed
backward simulations, very similarly to the way in which normed history relations correspond to
normed forward simulations.
A pair (r; n) is a normed prophecy relation from A to B if r is a step renement from B to
A and (r 1 ; n) is a normed backward simulation from A to B. We write A P B if there is a
normed prophecy relation from A to B, and A  iP B if there is a normed prophecy relation (r; n)
with r 1 image-nite. Thus A  iP B implies A  iB B and A P B, and A P B implies A B B
and B R A. Moreover, if all states of A are reachable, B has nite invisible nondeterminism and
A P B, then A  iP B. It is easy to check that the preorder and soundness results for backward
simulations and renements carry over to prophecy relations.
The following lemma is the analogue of Lemma 6.4 in the backward setting. Using this lemma,
we can prove that normed backward simulations are equivalent to normed prophecy variables
combined with step renements.
Lemma 7.1 Suppose (b; n) is a normed backward simulation from A to B. Let
and let  1 and  2 be the projection functions that map states of C to their rst and second
components, respectively. Let n 0 be the norm function given by n 0 (;
prophecy relation from A to C, and  2 is a step renement from C to B. If
b is image-nite then so is  1Theorem 7.2
1.
2. A  iB B ,
Proof: Analogous to that of Theorem 6.5, using Lemma 7.1.
We can now prove variants of the well-known completeness result of Abadi and Lamport [AL91].
Theorem 7.3 (Completeness of normed history+prophecy relations and step renements)
Suppose A  T B. Then
1.
2. If B has n then 9C; D : A H C  iP D R B.
Proof: By Theorem 6.3, there exists an automaton C with A H C B B. Next, Theorem 7.2
yields the required automaton D with C P D R B, which proves (1). The proof of (2) is
similar, but uses Proposition 5.6.
The following theorem states that P is a partial order on the class of automata with n,
considered modulo isomorphism of reachable subautomata. The proof is analogous to that of
Theorem 6.6, the corresponding result for normed history relations.
Theorem 7.4 Suppose A and B have n, A. Then the reachable subautomata
of A and B are isomorphic.
8 Decidability
Thus far, our exposition has been purely semantic. In the words of [AL91]: \We have considered
specications, but not the languages in which they are expressed. We proved the existence of
renement mappings, but said nothing about whether they are expressible in any language." In
this section, we move to the syntactic world and discuss some decidability issues. To this end we
have to x a language for dening automata. The language below can be viewed as a simplied
version of the IOA language of [GLV97].
We assume an underlying assertion language L which is a rst-order language over interpreted
symbols for expressing functions and predicates over some concrete domains such as integers,
arrays, and lists of integers. If X is a set of (typed) variables then we write F (X) and E(X)
for the collection of formulas and expressions, respectively, in which variables from X may occur
free. An automaton can be described syntactically by rst specifying a nite set X of variables,
referred to as the state variables. For each state variable x we assume the presence of a copy x 0 ,
called the primed version of x. We write X 0 for the set fx 0 j x 2 Xg and, if  is a formula then
we write  0 for the formula obtained from  by replacing each occurrence of a state variable by
its primed version. The set of states of the automaton is dened as the set of all valuations of the
state variables in X . The set of initial states is specied by a predicate in F (X), called the initial
condition. The actions are specied via a nite number of action names with, for each action name
a, a nite list ~v of variables called the parameters of a. We assume f~vg ;. The set of actions
of the automaton is dened as the union, for each action name a, of all tuples a( ~
d), where ~
d is a
valuation of the parameters ~v in their respective domains. The transition relation is specied by
providing, for each action name a with parameters ~v, a transition predicate in F (X[f~vg[X 0 ), i.e.,
a predicate that may contain action parameters as well as primed and unprimed state variables.
Example 8.1 Below we specify a FIFO channel in a self-explanatory IOA like syntax [GLV97].
automaton Channel
states
buffer: Seq[Nat]
initial condition
actions
send(v: Nat),
receive(v: Nat),
tau
transitions
action send(v)
predicate
action receive(v)
predicate buffer ~= {} /\
action tau
predicate false
This piece of syntax denes an automaton A with
steps(A) is the least set that contains the following elements, for all  2 N  and d 2 N,
send(d)
d
receive(d)
Now assume that we have specied two automata A and B, using state variables ~x and ~y,
respectively. Let
A step renement from A to B can be specied by a formula of the form
a list of expressions in E(X) that matches ~y in terms of length and types. In this
formula, the rst conjunct denes the domain of the step renement whereas the second conjunct
denes a map from states of A to states of B by specifying, for each state variable of B, its value
in terms of the values of the state variables of A.
A normed forward simulation can be described by a predicate in F (X [ Y ) together with, for
each action type a with parameters ~v, an expression in E(X [ f~vg [ species the
norm function. In practice, norm functions often only depend on the states of B, which means
that they can be specied by means of a single expression in E(Y ).
Example 8.2 Consider the following specication, essentially just the chaining of two FIFO
channels.
automaton TwoChannels
states
buffer1: Seq[Nat],
buffer2: Seq[Nat]
initial condition
actions
send(v: Nat),
receive(v: Nat),
tau
transitions
action send(v)
predicate
action receive(v)
predicate buffer2 ~= {} /\
action tau
predicate buffer1 ~= {} /\
Let B be the automaton denoted by this specication. It is easy to prove that the formula below
denes a step renement from B to the automaton A of Example 8.1.
It is also routine to check that this formula together with the norm on states of B dened by
if buffer1 ~= {} /\
denes a normed forward simulation from A to B.
We will now show that, under some reasonable (sucient but certainly not necessary) assump-
tions, it is in fact decidable whether a given predicate/expression indeed corresponds to a step
renement or normed forward simulation. Assume that automaton A is described using state
variables ~x, initial condition ' 0 and, for each action name a, a transition predicate ' a . Likewise,
assume that automaton B is described using state variables ~y, initial condition 0 and, for each
action name a, a transition predicate a . Assume further that each action name a of A is also an
action name of B, and that a has the same parameters in both A and B. Write P a for the list of
parameters of a. We require that P
Suppose that we want to check whether a formula
denotes a step renement.
This is equivalent to proving validity of the following formula:
a ' a
In this formula, the rst conjunct asserts that the function is dened for start states of A; the
second conjunct that start states of A are mapped onto start states of B; the third conjunct that
if the function is dened for the source of a transition then it is also dened for the target state
of a transition; and the two nal conjuncts encode the transfer condition. Thus checking whether
a partial function is a step renement from A to B is decidable if the partial function as well as
A and B can all be expressed within a fragment of L for which tautology checking is decidable.
Next suppose that we want to check whether a formula  together with norm expressions n a ,
for each action name a, denotes a normed forward simulation from A to B. In order to turn this
into a decidable question, we have to make some additional assumptions about the specication
of B. We assume that B has nitely many start states 2 , which are listed explicitly, i.e., we require
that the initial condition 0 is of the form
_
where I 0 is a nite index set and, for each i, ~
0 is a list of closed terms. In addition we assume
that in any state and for any given value of the action parameters, only nitely many transitions
are possible in B, which are listed explicitly. Formally we require that, for each action type a,
transition predicate a is of the form
_
i2Ia
a
where I a is a nite index set and, for each i,  i
a is a formula in F (Y [ fP a g) and ~
0 is a list of
expressions in E(Y [ fP a g). Basically,  i
a gives the precondition of the i-th instance of transition
a and ~
a species the eect of taking it. Both assumption (3) and (4) are satised by most
automaton specications that one encounters in practice. In particular, the assumptions hold for
the channels specied in Examples 8.1 and 8.1. Only specications that involve a nondeterministic
choice that is not a priori bounded fall outside of our format. An example of this, described in
93], is a FIFO channel in which a crash action may result in the loss of an arbitrary
subset of the messages contained in a buer. Under assumptions (3) and (4), we can eliminate the
existential quantiers that occur in the denition of a normed forward simulation, and checking
the conditions in this denition becomes equivalent to proving validity of the following formula:
_
_
i2Ia
_
i2I
_
i2I
_
i2I
If this formula can be expressed within a fragment of L for which tautology checking is decidable
then it is decidable whether  together with expressions n a constitutes a normed forward simula-
tion. It is easy to see that a similar result can also be obtained for normed history variables. Thus
far, however, we have not been able to come up with plausible syntactic restrictions, applicable in
practical cases, that ensure decidability of normed backward simulations and/or normed prophecy
relations. It is for instance not clear how one can eliminate the existential quantier in the formula
This assumption can be relaxed if we assume that the value of certain state variables of B is fully determined
by  and the state of A: for those state variables the initial value can be left unspecied.
that asserts that in a normed backward simulation for each state of A there exists a related state
of B.
Our decidability results for step renements and normed forward simulations do not carry over
to the renements and forward simulations as described, for instance, in [LV95]. In order to see
this, let A be a system with two states, an initial and a nal one, and a single transition labeled
halt from the initial to the nal state. Let B be a system that simulates the n-th Turing machine
such that each computation step of the Turing machine corresponds with a -move, and that
moves via a halt-action to a designated nal state if and only if the computation of the Turing
machine terminates. The function that maps the initial state of A to the initial state of B and the
nal state of A to the nal state of B is a weak renement i the n-th Turing machine halts. It
is straightforward to specify A, B and the function from states of A to states of B in a decidable
logic. Hence it is undecidable whether a given function is a weak renement, even in a setting
where the underlying logic is decidable.
9 Reachability
For the sake of simplicity, all denitions of simulations and renements so far have been presented
without any mention of reachability or invariants. However, in practical verications it is almost
always the case that rst some invariants (properties that hold for all reachable states) are established
for the lower-level and/or higher-level specication. These invariants are then used in
proving the step correspondence. In this section we show how to integrate reachability concerns
into the simulation denitions. More specically, we present adapted versions of step renements,
normed forward simulations and normed backward simulations which include reachability con-
cerns, and discuss their relationship with the original denitions. For examples of the use of these
adapted denitions and their formalization in PVS, we refer to [Gri00].
An adapted step renement from A to B consists of a partial function r
satisfying the following two conditions:
1. If s 2 start(A) then s 2 domain(r) and r(s) 2 start(B ).
2. If s a
(a)
(b) r(s) a
!B r(t).
Clause reachable(A; s) in condition (2) allows us to reuse invariants that have previously been
established for lower-level specication A, whereas clause reachable(B; r(s)) in condition (2) makes
it possible to reuse known invariants of higher-level specication B. The adapted denition can
easily be seen as a special case of the original denition in Section 3.1: if r is an adapted step
renement then the restriction r 0 of r dened by
is a regular step renement. Conversely, any regular step renement trivially satises the conditions
of the adapted version.
An adapted normed forward simulation from A to B consists of a relation f  states(A)
states(B) and a function n : steps(A)  states(B) ! S, for some well-founded set S, such that:
1. If s 2 start(A) then f [s] \ start(B) 6= ;.
2. If s a
(a)
!B v, or
(c)
Again, the clause reachable(A; s) in condition (2) allows us to reuse invariants that have previously
been established for A, whereas clause reachable(B; u) in condition (2) permits reuse of invariants
of B. And again the adapted denition can easily been seen as a special case of the original
denition (in Section 4): if (f; n) is an adapted normed forward simulation then the pair (g; n),
reachable(B)), is a regular normed forward simulation. Conversely,
any regular normed forward simulation trivially is an adapted normed forward simulation.
An adapted normed backward simulation from A to B consists of a relation b  states(A)
states(B ), a predicate Q  states(B ), and a function
for some well-founded set S, such that:
1. If s
(a)
2. If t a
(a)
(c) 9v
3. If reachable(A; s) then 9u
Clause reachable(A; t) in condition (2) allows us to reuse invariants that have previously been
established for A, and clause Q(u) in condition (2) permits reuse of invariants of B. Note that by
a trivial inductive argument a backward simulation can never relate a reachable state of A to a
non-reachable state of B. Thus we can safely restrict the range of any backward simulation by all
invariants proven for B. To this end predicate Q has been included in the denition of the adapted
normed backward simulation, even though strictly speaking (1) Q need not be an invariant, and
(2) Q can always be eliminated by restricting the range of b. Once more the adapted denition
is a special case of the original denition (in Section 5): if (b; n) is an adapted normed backward
simulation then (b; n) is also a regular normed backward simulation from the automaton A 0 , that
restricts A to its reachable states, to the automaton B 0 , that restricts B to the states in Q.
Conversely, any regular normed backward simulation trivially is an adapted normed backward
simulation with
We leave it up to the reader to work out adapted versions of the normed history and prophecy
relations.

Acknowledgement

We thank Marielle Stoelinga for spotting a mistake in an earlier version of this paper, and Jan
Willem Klop for discussions that led us to Theorem 6.6.



--R

Equational term graph rewriting.
The existence of re
Branching bisimilarity is an equivalence indeed!

Powerful techniques for the automatic generation of invariants.
Norm functions for probabilistic bisimulations with delays.


Three logics for branching bisimulation.
Algebraic Theory of Automata.
IOA: A language for speci

Focus points and convergent process operators


Branching time and abstraction in bisimulation semantics.

Compositional Veri
On decomposing and re
Fundamental Algorithms
Hierarchical correctness proofs for distributed algo- rithms
I: Untimed systems.
II: Timing-based systems
Distributed Algorithms.
Visual abstraction for temporal veri
Englewood Cli

A simple characterization of stuttering bisimulation.
I/O automata in Isabelle/HOL.
An axiomatic proof technique for parallel programs.
Formal veri
Data Re


Proving correctness with respect to nondeterministic safety speci
--TR
Hierarchical correctness proofs for distributed algorithms
Proving entailment between conceptual state specifications
Characterizing finite Kripke structures in propositional temporal logic
On decomposing and refining specifications of distributed systems
The existence of refinement mappings
Proving correctness with respect to nondeterministic safety specifications
languages and tools for formal specification
Compositional specification and verification of distributed systems
Proving nondeterministically specified safety properties using progress measures
Proof-checking a data link protocol
Three logics for branching bisimulation
Formal Verification for Fault-Tolerant Architectures
Forward and backward simulations I.
Branching bisimilarity is an equivalence indeed!
Forward and backward simulations II.
Branching time and abstraction in bisimulation semantics
Equational term graph rewriting
The art of computer programming, volume 1 (3rd ed.)
A model and proof system for asynchronous networks
Verification of a Leader Election Protocol
Distributed Algorithms
Communication and Concurrency
Visual Abstractions for Temporal Verification
Incremental Verification by Abstraction
Possibly Infinite Sequences in Theorem Provers
I/Q Automata in Isabelle/HOL
Simulations Between Specifications of Distributed Systems
Norm Functions for Probabilistic Bisimulations with Delays
A Simple Characterization of Stuttering Bisimulation
Normed Simulations
Computer-Assisted Simulation Proofs
Powerful Techniques for the Automatic Generation of Invariants
Verifying Safety Properties Using Non-deterministic Infinite-state Automata
Focus Points and Convergent Process Operators
LIVENESS IN TIMED AND UNTIMED SYSTEMS
Correctness of Communications Protocols, A case Study
An algebraic definition of simulation between programs
automata;computer-aided verification;prophecy variables;forward simulations;normed simulations;refinement mappings;backward simulations;history variables