BRICS RS-97-26 Aceto & Ingólfsdóttir: A Characterization of Finitary Bisimulation BRICS

Basic Research in Computer Science

A Characterization of Finitary Bisimulation

Luca Aceto Anna Ingólfsdóttir BRICS Report Series RS-97-26 ISSN 0909-0878 October 1997 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1997, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/97/26/

A Characterization of Finitary Bisimulation

Luca Aceto^{∗}

BRICS^{†}, Department of Computer Science, Aalborg University Fredrik Bajersvej 7E, 9220 Aalborg Ø, Denmark

                          Email: luca@cs.auc.dk

Anna Ingólfsdóttir^{‡}

Dipartimento di Sistemi ed Informatica, Università di Firenze Via Lombroso 6/17, 50134 Firenze, Italy

                     Email: annai@dsi2.ing.unifi.it

Keywords and Phrases: Concurrency, labelled transition system with divergence, bisimulation preorder, finitary relation.

1 Introduction

Following a paradigm put forward by Milner and Plotkin, a primary criterion to judge the appropriateness of denotational models for programming and specification languages is that they be in agreement with operational intuition about program behaviour. Of the “good fit” criteria for such models that have been discussed in the literature, the most desirable one is that of full abstraction. Intuitively, a fully abstract denotational model is guaranteed to relate exactly all those programs that are operationally indistinguishable with respect to some chosen notion of observation.

Because of its prominent role in process theory, bisimulation [12] has been a natural yardstick to assess the appropriateness of denotational models for several process description languages. In particular, when proving full abstraction results for denotational semantics based on the Scott-Strachey approach for CCS-like languages, several preorders based on bisimulation have been considered; see, e.g., [6, 3, 4]. In this paper, we shall study one such bisimulationbased preorder whose connections with domain-theoretic models are by now well understood, viz. the prebisimulation preorder ≲ investigated in, e.g., [6, 3]. Intuitively, p ≲ q holds of processes p and q if p and q can simulate each other’s behaviour, but at times the behaviour of p may be less specified than that of q.

A common problem in relating denotational semantics for process description languages, based on Scott’s theory of domains or on the theory of algebraic semantics, with behavioural semantics based on bisimulation is that the chosen behavioural theory is, in general, too concrete. The reason for this phenomenon is that two programs are related by a standard denotational interpretation if, in some precise sense, they afford the same finite observations. On the other hand, bisimulation can make distinctions between the behaviours of two processes based on infinite observations. (Cf. the seminal study [1] for a detailed analysis of this phenomenon.) To overcome this mismatch between the denotational and the behavioural theory, all the aforementioned full abstraction results are obtained with respect to the so-called finitely observable, or finitary, part of bisimulation. The finitary bisimulation is defined on any labelled transition system thus: p ≲^{F} q iff t ≲ p implies t ≲ q, for every finite synchronization tree t.

∗Partially supported by the Human Capital and Mobility project Express.

†Basic Research in Computer Science, Centre of the Danish National Research Foundation.

‡Supported by a grant from the Danish Research Council.

An alternative characterization of the finitary bisimulation for arbitrary transition systems has been given by Abramsky in [1]. This characterization is couched in logical terms, and is an impressive byproduct of Abramsky’s “theory of domains in logical form” programme. More precisely, Abramsky shows that two processes in any transition system are equated by the finitary bisimulation iff they satisfy the same formulae in the finitary version of the domain logic for transition systems. The existence of this logical view of the finitary bisimulation gives us a handle to work with this relation. However, an alternative, behavioural view of the finitary bisimulation might be more useful when establishing results which are more readily shown on the behavioural, rather than on the logical, side. Examples of such results are complete axiomatizations for the finitary bisimulation and full abstraction results. A behavioural characterization of the finitary bisimulation would also provide an easier way to establish when two processes in a transition system are related by it or not, thus giving more insight on the kind of identifications made by this relation.

