BRICS RS-95-59 Aceto & Ing� olfsd� ottir: On the Finitary Bisimulation

BRICS

Basic Research in Computer Science

On the Finitary Bisimulation

Luca Aceto Anna Ing� olfsd� ottir

BRICS Report Series RS-95-59 ISSN 0909-0878 November 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, 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 publications in the BRICS Report Series. 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@daimi.aau.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

On the Finitary Bisimulation

Luca Aceto^{∗}  Anna Ingólfsdóttir^{†}
BRICS^{‡}

Department of Mathematics and Computer Science Aalborg University Fredrik Bajersvej 7E 9220 Aalborg Ø, Denmark

Abstract

The finitely observable, or finitary, part of bisimulation is a key tool in establishing full abstraction results for denotational semantics for process algebras with respect to bisimulation-based preorders. A bisimulation-like characterization of this relation for arbitrary transition systems is given, relying on Abramsky’s characterization in terms of the finitary domain logic. More informative behavioural, observation-independent characterizations of the finitary bisimulation are also offered for several interesting classes of transition systems. These include transition systems with countable action sets, those that have bounded convergent sort and the sort-finite ones. The result for sort-finite transition systems sharpens a previous behavioural characterization of the finitary bisimulation for this class of structures given by Abramsky.

AMS Subject Classification (1991): 68Q10 (Modes of computation), 68Q55 (Semantics), 03B70 (Logic of Programming), 68Q90 (Transition nets). Keywords and Phrases: Concurrency, labelled transition systems with divergence, bisimulation preorder, finitary relations, domain logic for transition systems.

1 Introduction

Following a paradigm put forward by Milner and Plotkin in their seminal papers [20, 21, 26], 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 (cf., e.g., the reference [19] for a discussion), the most desirable one is that of full abstraction. Intuitively, a denotational model for a programming or specification language is fully abstract with respect to a notion of operationally based (or behavioural) equivalence or preorder iff it is in complete agreement with it. In other words, 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.

∗On leave from School of Cognitive and Computing Sciences, University of Sussex, Brighton BN1 9QH, UK. Partially supported by HCM project express. Email: luca@iesd.auc.dk.

†Email: annai@iesd.auc.dk.

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

Because of its prominent rôle in process theory, bisimulation [25, 24] has been a natural operational 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 [29] for CCS-like languages, several preorders based on bisimulation have been considered. (The interested reader is invited to consult, e.g., [13, 10, 4, 6, 17] for examples of full abstraction results with respect to bisimulation-based preorders for variations on CCS.) In this paper, we shall study one such bisimulation-based preorder whose connections with domain-theoretic models are by now well understood, viz. the prebisimulation preorder investigated in, e.g., [10, 4]. This preorder will henceforth be denoted by ≲. Intuitively, p ≲ q holds of processes p and q iff 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 [27] or on the theory of algebraic semantics [9], 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 [4] for a detailed analysis of this phenomenon.) As an example, consider the infinite synchronization trees

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

where Ω stands for the synchronization tree whose behaviour is completely unspecified, and 𝕆 stands for the one-node synchronization tree. Then, in a precise sense, no finite amount of observation can distinguish the behaviour of p from that of q. On the other hand, q ≲ p does not hold because p cannot simulate the infinite a-computation possessed by q.

To overcome this mismatch between the denotational and the behavioural theory, all the aforementioned full abstraction results are couched in terms of the so-called finitely observable, or finitary, part of bisimulation. (This relation will be henceforth referred to as the finitary bisimulation.) The finitary bisimulation preorder, denoted by ≲^{F}, is defined on any labelled transition system thus:

p ≲^{F} q iff for every finite synchronization tree t, t ≲ p implies t ≲ q .

The above definition of the finitary bisimulation, albeit very natural and intuitive, is rather indirect; it simply says that two processes are related iff they afford the same finite observations, which are taken to be finite, possibly partially specified, synchronization trees. Such an indirect definition often makes it quite hard to establish results about this relation, and a lot of research effort has been devoted to finding alternative, observation-independent versions of the finitary bisimulation for different process description languages. (Cf., e.g., [10, 4, 6, 16] for examples of these results.)

A general, observation-independent characterization of the finitary bisimulation for arbitrary transition systems has been given by Abramsky in [4]. This characterization is couched in logical terms, and is an impressive byproduct of Abramsky’s “theory of domains in logical form” programme [5]. More precisely, Abramsky shows that the domain logic for transition systems synthesized in [2] characterizes the finitary bisimulation for all transition systems, i.e., that two processes in any transition system are related by the finitary bisimulation iff they satisfy the same formulae in the finitary version of the domain logic for transition systems. In many ways, Abramsky’s logical characterization of the finitary bisimulation can be seen as the counterpart of the modal characterizations for bisimulation-like relations presented in, e.g., [22, 12, 30].

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. The existence of observation-independent, behavioural characterizations 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 particular, as transition systems abstract from the operational semantics of many process description languages, we believe that it would be worthwhile to establish general bisimulation-like characterizations of the finitary bisimulation for interesting classes of such structures. The availability of this type of results would imply, for instance, that, when establishing full abstraction results for a particular process description language, it would be sufficient to identify the kind of transition system giving an operational semantics to the chosen language, and check what form the finitary bisimulation for that type of transition system takes. One could then proceed to compare the appropriate explicit characterization of this behavioural preorder with the denotational ordering on processes.

1.1 Results

This study presents a collection of observation independent, bisimulation-like characterizations of the finitary bisimulation for several classes of labelled transition systems, including those that commonly arise in giving operational semantics to process description languages. First of all, we present a behavioural characterization of the finitary bisimulation for arbitrary transition systems (cf. Thm. 3.2). This result may be seen as the behavioural counterpart of Abramsky’s logical characterization theorem [4, Thm. 5.5.8]. We offer two independent proofs of this characterization theorem. The first relies on Abramsky’s logical characterization result in terms of the domain logic for transition systems; the second is purely operational, and is based on a generalization of a beautiful argument due to Hennessy [10]. This first behavioural characterization applies, e.g., to transition systems with an uncountable action set like those that arise in timed process calculi which postulate the positive real numbers as their time domain. (Cf., e.g., Wang’s TCCS [33].)

We then concentrate our attention on transition systems over a countable action set. For several classes of such transition systems (viz. the class of all such transition systems, the class of those which have bounded convergent sort, the sort-finite transition systems and those that are image finite [12] and weakly finite branching), we provide customized, and more informative, versions of the general behavioural characterization offered by Thm. 3.2. In particular, for the important class of sort-finite transition systems we are able to present a sharpened version of a behavioural characterization result first proven by Abramsky in [4, Propn. 6.13].

We hope that this taxonomy of characterizations of the finitary bisimulation will be useful for researchers interested in full abstraction results for process description languages.

1.2 Outline of the Paper

We conclude this introduction with a brief road-map to the contents of this study. We begin by presenting the basic notions from process theory and Abramsky’s domain logic for transition systems in Sect. 2. Section 3 is the côre of the paper, and is entirely devoted to a taxonomy of behavioural characterizations of the finitary bisimulation for various classes of transition systems. The characterization of ≲^{F} for arbitrary transition systems is the subject of Sect. 3.1. Section 3.2 is devoted to behavioural characterizations of the finitary bisimulation for transition systems over a countable action set. Apart from the class of all such transition systems, we also deal with transition systems that have bounded convergent sort, sort-finite transition systems and the image finite ones that are also weakly finite branching.

2 Preliminaries

In this section we present the basic notions from process theory and Abramsky’s domain logic for transition systems that will be needed in the remainder of this study.

2.1 Labelled Transition Systems and Prebisimulation

We begin by reviewing a variation on the model of labelled transition systems [18, 28] that takes divergence information into account, and abstracts from the operational semantics of many concurrent calculi. We refer the interested readers to, e.g., [13, 10, 22, 32] for motivation and more information on (variations on) this semantic model for reactive systems.

Definition 2.1 (Labelled Transition Systems with Divergence) 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 definitely converges”, iff it is not the case that p ↑. Intuitively, the fact that a process p definitely converges means that the initial behaviour of p 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 [4], we say that an lts is

image finite iff derivatives(p, a) is finite for every p ∈ Proc and a ∈ Act
sort-finite iff sort(p) is finite for every p ∈ Proc
finite branching iff {(a, q) | p →^{a} q} is finite for every p ∈ Proc
weakly finite branching iff for every p ∈ Proc, if p ↓ then {(a, q) | p →^{a} q} is finite
weakly initials finite iff for every p ∈ Proc, if p ↓ then initials(p) is finite.

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 [13, 22, 10, 32] (also known as partial bisimulation [4]).