In this study, we offer a behavioural characterization of the finitary bisimulation for arbitrary transition systems (cf. Thm. 3.5). This result may be seen as the behavioural counterpart of Abramsky’s logical characterization theorem [1, Thm. 5.5.8]. Moreover, for the important class of sort-finite transition systems we present a sharpened version of a behavioural characterization result first proven by Abramsky in [3, Propn. 6.13]. The interested reader may consult the unpublished report [5] for more results on the finitary bisimulation.

2 Preliminaries

We begin by reviewing a variation on the model of labelled transition systems [9] that takes divergence information into account. We refer the interested readers to, e.g., [11] for motivation and more information on this semantic model for reactive systems. A labelled transition system with divergence (lts) is a quadruple (Proc, Act, →, ↑), where:

• Proc is a set of processes, ranged over by p, q, r, s, possibly subscripted or superscripted;

• Act is a set of actions, ranged over by a, b, possibly subscripted;

• →⊆ Proc × Act × Proc is a transition relation. As usual, we shall use the more suggestive notation p →^{a} q in lieu of (p, a, q) ∈→;

• ↑⊆ Proc is a divergence predicate, notation p ↑.

We write p ↓, read “p converges”, iff it is not the case that p ↑. Intuitively, the fact that a process p converges means that its initial behaviour is completely specified. On the contrary, the divergence of a process signifies that the information on its initial behaviour is incomplete.

For n ≥ 0 and σ = a_{1} … a_{n} ∈ Act^{∗}, we write p →^{σ} q iff there exist processes

p_{0}, …, p_{n} such that p = p_{0} →^{a_{1}} p_{1} →^{a_{2}} ⋯ p_{n−1} →^{a_{n}} p_{n} = q. For a process p ∈ Proc

and action a ∈ Act we define:

initials(p) =^{Δ} {a ∈ Act | ∃q : p →^{a} q}
sort(p) =^{Δ} {a ∈ Act | ∃σ ∈ Act^{∗}, r, s ∈ Proc : p →^{σ} r →^{a} s}
derivatives(p, a) =^{Δ} {q | p →^{a} q} .

Following [3], we say that an lts is sort-finite iff sort(p) is finite for every p ∈ Proc.

A useful source of examples for labelled transition systems with divergence is the set of countably branching synchronization trees over a set of labels Act, denoted by ST_{∞}(Act). This is the set of infinitary terms generated by the inductive definition:

\frac{\{a_{i} ∈ Act, t_{i} ∈ ST_{∞}(Act)\}_{i∈I}}{∑_{i∈I} a_{i} : t_{i}[+Ω] ∈ ST_{∞}(Act)}

where I is a countable index set, and the notation [+Ω] means optional inclusion of Ω as a summand. We shall write 𝕆 for ∑_{i∈∅} a_{i} : t_{i}, and Ω for ∑_{i∈∅} a_{i} : t_{i} +Ω. Intuitively, 𝕆 stands for the one-node synchronization tree, a representation of an inactive process, and Ω stands for the synchronization tree whose behaviour is completely unspecified.

The set of terms built using only finite summations, i.e. the finite synchronization trees, will be denoted by ST(Act). The set of synchronization trees ST_{∞}(Act) can be turned into a labelled transition system with divergence by stipulating that, for t ∈ ST_{∞}(Act):

• t ↑ iff Ω is a summand of t, and

• t →^{a_{i}} t_{i} iff a_{i} : t_{i} is a summand of t.

The behavioural relation over processes that we shall study in this paper is that of prebisimulation [8, 11, 6, 13] (also known as partial bisimulation [3]).

Definition 2.1 Let (Proc, Act, →, ↑) be an lts. Let Rel(Proc) denote the set of binary relations over Proc. Define the functional F : Rel(Proc) → Rel(Proc) by:

F (R) = {(p, q) | ∀a ∈ Act

• p →^{a} p′ ⇒ ∃q′ : q →^{a} q′ and p′ R q′

• p ↓⇒ (q ↓ and (q →^{a} q′ ⇒ ∃p′ : p →^{a} p′ and p′ R q′))}

A relation R is a prebisimulation iff R⊆ F (R). We write p ≲ q iff there exists a prebisimulation R such that p R q.

An alternative method for using the functional F to obtain a behavioural preorder is to apply it inductively as follows:

≲_{0} =^{Δ} Proc × Proc
≲_{n+1} =^{Δ} F (≲_{n})

and finally ≲_{ω}=^{Δ} ⋂_{n≥0} ≲_{n}. Intuitively, the preorder ≲_{ω} is obtained by restricting the prebisimulation relation to observations of finite depth. As a standard example of the relevance of this restriction, consider the processes

p =^{Δ}  (∑_{i≥1} \underbrace{a : ⋯: a :}_{i-times} 𝕆) + Ω
q =^{Δ} p + a^{ω}

where a^{ω} denotes an infinite sequence of a actions. Then q ≴ p because the transition q →^{a} a^{ω} cannot be matched by any a-transition emanating from p. On the other hand, it is easy to see that q ≲_{ω} p does hold.

In this paper, we are interested in studying the “finitely observable”, or finitary, part of the bisimulation in the sense of, e.g., [6]. The following definition is from [3].

Definition 2.2 Let (Proc, Act, →, ↑) be an lts. The finitary bisimulation preorder ≲^{F} over Proc is defined as follows: p ≲^{F} q iff, for every t ∈ ST(Act), t ≲ p implies t ≲ q.

The preorders ≲, ≲_{ω} and ≲^{F} are related thus: ≲ ⊆ ≲_{ω} ⊆ ≲^{F}. Moreover the inclusions are strict for infinitely branching lts’s, and collapse to equalities for finitely branching ones. The interested reader is referred to [3] for a wealth of examples distinguishing these preorders, and a very deep analysis of their general relationships and properties.

3 The Behavioural Characterization

Abramsky’s logical characterization of the finitary bisimulation provides one general, observation-independent alternative view of ≲^{F}. It can be viewed as the counterpart of the modal characterization theorems for bisimulation-based equivalences and preorders which have been so popular and fruitful since the seminal [11, 7]. However, in order to gain more insight into the exact nature of the relationships between processes supported by ≲^{F}, and as a further tool for the study of this preorder (for example to establish results on full abstraction of denotational models and complete axiomatizations), it is useful to have purely behavioural, observation-independent characterizations of it. One such characterization was provided by Abramsky in, e.g., [3, Propn. 6.13]. There Abramsky shows that in any sort-finite lts that satisfies his axiom scheme of bounded nondeterminacy (BN) (cf. [1, Page 114]), the finitary bisimulation coincides with ≲_{ω}. We shall now present a bisimulation-like characterization of the finitary bisimulation for arbitrary transition systems. As a byproduct of our analysis of the finitary bisimulation, we shall be able to improve upon Abramsky’s behavioural characterization of ≲^{F} for sort-finite lts’s. (Cf. Propn. 3.6.)

Consider an arbitrary lts (Proc, Act, →, ↑). For every A ⊆ Act, we define the sequence of relations {⊏_{∼}_{n}^{A}| n ≥ 0} thus:

p ⊏_{∼}_{0}^{A} q ⇔ true
p ⊏_{∼}_{n+1}^{A} q ⇔ (1) ∀a ∈ A, p′ ∈ Proc. p →^{a} p′ ⇒ ∃q′ : q →^{a} q′ and p′ ⊏_{∼}_{n}^{A} q′

(2) If initials(p) ⊆ A and p ↓ then (2.1) initials(q) ⊆ A and q ↓

(2.2) ∀a ∈ A, q′ ∈ Proc. q →^{a} q′ ⇒ ∃p′ : p →^{a} p′ and p′ ⊏_{∼}_{n}^{A} q′ .

The following proposition collects some basic properties of the relations ⊏_{∼}_{n}^{A} which will be useful in the remainder of this study.