Definition 2.2 (Prebisimulation) 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.

The relation ≲ is a preorder over Proc based on a variation on bisimulation equivalence [25, 24]. Intuitively, p ≲ q if q’s behaviour is at least as specified as that of p, and p and q can simulate each other when restricted to the part of their behaviour that is fully specified. A divergent process p that, like the synchronization tree Ω, has no outgoing transition is a minimal element with respect to ≲, and intuitively corresponds to a process whose behaviour is totally unspecified — essentially an operational version of the bottom element ⊥ in Scott’s theory of domains (cf., e.g., the references [29, 27, 31] for information on domain theory).

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

≲_{0} =^{Δ} Rel(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, for every i ≥ 0,

a^{ω} ≲_{i} \underbrace{a : ⋯: a :}_{i-times} 𝕆 .

Therefore q ≲_{ω} p does instead hold.

Remark: Although the relations ≲ and ≲_{ω} have been defined over a given lts, we often want to use them to compare processes from different lts’s; for example, we shall often compare processes in an lts with finite synchronization trees. This can be done in standard fashion by forming the disjoint union of the two transition systems, and then using ≲ or ≲_{ω} on the resulting lts. In the sequel, this will be done without further comment.

In this paper, we shall be interested in studying the “finitely observable”, or finitary, part of the bisimulation in the sense of, e.g., [9, 10]. The following definition is from [4]. (The interested reader is invited to consult the aforementioned references for discussion and motivations.)

Definition 2.3 Let (Proc, Act, →, ↑) be an lts. The finitary bisimulation preorder ≲^{F} over Proc is defined thus:

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, in general, strict. The interested reader is referred to [4] for a wealth of examples distinguishing these preorders, and a very deep analysis of their general relationships and properties. Here we just discuss an instructive example from [4, Page 191] showing that the preorder ≲_{ω} (and a fortiori ≲) makes distinctions based on infinite observations.

Example: Consider the synchronization trees p and q given by:

p =^{Δ} a : (∑_{n∈ω} b_{n} : 𝕆 + Ω) + Ω  (1)
q =^{Δ}  ∑_{n∈ω} a : (∑_{m∈ω−{n}} b_{m} : 𝕆 + Ω) + Ω .  (2)

It is easy to see that p ≴_{2} q. We shall now argue that p ≲^{F} q does instead hold. To this end, let t be a finite synchronization tree such that t ≲ p. Because of the definition of the bisimulation preorder, this implies that the following conditions are met:

1. t ↑;

2. initials(t) = {a};

3. for every t′ such that t →^{a} t′, t′ ≲ ∑_{n∈ω} b_{n} : 𝕆 + Ω.

It is not too difficult to see that for every finite synchronization tree u,

u ≲ ∑_{n∈ω} b_{n} : 𝕆 + Ω implies u ≲ ∑_{m∈ω−{n}} b_{m} : 𝕆 + Ω, for some n ∈ ω.

This follows because any finite synchronization tree u such that u ≲ ∑_{n∈ω} b_{n} : 𝕆 + Ω is divergent, and its set of initial actions must be a finite subset of {b_{n} | n ∈ ω}.

Collecting the above observations it is immediate to see that t ≲ q also holds. □

To our mind, the above example demonstrates in an explicit and instructive way the mismatch between the finitary part of the bisimulation preorder and the preorder ≲_{ω}. Intuitively, the preorder ≲_{ω} is based on observations of finite depth. However, in the presence of (weakly) infinite branching processes like p and q above, this preorder can make distinctions based on observations of infinite width. As outlined in the above example, no observation of finite depth and width can differentiate the processes defined in (1) and (2). (The interested reader may wish to consult the reference [1] for illuminating discussions on the issue of finite, and infinite, depth and width in experiments in the setting of applicative, non-deterministic programs.)

Abramsky’s Domain Logic for Transition Systems

We now review the basic definitions and results on Abramsky’s domain logic for transition systems that will be useful in this study. We shall follow the presentation of the logic given in [2]; the interested reader is referred to that reference for a detailed explanation of the logic, its origins, semantics and proof theory.

Abramsky’s (finitary) domain logic for transition systems L_{ω} (over a set of actions Act) is a two-sorted language with sorts π (process) and κ (capability). We write L_{ωπ} (respectively, L_{ωκ}) for the class of formulae of sort π (respectively, κ), which are defined inductively as follows:

\frac{\{φ_{i} ∈ L_{ωσ}\}_{i∈I}}{⋀_{i∈I} φ_{i}, ⋁_{i∈I} φ_{i} ∈ L_{ωσ}}  \frac{a ∈ Act, φ ∈ L_{ωπ}}{a(φ) ∈ L_{ωκ}}  \frac{φ ∈ L_{ωκ}}{□φ, ♢φ ∈ L_{ωπ}}

where I is a finite index set, and σ ∈ {π, κ}. As usual, we write true =^{Δ} ⋀_{i∈∅} φ_{i} and

false =^{Δ} ⋁_{i∈∅} φ_{i}.

The modal depth of a formula φ, notation md(φ), is the non-negative integer giving the maximum nesting of occurrences of the modal operators □ and ♢ in it. Its sort, notation sort(φ), is the finite set of actions mentioned in φ.

For each A ⊆ Act and non-negative integer n:

L_{ω}^{(A,n)} =^{Δ} {φ ∈ L_{ω} | md(φ) ≤ n and sort(φ) ⊆ A} .

Given an lts (Proc, Act, →, ↑), we define:

Cap =^{Δ} {⊥} ∪ (Act × Proc) (the set of capabilities)
C(p) =^{Δ} {⊥ | p ↑} ∪ {⟨a, q⟩ | p →^{a} q} (the set of capabilities of process p) .

The satisfaction relations

⊧_{π} ⊆ Proc × L_{ωπ} and
⊧_{κ} ⊆ Cap × L_{ωκ}

are now defined thus (σ ∈ {π, κ}, w ∈ Proc ∪ Cap):

w ⊧_{σ} ⋀_{i∈I} φ_{i} =^{Δ} ∀i ∈ I. w ⊧_{σ} φ_{i}
w ⊧_{σ} ⋁_{i∈I} φ_{i} =^{Δ} ∃i ∈ I : w ⊧_{σ} φ_{i}
p ⊧_{π} □φ =^{Δ} ∀c ∈ C(p). c ⊧_{κ} φ
p ⊧_{π} ♢φ =^{Δ} ∃c ∈ C(p) ∪ {⊥}. c ⊧_{κ} φ
c ⊧_{κ} a(φ) =^{Δ} c = ⟨a, q⟩ and q ⊧_{π} φ .

For F ⊆ L_{ω} and process p, we write F(p) for the set of (process) formulae in the set F satisfied by p. In what follows, we shall always omit sort information from (sets of) formulae, and satisfaction relations.

As shown by Abramsky in his thesis [2], the logic L_{ω} is a powerful tool in the study of the finitary bisimulation preorder ≲^{F}. In particular, Abramsky shows the following key characterization theorem (see [2, Thm. 5.5.8]):

Theorem 2.4 (Characterization Theorem for L_{ω}) For p, q ∈ Proc in any transition system,

p ≲^{F} q ⇔ L_{ω}(p) ⊆ L_{ω}(q) .

The above seminal result will be a major tool in this study. In what follows, we shall also have some use for the following observation, which is due to Abramsky (cf., e.g., the proof of Propn. 5.5.12 in [2]).

Fact 2.5 Let A ⊆ Act be a finite set of actions. Then, for every non-negative integer n, L_{ω}^{(A,n)} is finite up to logical equivalence.

3 Behavioural Characterizations of the Finitary Bisimulation

The definition of the finitely observable part of the bisimulation preorder given in Def. 2.3 is rather indirect. Rather like the original definition of De Nicola and Hennessy’s testing equivalence [11], it just says that, in order for p ≲^{F} q to hold, every observation that is possible of p should also be possible of q, where we identify the set of observations with that of finite synchronization trees. Definitions of behavioural preorders like the one in Def. 2.3 are, albeit very natural and intuitively appealing, quite difficult to work with. For this reason, it is useful to have alternative, observation-independent characterizations for them. Again using the analogy with the testing equivalences, the alternative characterizations of these relations provided in [11] have proven to be indispensable tools in the development of their theory and practice.

Abramsky’s logical characterization of the finitary bisimulation (cf. Thm. 2.4) 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 [22, 12]. 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., [4, Propn. 6.13]. There Abramsky shows that in any sort-finite lts that satisfies his axiom scheme of bounded nondeterminacy (BN) (cf. [2, Page 114]), the finitary bisimulation coincides with ≲_{ω}. In this study, building on Abramsky’s work, we shall present several bisimulation-like characterizations of the finitary bisimulation for various classes of 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.11.)