Proposition 3.1 For every n ≥ 0 and A ⊆ Act, the following statements hold:

1. The relation ⊏_{∼}_{n}^{A} is a preorder.

2. For p, q ∈ Proc, p ⊏_{∼}_{n+1}^{A} q implies p ⊏_{∼}_{n}^{A} q.

3. Assume that A ⊆ B ⊆ Act. Then, for p, q ∈ Proc, p ⊏_{∼}_{n}^{B} q implies p ⊏_{∼}_{n}^{A} q.

We now define:

p ⊏_{∼}_{ω}^{A} q =^{Δ} ∀n ≥ 0. p ⊏_{∼}_{n}^{A} q
p ⊏_{∼}_{ω}^{fin} q =^{Δ} ∀A ⊆_{fin} Act. p ⊏_{∼}_{ω}^{A} q

where the notation A ⊆_{fin} Act means that A is a finite subset of Act. Note that, in light of Propn. 3.1(1), both the relations defined above are preorders. As initials(p) is contained in Act for every process p ∈ Proc, the preorder ⊏_{∼}Act_{ω} coincides with ≲_{ω}.

The above definitions are inspired by [8, page 266], where a preorder over value-passing CCS [10] which uses finite sets of communication capabilities of processes in a similar manner is presented. Intuitively, p ⊏_{∼}_{ω}^{A} q holds for two processes p and q iff there is no observation, in the sense of [2], of finite depth, and with actions drawn from the set A, that can distinguish between p and q. For example, p ⊏_{∼}_{ω}^{∅} q holds unless p is a convergent inactive process and q is either divergent or capable of performing some action. A similar intuition applies to the relation ⊏_{∼}_{ω}^{fin}, but there observations can only be drawn from finite sets of actions and are therefore required to have finite width as well as finite depth. That this is significant is shown by the following example:

Example: Assume that Act = {a_{i} | i ≥ 0}, and that i ≠ j implies a_{i} ≠ a_{j}. Consider the synchronization trees p and q given by:

p =^{Δ}  ∑_{i≥0} a_{i} : 𝕆  (1)
q =^{Δ} p + Ω .  (2)

Then p ≴_{1} q because p ↓ but q ↑. However, p ⊏_{∼}_{ω}^{fin} q. In fact, every transition from p can be matched identically by q, and, for A ⊆_{fin} Act, clause (2) in the definition of ⊏_{∼}_{n+1}^{A} is always vacuously satisfied because initials(p) = Act, which is countably infinite.

Indeed, it is also the case that p ≲^{F} q. In fact, let t ∈ ST(Act) be such that t ≲ p. We shall now argue that t ≲ q must also hold. First of all, note that t ≲ p implies that t ↑. (This is easy to see because otherwise the finite synchronization tree t would have to have Act as its set of initial actions.) Next we remark that if t →^{a} t′ for some action a, then t′ ≲ 𝕆. From these two observations, it follows immediately that t ≲ q. (End of Example)

Let (Proc, Act, →, ↑) be an arbitrary lts. Our aim is to show that ≲^{F} coincides with ⊏_{∼}_{ω}^{fin} over Proc. We begin by establishing two auxiliary results.

Lemma 3.2 For every t ∈ ST(Act), p ∈ Proc, t ≲ p iff t ⊏_{∼}_{ω}^{fin} p

Proof: The ‘only if’ implication is an immediate consequence of the following fact, which may be easily shown by mathematical induction on n,

∀t ∈ ST(Act), p ∈ Proc, n ≥ 0, A ⊆ Act. t ≲ p ⇒ t ⊏_{∼}_{n}^{A} p .

Here we just remark that if t ≲ p, t ↓ and initials(t) ⊆ A, then the definition of ≲ yields immediately that p ↓ and initials(p) ⊆ A.

In the proof of the ‘if’ implication, we shall make use of the notion of height of a synchronization tree. This is the ordinal defined thus:

ht(∑_{i∈I} a_{i} : t_{i}[+Ω]) =^{Δ} sup {ht(t_{i}) | i ∈ I} + 1 .

To establish the ‘if’ implication, it is sufficient to prove the following statement:

∀t ∈ ST(Act), p ∈ Proc. t ⊏_{∼}sort(t)_{ht(t)} p ⇒ t ≲ p .

The straightforward proof is by complete induction on ht(t). Here we limit ourselves to showing that

t ⊏_{∼}sort(t)_{ht(t)} p and t →^{a} t′ implies p →^{a} p′ for some p′ such that t′ ≲ p′ .

To this end, assume that t ⊏_{∼}sort(t)_{ht(t)} p and t →^{a} t′. Under these assumptions, ht(t) > 0

and it follows that p →^{a} p′ for some p′ such that t′ ⊏_{∼}sort(t)_{ht(t)−1} p. It is easy to see that

ht(t′) ≤ ht(t) − 1 and sort(t′) ⊆ sort(t). Thus, Propn. 3.1(2)-(3) yields t′ ⊏_{∼}sort(t′)_{ht(t′)} p′. As ht(t′) < ht(t), the induction hypothesis gives t′ ≲ p′ as required. □

The finitary bisimulation has the property that, for all p, q ∈ Proc,

p ≲^{F} q iff for every t ∈ ST(Act), t ≲^{F} p implies t ≲^{F} q .  (3)

This is an immediate consequence of the fact that t ≲ p iff t ≲^{F} p, for every finite synchronization tree t and process p. A binary relation over processes that enjoys property (3) is usually called finitary or finitely approximable [6, 4].

Lemma 3.3 The preorder ⊏_{∼}_{ω}^{fin} is finitary.

Before proving this lemma, we introduce some intermediate definitions and results. For every process p ∈ Proc, finite action set A and non-negative integer n, we define a synchronization tree p^{(A,n)} as follows:

p^{(A,0)} =^{Δ} Ω
p^{(A,n+1)} =^{Δ} ∑ {a : q^{(A,n)} | a ∈ A, q ∈ derivatives(p, a)}
[+Ω | p ↑ or initials(p) ⊈ A] .

Intuitively, the synchronization tree p^{(A,n)} stands for the approximation of the behaviour of p of width A and height n + 1. For example, if we apply the above definition to derive the approximations of the infinitely branching synchronization trees p and q given in (1) and (2), respectively, we obtain that, for every A ⊆_{fin} Act and n ≥ 0,

p^{(A,n+1)} = ∑_{{i|a_{i}∈A}} a_{i} : 𝕆^{(A,n)} + Ω = q^{(A,n+1)}

where 𝕆^{(A,n)} is Ω if n = 0, and 𝕆 otherwise. Thus, albeit p is a convergent synchronization tree, all of its approximations are divergent, and coincide with the approximations of the behaviour of q.

By a simple induction, we may show that, for every finite set of actions A and non-negative integer n, the set of synchronization trees {p^{(A,n)} | p ∈ Proc} is finite. Therefore the synchronization tree p^{(A,n+1)} is finite even when the set derivatives(p, a) is infinite for some a ∈ A. The fact that the synchronization trees p^{(A,n)} do behave as approximations of the behaviour of p of width A and depth n is the import of the following result, which may be easily shown by mathematical induction:

Lemma 3.4 For every A ⊆_{fin} Act, n ≥ 0,

1. p ⊏_{∼}_{n}^{A} p^{(A,n)}, and

2. p^{(A,n)} ≲ p.

We are now in a position to prove statement Lemma 3.3 above, i.e., that the preorder ⊏_{∼}_{ω}^{fin} is finitary.

Proof of Lemma 3.3: We prove that

p ⊏_{∼}_{ω}^{fin} q iff ∀t ∈ ST(Act). t ⊏_{∼}_{ω}^{fin} p ⇒ t ⊏_{∼}_{ω}^{fin} q .