3.1 A General Behavioural Characterization

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 in any transition system, p ⊏_{∼}_{n+1}^{A} q implies p ⊏_{∼}_{n}^{A} q.

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

implies p ⊏_{∼}_{n}^{A} q

Proof: The proofs of all the statements are routine by mathematical induction on n. Here we only remark that, in the proof of the inductive step for statement 3, the following simple observation is used:

if p ⊏_{∼}_{n+1}^{B} q, p ↓, q ↓ and initials(p) ⊆ A ⊆ B, then initials(q) ⊆ A.
□

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 preorder ≲_{ω}, defined on page 6.

Intuitively, p ⊏_{∼}_{ω}^{A} q holds for two processes p and q iff there is no observation, in the sense of [3], 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 example on page 7. A possibly even more striking example of the rôle played by finite width in observations, and of the weakness of ≲^{F} over infinite branching processes, is the following:

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} : 𝕆  (3)
q =^{Δ} p + Ω .  (4)

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.

The moral of the above example is that, for lts’s that are not weakly initials finite, observations based on finite synchronization trees cannot, in general, be used to test the convergence of a process that, like p above, can perform infinitely many distinct initial actions. As shown by the technical results to follow, this is the reason for the presence of the non-standard test on the set of initial actions of a process in clause (2) of the definition of the preorder ⊏_{∼}_{n+1}^{A}. □

Remark: The reader familiar with Apt and Plotkin’s arguments for the failure of continuous semantics for random assignment presented in [7, pp. 741–747] might have noticed that the example we have just discussed is closely related to the one used ibid. to demonstrate the mismatch between operational and continuous denotational semantics for countable nondeterminism.

Apt and Plotkin show that in any ‘reasonable’ continuous semantics the programs

P =^{Δ} x:=?;while x> 0 do x:=x−1 od

and

P or (while true do skip od)

where x:=? denotes the random assignment of a non-negative integer to the variable x, and or stands for nondeterministic choice, are necessarily identified, even though the former is guaranteed to terminate in a state where x has value 0, whereas the latter does not. The point is that, due to the countable nondeterminism in the computation tree for program P, no finite observation can detect the possible infinite loop in the second program.

Our aim is to prove:

Theorem 3.2 For p, q ∈ Proc in any transition system,

p ≲^{F} q ⇔ p ⊏_{∼}_{ω}^{fin} q .

Our proof of this general behavioural characterization theorem for the finitary bisimulation relies on the logical formulation of this relation given by Thm. 2.4. The key step in the proof is presented in the following result, that gives a logical characterization of the preorders ⊏_{∼}_{n}^{A} when the set of actions A is finite.

Proposition 3.3 Let (Proc, Act, →, ↑) be an lts. For every A ⊆_{fin} Act, n ≥ 0,

p ⊏_{∼}_{n}^{A} q ⇔ L_{ω}^{(A,n)}(p) ⊆ L_{ω}^{(A,n)}(q) .

Proof: We prove the two implications separately.

• ‘If Implication’. We prove the contrapositive statement; namely, we show that, for all p, q ∈ Proc, A ⊆_{fin} Act, n ≥ 0,

p ⊏̸_{∼}_{n}^{A} q ⇒ ∃φ ∈ L_{ω}^{(A,n)}(p) \ L_{ω}^{(A,n)}(q) .

The proof is by mathematical induction on n, and the basis of the inductive argument is vacuously true. For the inductive step, assume that p ⊏̸_{∼}_{n+1}^{A} q. By the definition of ⊏_{∼}_{n+1}^{A}, one of the following cases must arise:

1. there exist a ∈ A and p′ ∈ Proc such that p →^{a} p′, and, for every q′ ∈ derivatives(q, a),

p′ ⊏̸_{∼}_{n}^{A} q′; or

2. initials(p) ⊆ A, p ↓ and (a) q ↑ or

(b) initials(q) ⊈ A; or

3. initials(p) ⊆ A, initials(q) ⊆ A, p ↓, q ↓ and there exist a ∈ A and q′ ∈ Proc such that q →^{a} q′, and, for every p′ ∈ derivatives(p, a), p′ ⊏̸_{∼}_{n}^{A} q′.

In each case, we shall show how to construct a formula φ ∈ L_{ω}^{(A,n+1)}(p) \ L_{ω}^{(A,n+1)}(q).

1. Assume that there exist a ∈ A and p′ ∈ Proc such that p →^{a} p′, and, for every q′ ∈ derivatives(q, a), p′ ⊏̸_{∼}_{n}^{A} q′. The inductive hypothesis now gives that, for every q′ ∈ derivatives(q, a), there exists a formula φ_{q′} ∈ L_{ω}^{(A,n)}(p′) \ L_{ω}^{(A,n)}(q′). Consider the set of formulae {φ_{q′} | q′ ∈ derivatives(q, a)} ⊆ L_{ω}^{(A,n)}. As A is a finite set of actions, Fact 2.5 gives that, up to logical equivalence, there are only finitely many distinct formulae in {φ_{q′} | q′ ∈ derivatives(q, a)}, say φ_{1}, …, φ_{k}. We now define

φ =^{Δ} ♢a(⋀_{i=1}^{k} φ_{i}) .

By construction, φ is a formula in L_{ω}^{(A,n+1)}. It is now a simple matter to show that p satisfies φ, while q does not.

2. Assume that initials(p) ⊆ A, p ↓ and either q ↑ or initials(q) ⊈ A. As A is a finite set, so is initials(p). We now define:

φ =^{Δ} □ ⋁ {a(true) | a ∈ initials(p)} .

By construction, φ is a formula in L_{ω}^{(A,n+1)}. It is a simple matter to show that, as p ↓, p satisfies φ. On the other contrary, q does not satisfy φ. In fact, if q ↑, then ⊥ ∈ C(q) and ⊥ |̸= ⋁ {a(true) | a ∈ initials(p)}. Otherwise, there exists an action b ∈ initials(q)\A. Thus, for some q′, ⟨b, q′⟩ is a capability of q. As initials(p) is a subset of A, the capability ⟨b, q′⟩ does not satisfy the capability formula ⋁ {a(true) | a ∈ initials(p)}.

3. Assume that initials(p) ⊆ A, initials(q) ⊆ A, p ↓, q ↓ and there exist a ∈ A and q′ ∈ Proc such that q →^{a} q′, and, for every p′ ∈ derivatives(p, a), p′ ⊏̸_{∼}_{n}^{A} q′. By the inductive hypothesis, for every p′ ∈ derivatives(p, a), there exists a formula φ_{p′} ∈ L_{ω}^{(A,n)}(p′) \ L_{ω}^{(A,n)}(q′). Consider the collection of formulae

{φ_{p′} | p′ ∈ derivatives(p, a)} ⊆ L_{ω}^{(A,n)} .

As A is a finite set of actions, Fact 2.5 gives that, up to logical equivalence, there are only finitely many distinct formulae in {φ_{p′} | p′ ∈ derivatives(p, a)}, say φ_{1}, …, φ_{k}. We now define

φ =^{Δ} □(a(⋁_{i=1}^{k} φ_{i}) ∨ ⋁ {b(true) | b ∈ initials(p) − {a}}) .

Note that, as initials(p) ⊆ A ⊆_{fin} Act, φ is a formula in L_{ω}^{(A,n+1)}. It is now a simple matter to show that p satisfies φ, while q does not.

This completes the inductive argument and the proof of the ‘if’ implication.

• ‘Only If Implication’. We prove that, for all n ≥ 0, p, q ∈ Proc,

p ⊏_{∼}_{n}^{A} q ⇒ ∀φ ∈ L_{ω}^{(A,n)}. (p ⊧ φ implies q ⊧ φ) .

This we proceed to show by mathematical induction on n. The base case is trivially seen to hold because every formula in L_{ω}^{(A,0)} is logically equivalent to either true or false.