The ‘only if’ implication follows immediately from the fact that ⊏_{∼}_{ω}^{fin} is a preorder. To establish the ‘if’ implication, let us assume that p and q are two processes such that, for every t ∈ ST(Act),

t ⊏_{∼}_{ω}^{fin} p ⇒ t ⊏_{∼}_{ω}^{fin} q .  (4)

We show that p ⊏_{∼}_{n}^{A} q holds for every finite set of actions A and non-negative integer n. To this end, let A ⊆_{fin} Act and n ≥ 0. We know that p ⊏_{∼}_{n}^{A} p^{(A,n)} ≲ p (Lemma 3.4). As p^{(A,n)} is a finite synchronization tree, it follows that p ⊏_{∼}_{n}^{A} p^{(A,n)} ⊏_{∼}_{ω}^{fin} p (Lemma 3.2). Using (4), we now obtain that p ⊏_{∼}_{n}^{A} p^{(A,n)} ⊏_{∼}_{ω}^{fin} q holds. By the definition of ⊏_{∼}_{ω}^{fin} and the transitivity of ⊏_{∼}_{n}^{A} (Propn. 3.1(1)), we finally infer that p ⊏_{∼}_{n}^{A} q holds, which was to be shown. □

Collecting the intermediate results presented so far, we can now establish the main result of this paper.

Theorem 3.5 For p, q ∈ Proc in any transition system, p ≲^{F} q iff p ⊏_{∼}_{ω}^{fin} q.

Proof: The preorder ⊏_{∼}_{ω}^{fin} is finitary (Lemma 3.3), and coincides with ≲—and thus with ≲^{F} —over ST(Act) × Proc (Lemma 3.2). It is immediate to see that two finitary relations that coincide over ST(Act) × Proc do coincide over the whole of Proc. □

In [3, Propn. 6.13], Abramsky showed that for any sort-finite lts satisfying his axiom scheme of bounded nondeterminacy (BN) (cf. op. cit. on page 193), the finitary bisimulation coincides with the ω-iterate of the bisimulation preorder ≲_{ω}. Following the proof of our previous characterization theorem, we can now present a sharpened version of this result, which does not require the lts’s to satisfy the axiom (BN).

Proposition 3.6 For p, q ∈ Proc in any sort-finite transition system, p ≲^{F} q iff p ≲_{ω} q.

Proof: It is well-known that, in any lts, not necessarily sort-finite, p ≲_{ω} q implies p ≲^{F} q. We are therefore left to show that, for p, q ∈ Proc in any sort-finite transition system, p ≲^{F} q implies p ≲_{ω} q. This statement can be shown by mimicking the proof of Lemma 3.3 presented above. In fact, it is not too hard to show that, for every process p in a sort-finite lts, n ≥ 0 and finite set of actions A including sort(p), p ≲_{n} p^{(A,n)} ≲ p. In particular, we obtain that p ≲_{n} p^{(sort(p),n)} ≲ p. If p ≲^{F} q and sort(p) is finite, it follows that p ≲_{n} p^{(sort(p),n)} ≲ q. Using the fact that ≲ is included in ≲_{ω}, we may now infer that p ≲_{n} q holds for every n ≥ 0. We have therefore shown that, if p ≲^{F} q and sort(p) is finite, then p ≲_{ω} q. □

Acknowledgements: We thank the anonymous referees for their constructive suggestions.

References

[1] S. Abramsky, Domain Theory and the Logic of Observable Properties, PhD thesis, University of London, 1987. Available on the World Wide

    Web at the URL http://theory.doc.ic.ac.uk:80/people/Abramsky/
    as file phd.ps.gz.

[2] , Observation equivalence as a testing equivalence, Theoretical Comput. Sci., 53 (1987), pp. 225–241.

[3] , A domain equation for bisimulation, Information and Computation, 92 (1991), pp. 161–218.

[4] L. Aceto and M. Hennessy, Termination, deadlock and divergence, J. Assoc. Comput. Mach., 39 (1992), pp. 147–187.