For the inductive step, assume that p ⊏_{∼}_{n+1}^{A} q and that p ⊧ φ ∈ L_{ω}^{(A,n+1)}. We show that q ⊧ φ by a further structural induction on φ. Indeed, in light of [2, Lem. 5.5.2], it is sufficient to prove the claim for a specific class of formulae, viz. the normal forms defined in [2, Def. 5.5.1]. These are the formulae given by the following inductive definition:

1. If I is a finite index set and, for every i ∈ I, φ_{i} is a normal form, then ⋀_{i∈I} φ_{i} and ⋁_{i∈I} φ_{i} are normal forms;

2. if a ∈ Act and φ is a normal form, then ♢a(φ) is a normal form; and

3. If I is a finite index set, {a_{i} | i ∈ I} ⊆ Act and, for every i ∈ I, φ_{i} is a normal form, then □ ⋁_{i∈I} a_{i}(φ_{i}) is a normal form. (Abramsky’s definition of normal forms requires that the actions a_{i} be pairwise distinct. In the following, we shall not need this restriction, and we have decided to omit it for the sake of simplicity.)

We only consider the two interesting cases.

– Assume that p ⊧ ♢a(φ) ∈ L_{ω}^{(A,n+1)}. By the definition of the satisfaction relation and the fact that ⊥ |̸= a(φ), this is because there exists c ∈ C(p) such that c ⊧ a(φ). This capability must be of the form ⟨a, p′⟩ for some p′ ⊧ φ, i.e., p →^{a} p′ ⊧ φ for some p′. As

a ∈ A and p ⊏_{∼}_{n+1}^{A} q, it follows that q →^{a} q′ and p′ ⊏_{∼}_{n}^{A} q′ for some q′. As φ ∈ L_{ω}^{(A,n)}, we

may now apply the inductive hypothesis to infer that q′ ⊧ φ, from which q ⊧ ♢a(φ) follows immediately.

– Assume that p ⊧ □ ⋁_{i∈I} a_{i}(φ_{i}) ∈ L_{ω}^{(A,n+1)}. Then, for every c ∈ C(p),

c ⊧ ⋁_{i∈I} a_{i}(φ_{i}) .

Note, first of all, that this implies that p ↓, because otherwise ⊥ ∈ C(p) and ⊥ |̸= ⋁_{i∈I} a_{i}(φ_{i}).

Assume now that p →^{a} p′, for some action a ∈ Act and process p′. As ⟨a, p′⟩ ∈ C(p), it follows that, for some index i_{a,p′} ∈ I, a = a_{i_{a,p′}} and p′ ⊧ φ_{i_{a,p′}}. In particular,

this implies that initials(p) ⊆ {a_{i} | i ∈ I} ⊆ A. Therefore, as p ⊏_{∼}_{n+1}^{A} q, p ↓ and initials(p) ⊆ A, we have that:

∗ q ↓,

∗ initials(q) ⊆ A, and

∗ for every a ∈ A, q′ ∈ Proc, whenever q →^{a} q′, then p →^{a} p′ for some p′ such that

p′ ⊏_{∼}_{n}^{A} q′.

As q ↓, it follows that ⊥ ∉ C(q). Let now ⟨a, q′⟩ ∈ C(q). Then a ∈ A, q →^{a} q′ and p →^{a} p′ ⊏_{∼}_{n}^{A} q′ for some p′. As a = a_{i_{a,p′}} and p′ ⊧ φ_{i_{a,p′}}, an application of the inductive hypothesis gives that ⟨a, q′⟩ ⊧ a_{i_{a,p′}} (φ_{i_{a,p′}}). From this observation, q ⊧ □ ⋁_{i∈I} a_{i}(φ_{i}) follows immediately.

This completes the proof of the ‘only if’ implication.

The proof of the theorem is now complete. □

Remark: As witnessed by the proof of the ‘if implication’ in the statement of the above result, for each finite set of actions A we can construct a formula φ_{A} with the property that, for every p ∈ Proc:

p ⊧ φ_{A} ⇔ p ↓ and initials(p) ⊆ A .

Such a formula is simply defined thus:

φ_{A} =^{Δ} □ ⋁ {a(true) | a ∈ A} .

Note, however, that, if Act is countably infinite, there is no formula φ_{↓} in L_{ω} which is satisfied exactly by all the convergent processes. In fact, using such a formula we should be able to distinguish the behaviour of the synchronization trees p and q on page 11, which are related by the finitary bisimulation preorder. (The obvious candidate for such a formula φ_{↓} is □ ⋁ {a(true) | a ∈ Act}, which uses infinite disjunction if Act is countably infinite.) In other words, using the finitary domain logic we can only test convergence for processes that have a finite set of initial actions. This is in agreement with the operational considerations prompted by our discussion of the example on page 11.

By contrast with the above considerations, such a formula φ_{↓} can be constructed in the version of the domain logic for transition systems presented by Abramsky in [4]. The satisfaction relation for the □ and ♢ modalities is ibid. given thus:

p ⊧_{π} □φ =^{Δ} p ↓ and ∀c ∈ C(p). c ⊧_{κ} φ
p ⊧_{π} ♢φ =^{Δ} ∃c ∈ C(p) : c ⊧_{κ} φ

With this interpretation, the formula □true is satisfied exactly by all the convergent processes. In light of the example on page 11, the presence of such a formula invalidates Thm. 5.8 on page 191 of [4], that states the logical characterization theorem for the finitary bisimulation in terms of the version of the domain logic offered ibidem.

Using Propn. 3.3, we can now easily prove the promised general behavioural characterization theorem for ≲^{F}.

Proof of Theorem 3.2: Let (Proc, Act, →, ↑) be any lts. Let p, q ∈ Proc. Then:

p ≲^{F} q ⇔ L_{ω}(p) ⊆ L_{ω}(q)  (Thm. 2.4)
⇔ ∀A ⊆_{fin} Act, n ≥ 0. L_{ω}^{(A,n)}(p) ⊆ L_{ω}^{(A,n)}(q)
⇔ ∀A ⊆_{fin} Act, n ≥ 0. p ⊏_{∼}_{n}^{A} q  (Propn. 3.3)
⇔ p ⊏_{∼}_{ω}^{fin} q  (Definition of ⊏_{∼}_{ω}^{fin})
□

3.1.1 An Operational Proof of the Characterization Theorem

The use of Abramsky’s domain logic in establishing the general characterization of the finitary bisimulation offered in Thm. 3.2 has, we believe, led to an elegant proof of that result based on a logical view of the preorders ⊏_{∼}_{n}^{A}, for every finite set of actions A and non-negative integer n. In addition, it has allowed us to discuss the inequivalence of the two formulations of the domain logic L_{ω} given by Abramsky in the references [2, 4]. We trust that this remark will be of independent interest to researchers who want to apply the domain logic for transition systems in their studies.

An alternative proof of Thm. 3.2 can, however, be given by using purely operational considerations. As the type of argument used in this alternative proof recurs, sometimes incorrectly (cf. [10] and the remarks in [4, page 212]), in several papers on process theory for specific classes of transition systems (cf., e.g., [15, 16]), we find it interesting to present its general version below.

Let (Proc, Act, →, ↑) be an arbitrary lts. We note, first of all, that the finitary bisimulation over such an lts 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 .  (5)

This is an immediate consequence of the fact that, for every finite synchronization tree t and process p,

t ≲ p ⇔ t ≲^{F} p .

A binary relation over processes that enjoys property (5) is usually called finitary or finitely approximable [10, 6]. It is immediate to see that two finitary relations that coincide over ST(Act) × Proc do, in fact, coincide over the whole of Proc. To prove Thm. 3.2, it is therefore sufficient to show the following two statements:

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

(S2) The preorder ⊏_{∼}_{ω}^{fin} is finitary, i.e.,

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

We now proceed to prove these two statements in turn. In what follows, 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}[+Ω]) =^{Δ} 1 + sup {ht(t_{i}) | i ∈ I} .

Proof of Statement S1: We show that, for every t ∈ ST(Act), p ∈ Proc,

t ≲ p iff t ⊏_{∼}_{ω}^{fin} p.

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 .

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) and uses Propn. 3.1(2)-(3). □

We now proceed to prove statement S2. To this end, we shall need a few 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 (3) and (4), 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 nonnegative integer n, the set of synchronization trees {p^{(A,n)} | p ∈ Proc} is finite. Therefore p^{(A,n+1)} is a finite synchronization tree even when 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 S2 above, i.e., that the preorder ⊏_{∼}_{ω}^{fin} is finitary.

Proof of Statement S2: 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 .  (6)

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 (Lem. 3.4). As p^{(A,n)} is a finite synchronization tree, it follows that p ⊏_{∼}_{n}^{A} p^{(A,n)} ⊏_{∼}_{ω}^{fin} p (Statement S1). Using (6), 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. □

The operational proof of Thm. 3.2 is now complete.

3.2 Transition Systems over a Countable Action Set

The behavioural characterization of the finitary bisimulation presented in Thm. 3.2, like the logical one given by Abramsky, applies to arbitrary lts’s. For example, it can be used as an observation-independent version of ≲^{F} over lts’s with an uncountable action set. This means, in particular, that such a characterization applies to the bisimulation preorder for, e.g., timed calculi which postulate an uncountable time domain like, e.g., Wang’s TCCS [33].

However, the lts’s giving operational semantics to most standard process calculi, e.g. those for ACP [8], CCS [24] and CSP [14], have countable action sets. For such transition systems, it is possible to give an alternative characterization of the preorder ≲^{F} which is, in many ways, easier to work with than the one provided by Thm. 3.2. This we now proceed to present.

In the remainder of this study, we shall assume that the set of actions Act is countable. Let (Proc, Act, →, ↑) be an lts with Act = {a_{1}, a_{2}, …} a countable action set. For

every n ≥ 0, we write Act_{n} for the set of actions {a_{1}, …, a_{n}}. We now define:

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

(2) If initials(p) ⊆ Act_{n+1} and p ↓ then (2.1) initials(q) ⊆ Act_{n+1} and q ↓

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

Finally, for all p, q ∈ Proc,

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

Proposition 3.5 Let (Proc, Act, →, ↑) be an lts with Act a countable action set. Then:

1. The relations ⊏_{∼}_{n} (n ≥ 0) and ⊏_{∼}_{ω} are preorders.

2. For all p, q ∈ Proc, n ≥ 0, if p ⊏_{∼}_{n+1} q, then p ⊏_{∼}_{n} q.

The reader familiar with the literature on value-passing versions of Milner’s CCS (cf., e.g., [13, 15, 16]) might have noticed that the above definitions are inspired by the characterizations of the finitary bisimulation presented in the aforementioned references. The main difference in the definition we present is the presence of the condition on the set of initial actions of process p in clause (2) of the definition of ⊏_{∼}_{n+1}. The significance of this change is witnessed by the example on page 11.

Definition 3.6 Let Act = {a_{1}, a_{2}, …} be a countable action set. For every A ⊆_{fin} Act, we define

ı(A) =^{Δ} min {n | A ⊆ Act_{n}} .

Theorem 3.7 For p, q ∈ Proc in any transition system over a countable action set Act,

p ≲^{F} q ⇔ p ⊏_{∼}_{ω} q .

Proof: In view of Thm. 3.2, it is sufficient to prove that, for all p, q ∈ Proc,

p ⊏_{∼}_{ω}^{fin} q ⇔ p ⊏_{∼}_{ω} q .

This we now proceed to show by establishing the two implications separately.

• ‘Only If Implication’. We prove that, for all p, q ∈ Proc and n ≥ 0,

p ⊏_{∼}Act_{n}_{n} q ⇒ p ⊏_{∼}_{n} q

from which the claim follows immediately.

The above statement is proven by mathematical induction on n. The basis of the inductive argument is trivial as ⊏_{∼}_{0} is the universal relation over Proc. For the inductive step, assume that p ⊏_{∼}Act_{n+1}_{n+1} q. It is now a simple matter to show that p ⊏_{∼}_{n+1} q, using the inductive hypothesis and Propn. 3.1(2)-(3).

• ‘If Implication’. It is sufficient to prove that, for every finite set of actions A, n ≥ 0,

p, q ∈ Proc,

p ⊏_{∼}_{ı(A)+n} q ⇒ p ⊏_{∼}_{n}^{A} q .

The easy proof by mathematical induction on n is left to the reader.

The proof of the theorem is now complete. □

Remark: The characterization of the finitary bisimulation presented in the above theorem applies, for instance, to the versions of Milner’s SCCS [23] considered in [10, 4]. To the best of our knowledge, this is the first explicit behavioural characterization of the finitary bisimulation for the class of lts’s denotable by SCCS processes presented in the literature. Indeed, as remarked in [4, page 212], the characterization of ≲^{F} for SCCS in [10] was obtained under the implicit, and incorrect, assumption that SCCS processes are sort-finite.

The characterizations of the finitary bisimulation that we have so far presented apply to any lts with arbitrary or countable action sets. However, it is often the case that the lts’s specified by standard process description languages satisfy some sort of finiteness conditions, e.g., that they are weakly finite branching or sort-finite. We shall now provide more specific characterizations of ≲^{F} for several interesting classes of lts’s.

3.2.1 Transition Systems with Bounded Convergent Sort

We begin by studying a, to the best of our knowledge novel, class of lts’s, viz. those with bounded convergent sort (see Def. 3.8). Apart from its intrinsic interest, the characterization of the finitary bisimulation that we shall offer for this kind of lts’s will pave the way to a sharpened version of Propn. 6.13 in [4].

Definition 3.8 Let (Proc, Act, →, ↑) be an lts. For every p ∈ Proc, n ≥ 0, we define:

Csort(p, n) =^{Δ} ⋃ {initials(q) | q ↓ and there exists σ ∈ Act^{∗} of length at most n: p →^{σ} q}

We say that an lts has bounded convergent sort iff Csort(p, n) is finite for all p ∈ Proc and n ≥ 0.

Intuitively, in an lts with bounded convergent sort, if we unfold the behaviour of a process p and cut the resulting synchronization tree at depth n, we obtain a synchronization tree whose convergent processes have capabilities drawn from a finite set of actions. Of course, every lts that is finite branching has a fortiori bounded convergent sort. However, there are lts that have bounded convergent sort, but are not finite branching. For example, the synchronization tree

t =^{Δ}  ∑_{i≥1} \underbrace{a : ⋯: a :}_{i-times} 𝕆  (7)

is sort-finite, and therefore has bounded convergent sort, but it is infinite branching. An example of an lts which has bounded convergent sort and has an infinite sort is

p_{0} →^{a_{1}} p_{1} →^{a_{2}} p_{2} →^{a_{3}} ⋯  (8)

where each process p_{i} (i ≥ 0) is convergent. This lts is, up to isomorphism, the one associated with the CCS process:

All-Actions =^{def} a_{1}.(All-Actions[next])

where next is the relabelling mapping each action a_{i} to its successor a_{i+1} (i ≥ 1).

In general, the condition of weak finite branching is incomparable with that of having bounded convergent sort. The synchronization tree given in (7) has bounded convergent sort, but is not weakly finite branching. An example of a weakly finite branching synchronization tree which does not have bounded convergent sort is the following:

u =^{Δ} (∑_{i≥0} a : b_{i} : 𝕆) + Ω

where we assume that the actions b_{i} are pairwise distinct. This synchronization tree is, up to isomorphism, the one associated with the CCS process:

X =^{def} X[f] + a.b_{0}.Nil

where f is the relabelling mapping each action b_{i} to its successor b_{i+1} (i ≥ 0), and leaving a fixed.

Both the codings in CCS (with finite summation) of sort-infinite synchronization trees that we have presented make use of infinite relabellings, i.e., relabellings that change the nature of infinitely many actions. This is unavoidable because, as first observed by Abramsky [3, 4], CCS with finite relabellings can only describe sort-finite, and thus convergent sort bounded, lts’s. CCS with infinite relabellings, but only guarded recursion, can only specify finite branching, and thus convergent sort bounded, processes. As (8) shows, these processes need not be sort-finite.

After having discussed the bounded convergent sort condition, we now proceed to present a characterization of the finitary bisimulation for this class of lts’s.

Let (Proc, Act, →, ↑) be an lts with Act = {a_{1}, a_{2}, …} a countable action set. We now define:

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

(2) If p ↓ then (2.1) q ↓

(2.2) ∀a ∈ Act_{n+1}, q′ ∈ Proc. q →^{a} q′ ⇒ ∃p′ : p →^{a} p′ and p′ ⊏_{≈}_{n} q′ .

Finally, for all p, q ∈ Proc,