[5] L. Aceto and A. Ingólfsdóttir, On the finitary bisimulation, Research Report RS–95–59, BRICS (Basic Research in Computer Science, Centre of the Danish National Research Foundation), Department of Computer Science, Aalborg University, Nov. 1995. Available by anonymous ftp at

the address ftp.daimi.aau.dk in the directory pub/BRICS/RS/95/59.

[6] M. Hennessy, A term model for synchronous processes, Information and Control, 51 (1981), pp. 58–75.

[7] M. Hennessy and R. Milner, Algebraic laws for nondeterminism and concurrency, J. Assoc. Comput. Mach., 32 (1985), pp. 137–161.

[8] M. Hennessy and G. Plotkin, A term model for CCS, in 9^{th} Symposium on Mathematical Foundations of Computer Science, P. Dembiński, ed., vol. 88 of Lecture Notes in Computer Science, Springer-Verlag, 1980, pp. 261–274.

[9] R. Keller, Formal verification of parallel programs, Comm. ACM, 19 (1976), pp. 371–384.

[10] R. Milner, A Calculus of Communicating Systems, vol. 92 of Lecture Notes in Computer Science, Springer-Verlag, 1980.

[11] , A modal characterisation of observable machine behaviour, in Proceedings CAAP 81, G. Astesiano and C. Bohm, eds., vol. 112 of Lecture Notes in Computer Science, Springer-Verlag, 1981, pp. 25–34.

[12] D. Park, Concurrency and automata on infinite sequences, in 5^{th} GI Conference, Karlsruhe, Germany, P. Deussen, ed., vol. 104 of Lecture Notes in Computer Science, Springer-Verlag, 1981, pp. 167–183.

[13] D. Walker, Bisimulation and divergence, Information and Computation, 85 (1990), pp. 202–241.

Recent BRICS Report Series Publications

RS-97-26 Luca Aceto and Anna Ingólfsdóttir. A Characterization of Finitary Bisimulation. October 1997. 9 pp. To appear in Information Processing Letters.

RS-97-25 David A. Mix Barrington, Chi-Jen Lu, Peter Bro Miltersen, and Sven Skyum. Searching Constant Width Mazes Captures the AC^{0} Hierarchy. September 1997. 20 pp.

RS-97-24 Søren B. Lassen. Relational Reasoning about Contexts. September 1997. 45 pp. To appear as a chapter in the book Higher Order Operational Techniques in Semantics, eds. Andrew D. Gordon and Andrew M. Pitts, Cambridge University Press.

RS-97-23 Ulrich Kohlenbach. On the Arithmetical Content of Restricted Forms of Comprehension, Choice and General Uniform Boundedness. August 1997. 35 pp.

RS-97-22 Carsten Butz. Syntax and Semantics of the logic L_{ωω}^{λ}. July 1997. 14 pp.

RS-97-21 Steve Awodey and Carsten Butz. Topological Completeness for Higher-Order Logic. July 1997. 19 pp.

RS-97-20 Carsten Butz and Peter T. Johnstone. Classifying Toposes for First Order Theories. July 1997. 34 pp.

RS-97-19 Andrew D. Gordon, Paul D. Hankin, and Søren B. Lassen. Compilation and Equivalence of Imperative Objects. July 1997. iv+64 pp. Appears also as Technical Report 429, University of Cambridge Computer Laboratory, June 1997. To appear in Foundations of Software Technology and Theoretical Computer Science: 17th Conference, FCT&TCS ’97 Proceedings, LNCS, 1997.

RS-97-18 Robert Pollack. How to Believe a Machine-Checked Proof. July 1997. 18 pp. To appear as a chapter in the book Twenty Five Years of Constructive Type Theory, eds. Smith and Sambin, Oxford University Press.

RS-97-17 Peter Bro Miltersen. Error Correcting Codes, Perfect Hashing Circuits, and Deterministic Dynamic Dictionaries. June 1997. 10 pp.