p ⊏_{≈}_{ω} q =^{Δ} ∀n ≥ 0. p ⊏_{≈}_{n} q .

Proposition 3.9 Let (Proc, Act, →, ↑) be an lts with Act a countable action set. Then:

1. The relations ⊏_{≈}_{n} (n ≥ 0) and ⊏_{≈}_{ω} are preorders.

2. For all p, q ∈ Proc, n ≥ 0, if p ⊏_{≈}_{n+1} q, then p ⊏_{≈}_{n} q.

The definition of the preorder ⊏_{≈}_{ω} is very similar to that of the preorder ≲_{ω} given on page 6. The only difference consists in the set of actions an observer, in the sense of [3], is allowed to use in experiments of depth n. The requirement that the actions be drawn from the set Act_{n}, which is finite, guarantees that the resulting experiments be of finite width as well as depth. Note that, unlike in the definition of the preorder ⊏_{∼}_{n+1}, in clause (2) above we need not require that initials(p) is contained in Act_{n+1}. As the proof of the following result shows, this requirement is redundant for convergent sort bounded processes. Indeed, the requirement that initials(p) ⊆ Act_{n+1} for some n, was needed to ensure the testability of the convergence of a process. If the lts under consideration has bounded convergent sort, then every convergent process can only initially perform finitely many distinct actions. As argued in the remark on page 14, convergence of these processes can always be detected using finite observations.

Theorem 3.10 For p, q ∈ Proc in any transition system over a countable action set Act which has bounded convergent sort,

p ≲^{F} q ⇔ p ⊏_{≈}_{ω} q .

Proof: Consider a transition system over a countable action set Act which has bounded convergent sort. In view of Thm. 3.7, it is sufficient to prove that, for all p, q ∈ Proc,

p ⊏_{∼}_{ω} q ⇔ p ⊏_{≈}_{ω} q .

We show the two implications in the above statement separately.

• ‘Only If Implication’. To prove that, for all p, q ∈ Proc,

p ⊏_{∼}_{ω} q ⇒ p ⊏_{≈}_{ω} q .

it is sufficient to show that, for all p, q ∈ Proc, n ≥ 0:

p ⊏_{∼}_{ı(Csort(p, n))+n} q ⇒ p ⊏_{≈}_{n} q .  (9)

Note that ı(Csort(p, n)) is a well-defined non-negative integer because, as the lts has bounded convergent sort, Csort(p, n) is a finite set of actions. To ease readability, throughout the proof of (9) we use ı(p, n) as a shorthand for ı(Csort(p, n)). We prove statement (9) by mathematical induction on n. The basis of the induction is immediate because ⊏_{≈}_{0} is the universal relation. For the inductive step, we assume that p ⊏_{∼}_{ı(p,n+1)+n+1} q, and prove that p ⊏_{≈}_{n+1} q holds. To this end, it is sufficient to show that the defining clauses of ⊏_{≈}_{n+1} hold for p and q.

– Clause (1). Assume that p →^{a} p′ and a ∈ Act_{n+1}. Note that this means that a ∈ Act_{ı(p,n+1)+n+1}. Therefore, as p ⊏_{∼}_{ı(p,n+1)+n+1} q, there exists q′ ∈ derivatives(q, a) such that

p′ ⊏_{∼}_{ı(p,n+1)+n} q′ .  (10)

Note now that, as p →^{a} p′, Csort(p′, n) is included in Csort(p, n + 1). From this observation, it follows that

ı(p′, n) + n ≤ ı(p, n + 1) + n .

As the sequence of preorders {⊏_{∼}_{k}| k ≥ 0} is decreasing with respect to set inclusion (Propn. 3.5(2)), (10) implies that

p′ ⊏_{∼}_{ı(p′,n)+n} q′ .  (11)

An application of the inductive hypothesis for statement (9) to (11) now yields

p′ ⊏_{≈}_{n} q′

as desired.

– Clause (2.1). Assume that p ↓. We shall prove that q ↓. First of all, note that, as

p ↓,

initials(p) ⊆ Csort(p, n + 1) ⊆ Act_{ı(p,n+1)+n+1} .

Now, as p ⊏_{∼}_{ı(p,n+1)+n+1} q, q ↓ follows immediately. Moreover, for use in the remainder of the proof, we also observe that initials(q) ⊆ Act_{ı(p,n+1)+n+1} follows.

– Clause (2.2). Assume that p ↓, q ↓ and q →^{a} q′ for some a ∈ Act_{n+1}. We shall show that p →^{a} p′ for some p′ ⊏_{≈}_{n} q′. To this end, note, first of all, that we know that initials(p) ⊆ Act_{ı(p,n+1)+n+1} and initials(q) ⊆ Act_{ı(p,n+1)+n+1} hold from our analysis of clause (2.1). Therefore, as p ⊏_{∼}_{ı(p,n+1)+n+1} q and a ∈ Act_{n+1} ⊆ Act_{ı(p,n+1)+n+1}, it follows that there exists p′ ∈ derivatives(p, a) such that:

p′ ⊏_{∼}_{ı(p,n+1)+n} q′ .

Reasoning as in our argument for clause (1), we infer that

p′ ⊏_{∼}_{ı(p′,n)+n} q′  (12)

also holds. An application of the inductive hypothesis for statement (9) to (12) now yields

p′ ⊏_{≈}_{n} q′

as desired.

The proof of the inductive step is now complete.

• ‘If Implication’. To prove that, for all p, q ∈ Proc,

p ⊏_{≈}_{ω} q ⇒ p ⊏_{∼}_{ω} q .

it is sufficient to show that, for all p, q ∈ Proc, n ≥ 0:

p ⊏_{≈}_{ı(Csort(q, n))+n} q ⇒ p ⊏_{∼}_{n} q .  (13)

Again, note that ı(Csort(q, n)) is a well-defined non-negative integer because, as the lts has bounded convergent sort, Csort(q, n) is a finite set of actions. To ease readability, throughout the proof we use ı(q, n) as a shorthand for ı(Csort(q, n)). We prove statement (13) by mathematical induction on n. The basis of the induction is immediate because ⊏_{∼}_{0} is the universal relation. For the inductive step, we assume that p ⊏_{≈}_{ı(q,n+1)+n+1} q, and prove that p ⊏_{∼}_{n+1} q holds. To this end, it is sufficient to show that the defining clauses of ⊏_{∼}_{n+1} hold for p and q.

– Clause (1). Assume that p →^{a} p′ and a ∈ Act_{n+1}. Note that this means that a ∈ Act_{ı(q,n+1)+n+1}. Therefore, as p ⊏_{≈}_{ı(q,n+1)+n+1} q, there exists q′ ∈ derivatives(q, a) such that

p′ ⊏_{≈}_{ı(q,n+1)+n} q′ .  (14)

Note now that, as q →^{a} q′, Csort(q′, n) ⊆ Csort(q, n + 1). From this observation, it follows that

ı(q′, n) + n ≤ ı(q, n + 1) + n .

As the sequence of preorders {⊏_{≈}_{k}| k ≥ 0} is decreasing with respect to set inclusion (Propn. 3.9(2)), (14) implies that

p′ ⊏_{≈}_{ı(q′,n)+n} q′ .  (15)

An application of the inductive hypothesis for statement (13) to (15) now yields

p′ ⊏_{∼}_{n} q′

as desired.

– Clause (2.1). Assume that initials(p) ⊆ Act_{n+1} and p ↓. We shall prove that initials(q) ⊆ Act_{n+1} and q ↓. First of all, note that, as p ⊏_{≈}_{ı(q,n+1)+n+1} q and p ↓, it follows immediately that q ↓. We shall now argue that initials(q) ⊆ Act_{n+1} also holds. To this end, assume that q →^{a} q′ for some q′. As q ↓, the action a is contained in Csort(q, n + 1). Therefore a is also contained in Act_{ı(q,n+1)+n+1}. As p ⊏_{≈}_{ı(q,n+1)+n+1} q,

p ↓, q ↓ and q →^{a} q′ with a ∈ Act_{ı(q,n+1)+n+1}, we infer that

p →^{a} p′, for some p′ .

As initials(p) ⊆ Act_{n+1} by assumption, it follows that a is contained in Act_{n+1}, which was to be shown.

– Clause (2.2). Assume that p ↓, q ↓, initials(p) ⊆ Act_{n+1}, initials(q) ⊆ Act_{n+1} and q →^{a} q′ for some a ∈ Act_{n+1}. We shall show that p →^{a} p′ for some p′ ⊏_{∼}_{n} q′. To this end, note that, as p ⊏_{≈}_{ı(q,n+1)+n+1} q and a ∈ Act_{n+1} ⊆ Act_{ı(q,n+1)+n+1}, it follows that there exists p′ ∈ derivatives(p, a) such that:

p′ ⊏_{≈}_{ı(q,n+1)+n} q′ .

Reasoning as in our argument for clause (1), we infer that

p′ ⊏_{≈}_{ı(q′,n)+n} q′  (16)

also holds. An application of the inductive hypothesis for statement (13) to (16) now yields

p′ ⊏_{∼}_{n} q′

as desired.

The proof of the inductive step is now complete.

This completes the proof of the theorem. □

It is interesting to note that above theorem would not hold for lts’s that do not have bounded convergent sort, as shown by the following example.

Example: Let Act = {a_{1}, a_{2}, a_{3}, …} be a countably infinite set of actions. Define the

synchronization trees:

t_{1} =^{Δ} a_{1} : 𝕆 + Ω
t_{ω} =^{Δ} (∑_{n≥1} a_{1} : a_{n} : 𝕆) + Ω

Note that t_{ω} does not have bounded convergent sort. We claim that t_{1} ⊏_{≈}_{ω} t_{ω}, but t_{1} ≴^{F} t_{ω}. First of all, note that, as t_{1} is a finite synchronization tree, the fact that t_{1} ≴^{F} t_{ω} follows immediately from the observation that t_{1} ≴ t_{ω}. To see that t_{1} ⊏_{≈}_{ω} t_{ω} does instead hold, note that, for every n ≥ 1,

𝕆 ⊏_{≈}_{n} a_{n+1} : 𝕆 .

This fact guarantees that t_{1} ⊏_{≈}_{n} t_{ω} for every n ≥ 0. □

3.2.2 Sort-finite Transition Systems

In [4, 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 ≲_{ω} defined on page 6. Using 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.11 For p, q ∈ Proc in any sort-finite transition system over a countable action set Act,

p ≲^{F} q ⇔ p ≲_{ω} q .

Proof: First of all, note that, in any lts, not necessarily sort-finite, p ≲_{ω} q implies p ≲^{F} q. In fact, for all p, q,

p ≲_{ω} q ⇔ p ⊏_{∼}Act_{ω} q
⇒ p ⊏_{∼}_{ω}^{fin} q (Propn. 3.1(2))
⇔ p ≲^{F} q (Thm. 3.2) .

We are therefore left to show that, for p, q ∈ Proc in any sort-finite transition system over a countable action set Act,

p ≲^{F} q ⇒ p ≲_{ω} q .

To this end, note, first of all, that any sort-finite lts has a fortiori bounded convergent sort. In view of Thm. 3.10, it is therefore sufficient to show that, for all p, q ∈ Proc,

p ⊏_{≈}_{ω} q ⇒ p ≲_{ω} q .

This will follow if we show that, for all p, q ∈ Proc, n ≥ 0,

p ⊏_{≈}_{ı(p,q)+n} q ⇒ p ≲_{n} q  (17)

where we use ı(p, q) as a shorthand for ı(sort(p) ∪ sort(q)), which is a well-defined non-negative integer as the lts is sort-finite.

We prove statement (17) by mathematical induction on n. The basis of the induction is trivial because ≲_{0} is the universal relation. For the inductive step, let us assume that p ⊏_{≈}_{ı(p,q)+n+1} q. We show that p ≲_{n+1} q holds. To this end, we proceed to check that the defining clauses of ≲_{n+1} are met by p and q.

1. Assume that p →^{a} p′. We shall prove that q →^{a} q′ for some q′ such that p′ ≲_{n} q′. As a ∈ sort(p) ⊆ Act_{ı(p,q)+n+1} and p ⊏_{≈}_{ı(p,q)+n+1} q, it follows that q →^{a} q′ for some q′ such that

p′ ⊏_{≈}_{ı(p,q)+n} q′ .  (18)

Note now that, as sort(p′) ⊆ sort(p) and sort(q′) ⊆ sort(q), it follows that ı(p′, q′) ≤ ı(p, q). As the sequence of preorders {⊏_{≈}_{k}| k ≥ 0} is decreasing with respect to set inclusion (Propn. 3.9(2)), (18) implies

p′ ⊏_{≈}_{ı(p′,q′)+n} q′ .  (19)

We may now apply the inductive hypothesis for statement (17) to (19) to infer that

p′ ≲_{n} q′

as desired.

2. Assume that p ↓. Then q ↓ is immediate from the fact that p ⊏_{≈}_{ı(p,q)+n+1} q.

3. Assume that p ↓, q ↓ and q →^{a} q′. We shall prove that p →^{a} p′ for some p′ such that p′ ≲_{n} q′. As a ∈ sort(q) ⊆ Act_{ı(p,q)+n+1} and p ⊏_{≈}_{ı(p,q)+n+1} q, it follows that p →^{a} p′ for some p′ such that

p′ ⊏_{≈}_{ı(p,q)+n} q′ .

Now reasoning as in point 1 above, we may infer that

p′ ⊏_{≈}_{ı(p′,q′)+n} q′

also holds. Again, an application of the inductive hypothesis gives that p′ ≲_{n} q′ as desired.

This completes the inductive proof of statement (17). □

Remark: An alternative proof of the above result can be given by mimicking the proof of statement S2 presented in Sect. 3.1.1. 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.

Note that the above argument applies regardless of the cardinality of the action set Act and of sort(q).

3.2.3 A Class of Image Finite Transition Systems

To conclude our taxonomy of characterizations of the finitary bisimulation, we present a class of lts’s with countable action set which do not necessarily have bounded convergent sort, but for which the finitary bisimulation coincides with ⊏_{≈}_{ω}. We believe that this result is mainly of theoretical interest, but we find it worthwhile to include it for the sake of completeness.

Proposition 3.12 Let p, q ∈ Proc in any transition system over a countable action set Act. Assume furthermore that the transition system is image finite, and weakly initials finite. Then

p ≲^{F} q ⇔ p ⊏_{≈}_{ω} q .

Proof: Consider a transition system over a countable action set Act which is image finite and weakly initials finite. In view of Thm. 3.7, it is sufficient to prove that, for all p, q ∈ Proc,

p ⊏_{∼}_{ω} q ⇔ p ⊏_{≈}_{ω} q .

We show the two implications in the above statement separately.

• ‘Only If Implication’. We show that, for all p, q ∈ Proc, n ≥ 0

p ⊏_{∼}_{ω} q ⇒ p ⊏_{≈}_{n} q .

The proof is by mathematical induction on n. The basis of the inductive argument is trivial as ⊏_{≈}_{0} is the universal relation over Proc. To establish the inductive step, let us assume that p ⊏_{∼}_{ω} q holds. We prove that p ⊏_{≈}_{n+1} q also holds. To this end, it is sufficient to show that the defining clauses of ⊏_{≈}_{n+1} are met by p and q.

– Clause (1). Assume that a is an action in Act_{n+1} and p →^{a} p′. As p ⊏_{∼}_{ω} q and a is contained in Act_{m} for every m ≥ n + 1, for every such positive integer m there exists a process q_{m} such that

q →^{a} q_{m} and p′ ⊏_{∼}_{m} q_{m} .

As the lts is image-finite, the set of processes {q_{m} | m ≥ n + 1} is finite. This implies that, for some q′ contained in {q_{m} | m ≥ n + 1}, p′ ⊏_{∼}_{m} q′ for infinitely many positive integers m. As the sequence of preorders {⊏_{∼}_{k}| k ≥} is decreasing (Propn. 3.1(2)), it follows that p′ ⊏_{∼}_{m} q′ for all m ≥ 0, i.e., that p′ ⊏_{∼}_{ω} q′. By induction, we now obtain p′ ⊏_{≈}_{n} q′ as desired.

– Clause (2.1). Assume that p ↓. We shall prove that q ↓. As the lts under consideration is weakly initials finite, the set of initial actions from p is finite. Let M =^{Δ} ı(initials(p))+1. As p ⊏_{∼}_{ω} q, it follows that p ⊏_{∼}_{M} q. As p ↓ and initials(p) ⊆ Act_{M}, we infer that q ↓, which was to be shown. Moreover, for use in the remainder of the proof, we also obtain that initials(q) ⊆ Act_{M}.

– Clause (2.2). Assume that p ↓, q ↓, a ∈ Act_{n+1} and q →^{a} q′. By a previous observation, it follows that a ∈ Act_{M}, where M is the positive integer defined in the proof for clause (2.1). As p ⊏_{∼}_{ω} q, p ↓, q ↓, initials(p) ⊆ Act_{M}, initials(q) ⊆ Act_{M} and Act_{M} is included in Act_{m} for every m ≥ M, we infer that, for every such positive integer m, there exists a process p_{m} such that

p →^{a} p_{m} and p_{m} ⊏_{∼}_{m} q′ .

Reasoning as in the proof for clause (1) above, we may conclude that there is a process p′ ∈ derivatives(p, a) such that p′ ⊏_{∼}_{ω} q′. By induction, we now obtain p′ ⊏_{≈}_{n} q′ as desired.

This completes the proof for the inductive step.

• ‘If Implication’. We show that, for all p, q ∈ Proc in an image finite lts, n ≥ 0,

p ⊏_{≈}_{ω} q ⇒ p ⊏_{∼}_{n} q .

The proof is by mathematical induction on n, and is very similar to the one presented above. For this reason, we limit ourselves to presenting the argument for clause (2.1) of the definition of ⊏_{∼}_{n+1}. To this end, assume that p ⊏_{≈}_{ω} q, p ↓ and initials(p) ⊆ Act_{n+1}. We prove that q ↓ and that initials(q) is also included in Act_{n+1}. The fact that q definitely converges is an immediate consequence of the assumption that p ↓ and p ⊏_{≈}_{1} q. To see that every action a contained in initials(q) is also in Act_{n+1}, we reason as follows. Assume that q →^{a} q′. Pick a positive integer N such that a is contained in Act_{N}. As p ⊏_{≈}_{N} q, p ↓, q ↓, a ∈ Act_{N} and q →^{a} q′, it follows that p →^{a} p′ for some p′ ⊏_{≈}_{N−1} q′. That is a ∈ initials(p) ⊆ Act_{n+1}, which was to be shown.

The proof of the theorem is now complete. □

The examples on pages 11 and 24 show that neither of the constraints in the proviso of the above result can be omitted.

Acknowledgements: We have benefited from illuminating discussions with Samson Abramsky on the two different versions of the domain logic for transition systems presented in [2, 4]. Our overall debt to his seminal work will be evident to the readers of this paper.

References

[1] S. Abramsky, Experiments, powerdomains and fully abstract models for applicative multiprogramming, in Foundations of Computation Theory, M. Karpinski, ed., vol. 154 of Lecture Notes in Computer Science, Springer-Verlag, 1983, pp. 1–13.

[2] , Domain Theory and the Logic of Observable Properties, PhD thesis, University of London, 1987.

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

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

[5] , Domain theory in logical form, Annals of Pure and Applied Logic, 51 (1991), pp. 1–77.

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

[7] K. Apt and G. Plotkin, Countable nondeterminism and random assignment, J. Assoc. Comput. Mach., 33 (1986), pp. 724–767.

[8] J. Baeten and W. Weijland, Process Algebra, Cambridge Tracts in Theoretical Computer Science 18, Cambridge University Press, 1990.

[9] I. Guessarian, Algebraic Semantics, vol. 99 of Lecture Notes in Computer Science, Springer-Verlag, 1981.

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

[11] , Algebraic Theory of Processes, MIT Press, Cambridge, Massachusetts, 1988.

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

[13] 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.

[14] C. Hoare, Communicating Sequential Processes, Prentice-Hall International, Englewood Cliffs, 1985.

[15] A. Ingólfsdóttir, Semantic Models for Communicating Process with Value-Passing, PhD thesis, School of Cognitive and Computing Sciences, University of Sussex, June 1994. Computer Science Report 8/94. Also available as Report R–94– 2044, Department of Mathematics and Computer Science, Aalborg University.

[16] , A semantic theory for value-passing processes late approach — Part II: A behavioural semantics and full abstractness, Report RS–95–22, BRICS (Basic Research in Computer Science, Centre of the Danish National Research Foundation), Institute for Electronic Systems, Department of Mathematics and Computer Science, Aalborg University Centre, April 1995.

[17] A. Ingólfsdóttir and A. Schalk, A fully abstract denotational model for observational congruence, Report RS–95–40, BRICS (Basic Research in Computer Science, Centre of the Danish National Research Foundation), Institute for Electronic Systems, Department of Mathematics and Computer Science, Aalborg University Centre, August 1995. To appear in Proceedings CSL ’95.

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

[19] A. Meyer, Semantical paradigms: Notes for an invited lecture, in Proceedings 3^{th} Annual Symposium on Logic in Computer Science, Edinburgh, IEEE Computer Society Press, 1988, pp. 236–242.

[20] R. Milner, Processes: A mathematical model of computing agents, in Proceedings Logic Colloquium 1973, H. Rose and J. Shepherdson, eds., North-Holland, 1973, pp. 158–173.

[21] , Fully abstract models of typed λ-calculi, Theoretical Comput. Sci., 4 (1977), pp. 1–22.

[22] , 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.

[23] , Calculi for synchrony and asynchrony, Theoretical Comput. Sci., 25 (1983), pp. 267–310.

[24] , Communication and Concurrency, Prentice-Hall International, Englewood Cliffs, 1989.

[25] 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.

[26] G. Plotkin, LCF considered as a programming language, Theoretical Comput. Sci., 5 (1977), pp. 223–256.

[27] , Lecture notes in domain theory, 1981. University of Edinburgh.

[28] , A structural approach to operational semantics, Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.

[29] D. Scott and C. Strachey, Towards a mathematical semantics for computer languages, in Proceedings of the Symposium on Computers and Automata, vol. 21 of Microwave Research Institute Symposia Series, 1971.

[30] C. Stirling, Modal logics for communicating systems, Theoretical Comput. Sci., 49 (1987), pp. 311–347.

[31] V. Stoltenberg-Hansen, I. Lindström, and E. Griffor, Mathematical Theory of Domains, Cambridge Tracts in Theoretical Computer Science 22, Cambridge University Press, 1994.

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

[33] Y. Wang, Real-time behaviour of asynchronous agents, in Proceedings CONCUR 90, Amsterdam, J. Baeten and J. Klop, eds., vol. 458 of Lecture Notes in Computer Science, Springer-Verlag, 1990, pp. 502–520.

Recent Publications in the BRICS Report Series

RS-95-59 Luca Aceto and Anna Ing� olfsd� ottir. On the Finitary Bisimulation. November 1995. 29 pp.

RS-95-58 Nils Klarlund, Madhavan Mukund, and Milind Sohoni. Determinizing Asynchronous Automata on In�nite Inputs. November 1995. 32 pp.

RS-95-57 Jaap van Oosten. Topological Aspects of Traces. November 1995. 16 pp.

RS-95-56 Luca Aceto, Wan J. Fokkink, Rob J. van Glabbeek, and Anna Ing� olfsd� ottir. Axiomatizing Pre�x Iteration with Silent Steps. November 1995. 25 pp.

RS-95-55 Mogens Nielsen and Kim Sunesen. Trace Equivalence - Partially Decidable! November 1995.

RS-95-54 Nils Klarlund, Mogens Nielsen, and Kim Sunesen. Using Monadic Second-Order Logic with Finite Domains for Speci�cation and Veri�cation. November 1995.

RS-95-53 Nils Klarlund, Mogens Nielsen, and Kim Sunesen. Automated Logical Veri�cation based on Trace Abstractions. November 1995.

RS-95-52 Anton��n Ku� cera. Deciding Regularity in Process Algebras. October 1995. 42 pp.

RS-95-51 Rowan Davies. A Temporal-Logic Approach to Binding-Time Analysis. October 1995. 11 pp.

RS-95-50 Dany Breslauer. On Competitive On-Line Paging with Lookahead. September 1995. 12 pp.

RS-95-49 Mayer Goldberg. Solving Equations in the λ-Calculus using Syntactic Encapsulation. September 1995. 13 pp.

RS-95-48 Devdatt P. Dubhashi. Simple Proofs of Occupancy Tail Bounds. September 1995. 7 pp. To appear in Random Structures and Algorithms.

RS-95-47 Dany Breslauer. The Suf�x Tree of a Tree and Minimizing Sequential Transducers. September 1995. 15 pp.