BRICS RS-99-14 Fiore et al.: Weak Bisimulation and Open Maps BRICS

Basic Research in Computer Science

Weak Bisimulation and Open Maps

Marcelo P. Fiore Gian Luca Cattani Glynn Winskel BRICS Report Series RS-99-14 ISSN 0909-0878 May 1999 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1999, Marcelo P. Fiore & Gian Luca Cattani & Glynn

Winskel. 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/99/14/

Weak Bisimulation and Open Maps

(Extended Abstract)

Marcelo Fiore COGS

University of Sussex, UK Gian Luca Cattani^{∗} Computer Laboratory University of Cambridge, UK

Glynn Winskel BRICS^{†} University of Aarhus, DK

April 1999

Abstract

A systematic treatment of weak bisimulation and observational congruence on presheaf models is presented. The theory is developed with respect to a “hiding” functor from a category of paths to observable paths. Via a view of processes as bundles, we are able to account for weak morphisms (roughly only required to preserve observable paths) and to derive a saturation monad (on the category of presheaves over the category of paths). Weak morphisms may be encoded as strong ones via the Kleisli construction associated to the saturation monad. A general notion of weak open-map bisimulation is introduced, and results relating various notions of strong and weak bisimulation are provided. The abstract theory is accompanied by the concrete study of two key models for concurrency, the interleaving model of synchronisation trees and the independence model of labelled event structures.

To appear in Proceedings of the 14th Annual IEEE Symposium on Logic in Computer science, LICS’99, IEEE Press, July 1999.

∗This author is supported by EPSRC grant GR/L62290: Calculi for Interactive Systems: Theory and Experiment.

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

Introduction

Strong bisimulation of Park and Milner is often too discriminating an equivalence on transitions systems. For this reason Milner invented weak bisimulation [16] which abstracts away from invisible actions, usually labelled τ. Although an action is itself invisible its effect need not be, leading Milner to a construction which we can view as adjoining to a transition system all its weak transitions. A weak transition with label τ represents a, possibly empty, sequence of τ-transitions whereas a weak transition with non-τ label a represents the visible action a preceded and followed by, possibly empty, sequences of τ-transitions in the original transition system. Transition systems are weakly bisimilar if they become strongly bisimilar when saturated with all their weak transitions.

Weak bisimulation has the drawback of not being a congruence with respect to the usual operations of process calculi—it is not respected by nondeterministic sum—which forced Milner to refine weak bisimulation to observational congruence. Again observational congruence can be reduced to strong bisimulation via an operation on transition systems like that for weak bisimulation, but this time treating the initial actions specially. For this operation to make sense the transition systems need to be “non-restarting” (i.e., transition systems for which there are no transitions back to the initial state).

Milner’s operations on transition systems translate to the category of transition systems with label-preserving maps [25]. Both operations become monads on the category of transition systems, in line with their being operations of saturation. Corresponding monads on the category of synchronisation trees are derived by composing the coreflection from synchronisation trees to transition systems with the monads on transition systems.

The paper [13] shows how to generalise strong bisimulation to other classes of models presented as categories via spans of open maps. Once we have strong bisimulation in place for a particular category of models, given analogues of Milner’s operations as monads we can define the corresponding weak bisimulation and observational congruence. But this raises the question of how to define the monads for other models. Indeed the question of weak bisimulation and observational congruence has traditionally been addressed afresh for each new process language.

The contribution of this paper is a study of a systematic way to define weak bisimulation and observational congruence on presheaf models. Presheaf models have been shown to include traditional models like synchronisation trees and event structures [13] along with their notion of bisimulation, to be related by powerful preservation properties associated with colimit-preserving functors [9], and to form a domain theory for bisimulation [23, 7, 6] in which a wide range of, possibly higher-order, process languages can receive a denotational semantics.

In [17] an approach to an open-map account of weak bisimulation on transition systems is based on “weak morphisms”, a reconstruction of the maps between transition systems to account for the invisibility of τ-actions. That paper implicitly takes the weak morphisms to be maps in the Kleisli category of the saturation monad and shows that weak bisimulation coincides with open-map bisimulation in this Kleisli category.

This line can be followed for presheaf models but more generally with respect to any “hiding” functor h : ℙ [figure] ℚ. Here we think of ℙ as a category of computation paths with invisible actions and ℚ as paths without; for instance ℙ might be strings of actions with τ while ℚ is strings of just visible actions. A treatment of weak bisimulation must also yield an operation of hiding which makes certain events of a process invisible. For example, Milner’s operations can be regarded as hiding the τ-actions a process can do by allowing arbitrarily many τ-actions to participate in any transition between states—a sort of hiding by obfuscation. Our treatment of weak bisimulation goes via an intermediary construction of hiding on processes regarded as bundles—this view seems important in its own right. A presheaf over ℙ can be viewed as a discrete fibration and so as an object in Cat/ℙ, i.e., as a bundle over ℙ in Cat. We can regard such bundles as generalised transition systems as advocated in [26, 4]. Now we can express the operation of hiding directly: via composition with the hiding functor h a bundle over ℙ becomes a bundle over ℚ. Maps in Cat/ℚ need only respect the “visible” actions ℚ and generalise “weak morphisms”. The operation of taking a presheaf over ℙ to a bundle over ℚ has a right adjoint. This adjunction induces a saturation monad T_{h} on presheaves over ℙ. This monad is shown to preserve open-map bisimulation, generalising the expectation that strongly bisimilar processes should be weakly bisimilar.

There are two ways we might say that presheaves X, Y over ℙ are weakly bisimilar:

(i) if T_{h}(X) and T_{h}(Y) are open-map bisimilar as presheaves over ℙ;

(ii) if X and Y are open-map bisimilar in the Kleisli category of T_{h}.

The two conditions are not equivalent in general. We investigate when they are (see ‘Sharp functors’, Section 3).

Interestingly, in our work it is the analogue of observational congruence which becomes primary; the general treatment of weak bisimulation involves considering initial states explicitly. We accompany the general theory of weak bisimulation and observational congruence with a discussion of two running examples, the principal models for concurrency of synchronisation trees and labelled event structures. We leave to future work the investigation of weak bisimulation for higher-order process languages whose semantics is supported by presheaf models.

Organisation of the paper. In Sections 1 and 2, after reviewing the notions of open-map bisimulation and the view of processes as presheaves, we advocate a view of processes as bundles. Section 3 contains the main theoretical development. The notions of weak morphism and weak open-map bisimulation, and the construction of the saturation monad are introduced. Results relating the various notions of strong and weak bisimulation are provided. In Section 4 consequences of the general theory are derived for the models of synchronisation trees and of labelled event structures. In the case of synchronisation trees, weak open-map bisimulation is shown to coincide with Milner’s weak bisimulation and observational congruence depending on whether the “hiding” functor is defined on all strings of actions or just on the non-empty ones. For event structures, weak open-map bisimulation is characterised in terms of a weak form of hereditary history preserving bisimulation.

1 Open maps and bisimulation

We briefly review the notion of open map bisimulation [13]. The starting point is the work on categorical models for concurrency, such as [24, 19, 21, 22], which has concentrated on understanding the structure and relationships between classes of models, ranging from synchronisation trees to transition systems, event structures and Petri nets. Morphisms between models account for the possibility of a model to simulate the behaviour of another. In other words they represent functional simulations. A primary example of such a category of models is represented by transition systems.

Definition 1.1 For a set of actions A, let TS_{A} be the category of transition systems over A with morphisms given by functions between the corresponding sets of states that preserve the initial state and the transition relation, respecting the labelling (see [13]).

If morphisms in a category of models are understood as functional simulations. It is natural to ask whether it is possible to distinguish among all such functional simulations those that in fact are bisimulations. Consider two transition systems over the same set of actions A, T_{0} = (S_{0}, ∗_{0}, [figure]_{0}) and T_{1} = (S_{1}, ∗_{1}, [figure]_{1}), and a morphism f : T_{0} [figure] T_{1} between them. The morphism f is said to be a zig-zag morphism [2] if it further satisfies the following property, for every reachable state s ∈ S_{0} and every action a ∈ A:

f(s) [figure: a]_{1} t′ implies ∃ t ∈ S_{0}. s [figure: a]_{0} t and f(t) = t′ .

In other words, f not only preserves but also reflects reachable transitions. If f is a zig-zag morphism, then its graph is a bisimulation between the two transition systems. In [13] the above situation was axiomatised in terms of the following path lifting property (see [13, 6] for more detailed explanations). Suppose that within a category of models, M, one can distinguish a subcategory of computation paths (or shapes), ℙ. The objects of ℙ account for runs (or history) of a process and their morphisms tell us how one path can be extended by another one. Given the inclusion functor I : ℙ [figure] M, a morphism X [figure] Y in M is said to be an I-open map if, for all e : p [figure] q in ℙ, every commutative square

\xymatrix{Ip \ar[r] \ar[d]_{Ie} & X \ar[d] \\ Iq \ar[r] \ar@{.>}[ur]^{∃} & Y}

has a fill-in as indicated. Note that the definition of open map makes sense for any functor P [figure] M and not only for inclusions.

Going back to transition systems, a natural choice for the category ℙ is that of transition systems whose transition graph consists of a finite sequence of transitions. If A is the set of actions, this category is equivalent to the partial order A^{∗} of finite strings of elements of A. With this choice of ℙ for M = TS_{A}, we have that the I-open maps are the zig-zag morphisms.

Since I-open maps correspond to functional bisimulations, open map bisimilarity is defined in terms of spans of open maps: two objects in M are said to be I-open map bisimilar if they are related by a span of I-open maps. Not surprisingly one can prove that two transition systems are Park-Milner strong bisimilar iff they are I-open map bisimilar for I : A^{∗} [figure] TS_{A} [13].

Preservation properties. We list some properties of the notion of openness (see also [13]) that will be used in the study of weak open-map bisimilarity in Section 3.

In the situation [figure: C; H; A; F; ⊤; B,; G] we have that:

1. For every g ∈ B, Gg is H-open iff g is F H-open.

Therefore, given a monad T on A, it follows that, for all f ∈ A, F_{T} f ∈ Kleisli(T) is F_{T} H-open iff T f ∈ A is H-open.

2. For X, Y ∈ A, if F X and F Y are F H-open map bisimilar then GF X and GF Y are H-open map bisimilar. In addition, if GF preserves H-open maps and the multiplication of the monad induced by the adjunction F ⊣ G is pointwise H-open, then the converse also holds.

2 Presheaf models

2.1 Processes as presheaves

There is much freedom in the choice of the path category, ℙ, which, in principle, bears no particular relationship with the category of models M other than being one of its subcategories. For some concrete examples, such as transition systems, certain path categories immediately suggest themselves as “natural” choices (see [13]) but, in general we cannot expect this to happen. There is an important class of categories which are equipped with a canonical choice of path category. These are the so-called presheaf categories. Given a small category ℙ, the category of presheaves over ℙ, written ℙ̂, is the category of functors ℙ^{op} [figure] Set (where Set is the category of sets and functions) and natural transformations. What is crucial for us is that the category ℙ̂ is also a concrete representation of the free colimit completion of ℙ (we shall expand on the corresponding universal property in the last paragraph of this section). The embedding of a category ℙ into its presheaf completion, ℙ̂, is the well-known Yoneda embedding, Y_{ℙ} : ℙ [figure]ℙ̂ [14]. Henceforth we will identify ℙ with its image in ℙ̂ under Y_{ℙ}.

Given a category ℙ, we write ℙ_{⊥} for the category ℙ to which a strict new initial object, ⊥, has been added. Writing Y_{ℙ}^{∘} : ℙ_{⊥} [figure] ℙ̂ for the strict (i.e., initial-object preserving) extension of Y_{ℙ}, a map in ℙ̂ is Y_{ℙ}^{∘}-open iff it is surjective and Y_{ℙ}-open, the canonical choice for open-map bisimulation in a presheaf category [13].

Presheaf categories subsume more traditional categories of models. It was suggested in [13] that they deserve to be studied as categories of models for concurrency in their own right. Subsequent work on this line appeared in [9, 23, 26, 8, 7, 11, 6].

Synchronisation trees. A simple example of a presheaf model is given by synchronisation trees. A synchronisation tree is a transition system whose transition graph is a tree with root the initial state.

Definition 2.1 For a set of actions A, let ST_{A} be the full subcategory of TS_{A} of synchronisation trees.

We have already seen the partial order, regarded as a category, A^{∗}. We define A^{+} to be its subcategory consisting of non-empty strings. Notice that (A^{+})_{⊥} ≅ A^{∗}.

Proposition 2.2 (cf. [13]) For a set of actions A, the categories ST_{A} and Â^{+} are equivalent.

Via the equivalence of the above proposition, Park-Milner strong bisimulation [16] coincides with Y_{A^{+}}^{∘}-open map bisimulation [13].

Event structures. Event structures do not correspond to presheaf categories as transparently as synchronisation trees. Still, categories of event structures embed in presheaf categories over pomset categories as observed in [13].

Definition 2.3 For a set of actions A, let ES_{A} be the category of event structures labelled in A with arrows given by total functions between event sets which respect actions and whose direct image preserve configurations bijectively on events, as in [13]. A morphism is said to be strict if it is a monotone function with respect to the partial order relation on events. Define ES_{A}^{s} to be the subcategory of ES_{A} with the same objects but only strict morphisms.

In [13] open map bisimulation for event structures was studied with respect to the choice of pomsets [18] as objects of the path category.

Definition 2.4 Define a pomset to be a triple (P, ≤, l) with P a finite set, (P, ≤) a partial order and l : P [figure] A a labelling function.

Any pomset gives rise to an event structure (see [13]). The full subcategory of ES_{A} of pomsets is a large category, though equivalent to a small one. We thus take as path category a small category equivalent to the category of pomsets. In particular we can choose it to be skeletal, i.e., such that any two isomorphic objects are equal. (This will have some technical advantages for proving the results of Subsection 4.2.)

Definition 2.5 For a set of actions A, let Pom_{A} be a skeleton of the full subcategory of ES_{A} of non-empty pomsets labelled in A. Define Pom_{A}^{s} to be the subcategory of Pom_{A} with the same objects but only strict morphisms.

The embeddings of Pom_{A} into ES_{A} and of Pom_{A}^{s} into ES_{A}^{s} are dense functors; hence ES_{A} fully embeds into \begin{matrix} \\ Pom & A \end{matrix} and ES_{A}^{s} fully embeds into \begin{matrix} \\ Pom & sA \end{matrix} (see [14, 13]). Moreover, for either Y^{∘} : (Pom_{A})_{⊥} [figure] \begin{matrix} \\ Pom & A \end{matrix} or Y^{∘} : (Pom_{A}^{s})_{⊥} [figure] \begin{matrix} \\ Pom & sA \end{matrix}, open map bisimulation corresponds to hereditary history preserving bisimulation [1] (see [13, 26] for more details).

Universal property of presheaf categories. As mentioned at the beginning of this subsection, the Yoneda embedding Y : ℙ [figure] ℙ̂ exhibits ℙ̂ as the free cocompletion of ℙ (see, eg., [15]). More precisely, for every cocomplete category C, we have the following equivalence of categories.

Adj(ℙ̂, C) ≃ Cocont(ℙ̂, C) ≃ CAT(ℙ, C)
[figure: (L ⊣ R); L; LY]

where Adj(A, B) is the category of adjoint pairs L ⊣ R : B [figure] A (and natural transformations between left adjoints), Cocont(A, B) is the category of colimit preserving (i.e., cocontinuous) functors A [figure]B (and natural transformations), and CAT(A, B) is the category of functors A [figure] B (and natural transformations). This information can be succinctly expressed by the diagram

[figure: ℙ; Y; F; ≅; ℙ̂; L; ⊣; C; R]

with L = Lan_{Y}(F), the left Kan extension [14] of F along Y, and R = (C [figure] C(F , C)). In particular, for C = ℚ̂, we have the following coend formula for left Kan extensions

L(X)(q) = ∫ ^{p∈ℙ} X(p) × F (p)(q) .

2.2 Processes as bundles

We advocate a viewpoint of processes, as bundles (see also [4, 26]), that is important in our treatment of weak bisimulation. Roughly speaking, “a bundle is just a map viewed as an object in a particular category” [12, page 11]; which in our case is the category of small categories and functors Cat.

To motivate this point of view let us consider a synchronisation tree T = (S, ∗, [figure] ) over a set of actions A. This representation of processes is misleading in that it does not provide a clear cut between two conceptually different notions; viz., the transitions between states and the actions being observed along a transition. However, a structure embodying these concepts

may be disentangled from the above representation, to obtain a bundle [figure: 𝕋; 𝔸]

in Cat, as follows.

1. The category of computation states and transitions 𝕋 associated to the synchronisation tree T has objects given by pairs (α ∈ A^{+}, s ∈ S) such

that ∗ [figure: α]^{∗}s in T, and morphisms β : (α, s) [figure] (αβ, s′) iff s [figure: β]^{∗}s′ in T, where for a string α = a_{1}a_{2} … a_{n}, we write s [figure: α]^{∗}s′ to mean that there exist states s_{1}, s_{2}, …, s_{n} such that s [figure: a_{1}] s_{1} [figure: a_{2}] s_{2} [figure] … [figure: a_{n}] s_{n} = s′.

2. The category of path shapes (or observation stages) is given by the poset A^{+}.

3. The labelling functor 𝕋 [figure] 𝔸 associates to a transition β : (α, s) [figure] (αβ, s′) the sequence of actions β observed along the computation path

s [figure: β]^{∗}s′ in T.

This association of a bundle to a synchronisation tree (that is, a presheaf in Â^{+}) can be done for presheaves over an arbitrary path category, and corresponds to the well-known Grothendieck construction [15] given by the functor:

ℙ̂ [figure: D]Cat/ℙ
(X [figure: f] Y) [figure] \xymatrix{ℙ/X \ar[rr]^{Σ_{f}} \ar[dr]_{_{dom_{X}}} &  & ℙ/Y \ar[dl]^{_{dom_{Y}}} \\  & ℙ}

where Σ_{f}(x) = f ∘ x and Σ_{f}(x [figure: χ]x′) = χ. Intuitively, the category of computation states and transitions ℙ/X (usually denoted ∫ X) consists of the computation paths x : p [figure] X (in ℙ̂) of the process X with transitions e : (p, x) [figure] (p′, x′) (in ℙ) given by path extensions (that is, subject to the equality p = p′ ∘ e).

The Grothendieck construction D is an embedding (i.e., full and faithful). Thus, a map of processes X [figure] Y in ℙ̂ amounts precisely to a functor ∫ X [figure]∫ Y between the corresponding categories of computation states and transitions that is compatible with the observations along transitions; that is, such that the diagram

\xymatrix{∫ X \ar[rr] \ar@{-->}[dr]_{DX} &  & ∫ Y \ar@{-->}[dl]^{DY} \\  & ℙ}  (1)

commutes. Moreover, D cuts down to an equivalence

ℙ̂ ≃ DFib/ℙ ,

where DFib/ℙ is the full subcategory of discrete fibrations over ℙ [10], which characterises presheaf models as bundles.

As it will be useful for us in the next section, we remark on a universal characterisation of the Grothendieck construction (that is presumably folklore—cf. [20]) summarised in the statement below.

Theorem 2.6 We have the following situation

[figure: p; ℙ; Y; dom; ℙ̂; D; ⊣; ℙ/p; ℙ; _{dom_{p}}; Cat/ℙ; U]

where D = Lan_{Y}(dom), U( [figure: 𝕏; ℙ]) = Cat/ℙ( [figure: ℙ/(−); ℙ; dom] , [figure: 𝕏; ℙ]).

Informally, the functor U unfolds a bundle [figure: 𝕏; ℙ]into the process consisting

of all the possible runs, along paths in ℙ, in the category of states and transitions 𝕏.

3 Weak open-map bisimulation on presheaf models

We provide a uniform treatment of weak open-map bisimulation for presheaf models. In this section, we focus in the motivation and analysis of the concepts and mathematical structures involved; case studies of particular examples are deferred to Section 4.

Weak bisimulation. A central rôle in the development of weak bisimulation in [16, Chapter 5, Section 1] is played by notions of weak transitions. Given a transition system T = (S, ∗, [figure] ) over a set of actions A = L + {τ}, for s, t ∈ S, there is a weak transition s [figure: α] t (α = a_{1} … a_{n}) iff s ( [figure: τ] )^{∗} [figure: a_{1}] ( [figure: τ] )^{∗} ⋯ ( [figure: τ] )^{∗} [figure: a_{n}] ( [figure: τ] )^{∗} t. With the aid of this definition, given a transition system T = (S, ∗, [figure] ) one may construct its saturation by τ actions (cf. [16]) as the transition system T (T) = (S, ∗, [figure] ) where s [figure: a] s′

iff s [figure: â] s′ with τ̂ = ε and ℓ̂= ℓ (ℓ ∈ L). This construction is important for defining and characterising weak bisimulation. Indeed, recall that a relation R ⊆ S_{0} × S_{1} between states of transition systems T_{0} and T_{1} is said to be a weak bisimulation [16] if ∗_{0} R ∗_{1} and, whenever s R s′, we have that s [figure: a]_{0} t

implies s′ [figure: â]_{1} t′ with t R t′, for some t′; and s′ [figure: a]_{1} t′ implies s [figure: â]_{0} t with t R t′, for some t. Moreover, as is well-known, two transition systems are weakly bisimilar iff their saturations are strongly bisimilar.

Notice in particular that a functional weak-bisimulation f from T_{0} to T_{1} is a function S_{0} [figure] S_{1} between states which preserves the initial state and is such that

1. for every s ∈ S_{0}, s [figure: a]_{0} t in T_{0} implies f(s) [figure: a]_{1} f(t) in T (T_{1}),

2. for every reachable s ∈ S_{0}, f(s) [figure: a]_{1} t′ in T_{1} implies s [figure: a]_{0} t in T (T_{0}) with f(t) = t′, for some t.

This suggests that in order to capture the notion of weak bisimilarity via (spans of) open maps one should consider weak morphisms mapping strong transitions to weak ones, as in condition (1) above. The idea of considering weak morphisms in connection with studies of weak bisimulation has been considered before; it first appeared in [5] and was used in [17] to characterise weak bisimulation via open maps. However, what is new in our work is the following conceptual treatment of weak morphisms and of the saturation construction.

Weak morphisms. The definition of the weak transition [figure] involves two ingredients:

1. the consideration of sequences of transitions, and

2. a notion of hiding associated to observations.

The viewpoint of processes as bundles of Subsection 2.2 already accounts for (1), as the structure of states and transitions is given by a category (where transitions may be composed). The incorporation of (2) requires the assumption of extra structure. For instance, the hiding operation associated to the observations on synchronisation trees over the set of actions A = L + {τ} (i.e., presheaves over A^{+}) is given by the (monotone) function ˆ(−) : A^{+} [figure] L^{∗} that hides the invisible τ actions. Indeed, given a presheaf

T on A^{+}, a weak transition s [figure: ℓ]t (ℓ ∈ L) corresponds to a transition β : (α, s) [figure](αβ, t) in the category of computation states ∫ T such that β̂ = ℓ (i.e., β = τ^{m}ℓτ^{n}); whilst s [figure: τ]t corresponds to a transition β : (α, s) [figure] (αβ, t) in ∫ T for which β̂ = ε (i.e., β = τ^{n}).

These considerations, scaled-up to arbitrary presheaf models, motivate introducing the notion of weak morphism between processes in ℙ̂ with respect to a functor h : ℙ [figure] ℚ that interprets the paths in ℙ as observations in ℚ. Hence, we define an h-weak morphism between processes X, Y ∈ ℙ̂ as a functor ∫ X [figure] ∫ Y between their associated categories of computation states and transitions that is compatible with the observations along transitions; that is, such that the diagram

\xymatrix{∫ X \ar[rr] \ar[d]_{DX} &  & ∫ Y \ar[d]^{DY} \\ ℙ \ar[dr]_{h} &  & ℙ \ar[dl]^{h} \\  & ℚ}

commutes. We write Weak(h) for the category of h-weak morphisms between presheaves in ℙ̂. Notice that since every (strong) morphism in ℙ̂ yields a weak morphism in Weak(h) (see (1)) we have an identity-on-objects faithful functor W_{h} : ℙ̂ [figure]Weak(h) : f [figure]Σ_{f}. This equips the category Weak(h) with the path functor W_{h}Y^{∘} : ℙ_{⊥} [figure] Weak(h) which induces a notion of weak open-map bisimilarity, W_{h}Y^{∘}-open map bisimilarity, referred to as h-bisimilarity.

Saturation monad. We show that a saturation construction for presheaf models, allowing the encoding of weak morphisms as strong ones, arises naturally from our analysis. Notice first that, for h : ℙ [figure] ℚ, the category of h-weak morphisms may be more abstractly presented using the functor

D_{h} = ℙ̂ [figure: D] Cat/ℙ [figure: Σ_{h}] Cat/ℚ ;

since, for X, Y ∈ ℙ̂,

Weak(h)(X, Y) = Cat/ℚ (D_{h}X, D_{h}Y) .  (2)

As D_{h} has a right adjoint U_{h} given as follows

ℙ̂ [figure: D; ⊤; U]Cat/ℙ [figure: Σ_{h}; ⊤; h^{∗}]Cat/ℚ ,  (3)

(where h^{∗} denotes the functor that pullbacks a bundle along h) we have, from (2), that

Weak(h)(X, Y) ≅ ℙ̂(X, U_{h}D_{h}Y)
= Kleisli(T_{h})(X, Y)

where T_{h} is the saturation monad on ℙ̂ induced by the adjunction (3). Thus, Weak(h) is (isomorphic to) the Kleisli category of the saturation monad T_{h}.

The saturation monad has the following explicit description

T_{h}(X) = Cat/ℚ (D_{h}(−), D_{h}X)  (4)

from which one clearly sees that the computation paths in T_{h}(X) correspond to weak computation paths in X.

To see the saturation monad at work, let us consider the hiding functor h = ˆ( ) : A^{+} [figure]L^{∗}. To compute, for instance, the saturation of the synchronisation tree T = (∗ [figure: τ] 0 [figure: τ] 1) we proceed as follows.

1. We regard T as the bundle [figure: ∫ T; A^{+}; t] given by

[figure: 0; 1; τ; ττ; .]

2. We hide observations as prescribed by h to obtain the bundle [figure: ∫ T; L^{∗}; ht]

that collapses ∫ T into ε.

3. We pullback along h to obtain the first-projection bundle [figure: h^{∗} ∫ T; A^{+}; h^{∗}(ht)]

where h^{∗} ∫ T is the category

[figure: (τ, 0); (ττ, 0); (τττ, 0); ⋯; ···; (τ, 1); (ττ, 1); (τττ, 1); ⋯]  (5)

4. Finally, we unfold (5) to obtain the synchronisation tree

\xymatrix{ &  &  &  & ⋯ \\  &  &  & 000 \ar[r] \ar[ur] & ⋯ \\  &  & 00 \ar[r]_{τ} \ar[ur]^{τ} & 001 \ar[r] & ⋯ \\  & 0 \ar[r]_{τ} \ar[ur]^{τ} & 01 \ar[r]_{τ} & 011 \ar[r] & ⋯ \\ ∗ \ar[r]_{τ} \ar[ur]^{τ} & 1 \ar[r]_{τ} & 11 \ar[r]_{τ} & 111 \ar[r] & ⋯ & .}

Note that the saturation is actually taking place in steps (2) and (3), which correspond to the adjunction

Cat/ℙ [figure: Σ_{h}; ⊤; h^{∗}]Cat/ℚ

related to the treatment of existential quantifiers as adjoints (see [15]).

We have remarked in (4) that the saturation monad can be given explicitly by considering weak computation paths. In order to obtain a deeper understanding of the saturation process, we study weak computation paths in detail. In particular, we show that every weak computation path admits a universal factorisation as a weak path extension followed by a (strong) computation path. Indeed, for x : D_{h}(p) [figure]D_{h}X (p ∈ ℙ, X ∈ ℙ̂) in Cat/ℚ,

• let \overline{x} : \overline{p} [figure] X in ℙ̂ be x(id_{p}), and

• define x̃ : D_{h}(p) [figure] D_{h}(\overline{p}) by x̃(e) =^{def} x(e) and x̃(e [figure: ϵ] e′) =^{def} x(ϵ).

Then, we have the following factorisation lemma.

Lemma 3.1 For x : D_{h}(p) [figure] D_{h}X (p ∈ ℙ, X ∈ ℙ̂) in Cat/ℚ, 1. x = D_{h}(\overline{x}) ∘ x̃; and

2. for y : q [figure] X (q ∈ ℙ) in ℙ̂ and f : D_{h}(p) [figure] D_{h}(q) in Cat/ℚ such that x = D_{h}(y) ∘ f, there exists a unique e : \overline{p} [figure] q in ℙ such that f = D_{h}(e) ∘ x̃ and \overline{x} = y ∘ e.

It follows that, for q ∈ ℙ and X ∈ ℙ̂, the family

\xymatrix{\{ X(p) × Cat/ℚ (D_{h}(q), D_{h}(p)) \ar[r] & T_{h}(X)(q) \}_{p∈ℙ}}
\xymatrix{(x, f) \ar@{|->}[r] & D_{h}(x) ∘ f}

exhibits T_{h}(X)(q) as the coend

∫ ^{p∈ℙ} X(p) × Cat/ℚ (D_{h}(q), D_{h}(p)) ,  (6)

and hence that T_{h} is a left Kan extension of the functor ℙ [figure]ℙ̂ : p [figure] Cat/ℚ (D_{h}(−), D_{h}(p)) along the Yoneda embedding. We have shown the following result.

Theorem 3.2 For every functor h, the saturation monad T_{h} is cocontinuous.

Properties. For h : ℙ [figure] ℚ, the following hold.

1. A map f : X [figure] Y in Weak(h) is W_{h}Y^{∘}-open iff the map f : D_{h}X [figure] D_{h}Y in Cat/ℚ is D_{h}Y^{∘}-open.

2. For a map f in ℙ̂, T_{h}(f) is Y^{∘}-open iff D_{h}(f) is D_{h}Y^{∘}-open.

3. T_{h} preserves Y^{∘}-open maps (as so does every cocontinuous functor, see [9, 6]) and hence Y^{∘}-open map bisimilarity implies h-bisimilarity.

The last statement is an abstract expression of the result “strong bisimilarity implies weak bisimilarity (observational congruence)”.

Sharp functors. A functor h is said to be sharp whenever the multiplication of the saturation monad T_{h} is pointwise Y^{∘}-open (cf. ‘Preservation Properties (2)’, Section 1). The notion of bisimilarity with respect to sharp functors has interesting properties.

Proposition 3.3 Let h : ℙ [figure] ℚ.

1. If two presheaves over ℙ are h-bisimilar then their saturations are Y^{∘}- open map bisimilar. In addition, if h is sharp then the converse also holds.

2. For a sharp functor h, h-bisimilarity is a congruence with respect to sums.

In presheaf models in which sums interpret choice (as it is the case in Â^{+}) the last result shows that the notion of h-bisimilarity, for sharp functors h, is closer to observational congruence rather than to weak bisimilarity. We will see in the next section that this is indeed the case.

A characterisation of sharp functors. Assuming a functor h : ℙ [figure] ℚ, we first see how to understand the components of the multiplication μ of the monad T_{h} as derived from composition in Cat/ℚ.

Define profunctors V, W : ℙ [figure: +] ℙ, in other words presheaves V, W over ℙ^{op} × ℙ, as follows:

V (p, p′) =^{def} Cat/ℚ (D_{h}(p′), D_{h}(p)) ,
W (p, p′) =^{def} ∫ ^{q} V (q, p′) × V (p, q) .

Define γ to be the natural transformation from W to V (so a map in { \atop ℙ^{op} × ℙ}) such that

γ_{p,p′} : W (p, p′) [figure] V (p, p′)

is induced by composition.

Recalling the coend formula (6) for T_{h} applied to X ∈ ℙ̂, we see that

T_{h}(X)(p) = ∫ ^{q} X(q) × V (q, p) .

Applying the coend formula for T_{h} twice, using “Fubini” [14] to interchange coends and that products in Set preserve colimits, we obtain

T_{h}^{2}(X)(p) = ∫ ^{q} X(q) × W (q, p) .

A calculation shows that the natural transformation with p-components

∫ ^{q} X(q) × γ_{q,p} : (T_{h}^{2}X)(p) [figure] (T_{h}X)(p)

induced by composition in Cat/ℚ is the multiplication μ_{X}. (In other words μ_{X} = γ∗X, where ∗ is the horizontal composition of 2-cells in the bicategory of profunctors [3], in this case “whiskering” the 2-cell γ : W [figure] V with the one cell X : 1 [figure: +] ℙ.)

Thus we see μ_{X} as the result of applying the cocontinuous functor

\begin{matrix}{ \atop ℙ^{op} × ℙ} & [figure] & ℙ̂ \\ U & [figure] & (p [figure] ∫^{q} X(q) × U(q, p)) \end{matrix}

to the map γ : W [figure] V. Hence if γ is open as a map in { \atop ℙ^{op} × ℙ}, then for any X ∈ ℙ̂ the multiplication μ_{X} will be open. But γ will be open iff it is open in each argument separately, yielding conditions corresponding to the covariant and contravariant arguments:

Covariant openness. Fixing p, we require that γ_{p,−} : W (p, −) [figure] V (p, −) is open in ℙ̂.

Contravariant openness. Fixing p′, we require that γ_{−,p′} : W (−, p′) [figure] V (−, p′) is open in ℙ̂^{op}.

These two conditions are sufficient for the functor h to be sharp. The first condition (covariant openness) is also necessary—instantiating the presheaf X to a representable we see that the openness of μ_{X} amounts to the first condition. The following “fill-in” condition can be shown to be sufficient to ensure covariant openness:

\xymatrix{D_{h}(p) \ar[d]_{x} \ar[r]^{D_{h}(e)} & D_{h}(q) \ar[ddr]^{z} \ar@{.>}[d]_{x′} \\ D_{h}(p′) \ar[drr]_{y} \ar@{.>}[r]_{D_{h}(e′)} & D_{h}(q′) \ar@{.>}[dr]_{w} \\  &  & D_{h}(o) & ,}  (7)

meaning if the outer arrows commute in Cat/ℚ then one can fill-in with the dotted arrows. All arrows but D_{h}(e) and D_{h}(e′) may be weak morphisms. The arrow x : D_{h}(p) [figure] D_{h}(p′) is assumed extreme in the sense that x(id_{p}) = id_{p′}. A fill-in condition dual to (7) can be proved to always hold ensuring contravariant openness in general.

In summary, we have the following result.

Theorem 3.4 1. The functor h is sharp iff for all p ∈ ℙ the map γ_{p,−} : W (p, −) [figure] V (p, −) is open in ℙ̂.

2. The functor h is sharp if the fill-in condition (7) above holds.

4 Examples

4.1 Synchronisation trees

Observational congruence. We study bisimilarity with respect to the hiding functor h = ˆ( ) : A^{+} [figure] L^{∗} where A = L + {τ}.

The (Kleisli) category Weak(h) is (equivalent to) the category with objects given by synchronisation trees and morphisms T_{0} [figure] T_{1} given by functions f : S_{0} [figure] S_{1} between states that preserve the initial state (i.e., f(∗_{0}) = ∗_{1}) and are such that

1. ∗_{0} [figure: a]_{0} s implies ∗_{1} [figure: a]_{1} f(s);

2. ∗_{0} ≠ s [figure: a]_{0} s′ implies f(s) [figure: â]_{1} f(s′).

We have the following characterisation of h-bisimilarity (cf. [5]).

Proposition 4.1 For h = ˆ( ) : A^{+} [figure]L^{∗}, h-bisimilarity coincides with observational congruence.

It is well-known that two synchronisation trees are observationally congruent if, after the saturation construction, they are strongly bisimilar (cf. [16]). This property is reflected here by the fact that the hiding functor h is sharp. Indeed, referring to the diagram (7) for the fill-in condition, suppose that e represents the string extension q = ps. Fill-in by taking: q′ = p′s and e′ the witness to this extension; the map x′ such that x′(ps_{0}) = p′s_{0} and x′(p_{0}) = x(p_{0}) when p_{0} ≤ p; the map w such that w(p′s_{0}) = z(ps_{0}) and w(p′_{0}) = y(p′_{0}) if p′_{0} ≤ p′.

Weak bisimulation. Let A be L + {τ}. For h the hiding functor ˆ( ) : A^{∗} [figure] L^{∗}, the (Kleisli) category Weak(h) is (equivalent to) the category with objects given by synchronisation forests and morphisms T_{0} [figure] T_{1} given by functions f : S_{0} [figure] S_{1} between the corresponding sets of states such that

s [figure: a] s′ implies f(s) [figure: â] f(s′) (cf. [17]).

Proposition 4.2 For h = ˆ( ) : A^{∗} [figure] L^{∗}, h-bisimilarity between synchronisation trees coincides with weak bisimulation.

As for observational congruence, one can verify that also in this case the hiding functor ˆ( ) : A^{∗} [figure] L^{∗} is sharp.

4.2 Event structures

In this section we begin the study of weak bisimulation for event structures. The category ES_{A}^{s} fully embeds in the presheaf category \begin{matrix} \\ Pom & sA \end{matrix}. It is natural to consider the hiding functor h : Pom_{A}^{s} [figure] (Pom_{L}^{s})_{⊥} which removes from a pomset P all the events which are labelled τ. In particular if all the events of P are labelled τ, h(P) is the empty pomset that we denote as ⊥.

For a pomset P, write P↓ for the partial order of sub-pomsets of P.

Definition 4.3 Given a monotone function f : P↓ [figure] Q↓, we say that f is extreme if f(P) = Q (cf. the assumption on the fill-in condition (7)), and we say that f is h-respecting if, for every P′ ⊆ P, h(P′) is isomorphic to h(f(P′)).

Extreme, h-respecting maps induce isomorphisms between pomsets with τevents hidden.

Proposition 4.4 For every f : P ↓ [figure] Q↓ extreme and h-respecting there exists a (necessarily unique) isomorphism f′ : h(P) [figure] h(Q) in (Pom_{L}^{s})_{⊥} such that for every P′ ⊆ P, f′(h(P′)) = h(f(P′)).

Definition 4.5 Define WPom_{A}^{s} to be the category with the same objects as Pom_{A}^{s} and arrows h-respecting monotone functions.

The category WPom_{A}^{s} corresponds to a category of pomsets and weak morphisms.

Proposition 4.6 The category WPom_{A}^{s} is isomorphic to the full subcategory of Weak(h) with objects given by the images under the Yoneda embedding of the pomsets in Pom_{A}^{s}.

We can now show that the hiding functor h is sharp hence by Proposition 3.3 h-bisimilarity and Y^{0}-open bisimilarity after saturation coincide for presheaves over Pom_{A}^{s}. We show that h is sharp by verifying the fill-in condition of diagram (7). By Theorem 3.4, it is sufficient to verify that the fill-in condition holds in WPom_{A}^{s}. Adopting the same names for maps as in the fill-in diagram (7), we can (without loss of generality) assume that e is an inclusion of pomsets e : P ⊆ Q; otherwise modify Q to within isomorphism and z accordingly—a fill-in for the new diagram implies one for the old. In a similar way we may further assume that Q and P′ have disjoint sets of events. It is sufficient to get a fill-in for the situation when Q consists of the pomset P with only one additional event α; a fill-in for a general inclusion can be got from the fill-in’s from adding one (enabled) event at a time. Let C = {ϵ ∈ P | ϵ ≤ α}, the events in P on which α causally depends. We can identify downward-closed subsets of events of a pomset with its corresponding sub-pomset and, in particular, C with a pomset C ⊆ P.

Write Tau(R) for the τ-events of a pomset R. Now define the pomset Q′ to consist of α, the events of P′ and events Tau(P) with their original labels and ordered as follows. The events of P′ are ordered as in P′. The event α is to causally depend on precisely the events x(C) in P′. Suppose a τ-event ϵ of P causally depends on the subset of events P_{0} of P. Then in Q′ the τ-event ϵ is to causally depend on precisely the set of events h(x(P_{0})). The filling-in map e′ is just the inclusion of P′ in Q′. The remaining filling-in maps x′ and w are defined by

x′(Q_{0}) = \{ \begin{matrix}x(Q_{0}) & if α ∉ Q_{0} . \\ x(Q_{0} ∩ P) ∪ Tau(Q_{0}) ∪ \{α\} & if α ∈ Q_{0} . \end{matrix}

w(Q_{0}′) = y(Q_{0}′ ∩ P′) ∪ ⋃{z(Q_{0}) | α ∈ Q_{0} & x′(Q_{0}) ⊆ Q_{0}′} .

This concludes the verification that the hiding functor h : Pom_{A}^{s} [figure] (Pom_{L}^{s})_{⊥} is sharp.

For a pomset morphism f : P [figure] Q, we will write f↓: P↓ [figure] Q↓ for the monotone function defined as f↓ (R ⊆ P) = (f(R) ⊆ Q).

Definition 4.7 A hereditary history-preserving weak bisimulation, S, between two event structures E and F in ES_{A}^{s} is given by a set of spans

(x↓ [figure: α] P↓ [figure: β] y↓) ,

where x is a finite configuration of E, y a finite configuration of F, P a pomset in (Pom_{A}^{s})_{⊥} while α and β are two monotone functions. The initial span (∅↓ [figure] ⊥↓ [figure] ∅↓) must be in S and the following conditions need to be

met whenever (x↓ [figure: α] P↓ [figure: β] y↓) is an element of S:

1. If (x↓ [figure: α] P↓ [figure: β] y↓) ≠ (∅↓ [figure] ⊥↓ [figure] ∅↓), then α and β are extreme and h-respecting.

2. For m : Q [figure] P, we have (x′↓ [figure: α′] Q↓ [figure: β′] y′↓) ∈ S where α′ =^{def} α∘(m↓)

and β′ =^{def} β ∘ (m↓).

3. If the following square of monotone functions commutes

\xymatrix{P↓ \ar[r]^{α} \ar[d]_{m↓} & x↓ \ar@{^{(}->}[d] \\ Q↓ \ar[r]_{α′} & x′↓ & ,}

where m : P [figure]Q is a strict pomset morphism, x′ ⊇ x is a finite configuration of E and α′(Q) = x′, then there exists y′ ⊇ y and β′ :

Q↓ [figure] y↓ such that (x′↓ [figure: α′] Q↓ [figure: β′] y′↓) ∈ S and the following square commutes

[figure: P↓; β; m↓; y↓; Q↓; β′; y′↓; .]

4. As (3) above where α is swapped with β and x swapped with y.

If for every span (x↓ [figure] P↓ [figure] y↓) ∈ S, it is also the case that x = ∅ iff y = ∅ iff P = ⊥, then we say that S is an observational congruence.

Note that a hereditary history-preserving weak bisimulation between event structures E and F induces, by the action of the hiding functor h, a hereditary history-preserving bisimulation [1, 13] between h(E) and h(F).

Hereditary history-preserving observational congruence characterises hbisimilarity.

Theorem 4.8 Two event structures in ES_{A}^{s} are hereditary history-preserving observationally congruent if and only if they are h-bisimilar.

If h is extended in the obvious way to act on the empty pomset over A, then the version of the above theorem obtained by replacing “observationally congruent” by “weakly bisimilar” also holds.

The characterisation of Definition 4.7 for h-bisimilarity requires relating computations of the same shape in E and F rather than, more simply, matching only system states, i.e., configurations. For event structures regarded as presheaves over Pom_{A}, i.e., when we no longer restrict to strict morphisms, Definition 4.7 needs to be refined by considering augmentations of the configurations (cf. [26]) in any span. We believe, but lack a proof, that the corresponding hiding functor h : Pom_{A} [figure] (Pom_{L})_{⊥} is also sharp.

It is important to notice that it is only by embedding event structures in the presheaf category \begin{matrix} \\ Pom & sA \end{matrix} that we have been able to define the saturation monad for weak bisimulation which cannot be restricted to ES_{A}^{s}.

References

[1] M. Bednarczyk. Hereditary history preserving bisimulation or what is the power of the future perfect in program logics. Technical report, Polish Academy of Sciences, Gdansk, 1991.

[2] J. v. Bentham. Correspondence theory. In Handbook of Philosophical Logic, volume 2, pages 167–247. Reidel, 1984.

[3] F. Borceux. Handbook of categorical algebra I. Cambridge University Press, 1994.

[4] M. Bunge and M. Fiore. Unique factorisation lifting functors and categories of linearly-controlled processes. To appear in Mathematical Structures in Computer Science, 1999.

[5] I. Castellani. Bisimulation and abstraction homomorphisms. J. Comput. System Sci., 34(2-3):210–235, 1987.

[6] G. L. Cattani. Presheaf Models for Concurrency. PhD thesis, University of Aarhus, 1999. Forthcoming.

[7] G. L. Cattani, M. Fiore, and G. Winskel. A theory of recursive domains with applications to concurrency. In Proceedings of LICS’98, pages 214–225. IEEE Press, 1998.

[8] G. L. Cattani, I. Stark, and G. Winskel. Presheaf models for the π-calculus. In Proceedings of CTCS ’97, volume 1290 of LNCS, pages 106–126. Springer-Verlag, 1997.

[9] G. L. Cattani and G. Winskel. Presheaf models for concurrency. In Proceedings of CSL’96, volume 1258 of LNCS, pages 58–75. Springer-Verlag, 1997.

[10] J. Gray. Fibred and cofibred categories. In Proceedings of La Jolla Conference on Categorical Algebra, pages 21–83. Springer-Verlag, 1966.

[11] T. T. Hildebrandt, P. Panangaden, and G. Winskel. A relational model of non-deterministic dataflow. In Proceedings of CONCUR ’98, volume 1466 of LNCS, pages 613–628. Springer-Verlag, 1998.

[12] D. Husemoller. Fibre Bundles. Springer-Verlag, 1994.

[13] A. Joyal, M. Nielsen, and G. Winskel. Bisimulation from open maps. Information and Computation, 127(2):164–185, 1996.

[14] S. Mac Lane. Categories for the Working Mathematician. Springer-Verlag, 1971.

[15] S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic. Springer-Verlag, 1992.

[16] R. Milner. Communication and Concurrency. Prentice Hall, 1989.

[17] M. Nielsen and A. Cheng. Observe behaviour categorically. In Proceedings of FST&TCS ’95, volume 1026 of LNCS, pages 263–278. Springer-Verlag, 1995.

[18] V. Pratt. Modelling concurrency with partial orders. International Journal of Parallel Processing, 15:33–71, 1986.

[19] V. Sassone, M. Nielsen, and G. Winskel. Models for concurrency: towards a classification. Theoretical Computer Science, 170(1-2):297–348, 1996.

[20] R. Street. Cosmoi of internal categories. Trans. Amer. Math. Soc., 258(2):271– 318, 1980.

[21] G. Winskel. Synchronisation trees. Theoretical Computer Science, 34:33–82, 1985.

[22] G. Winskel. A category of labelled petri nets and compositional proof system. In Proceedings of LICS’88, pages 142–154. IEEE Press, 1988.

[23] G. Winskel. A presheaf semantics of value-passing processes (extended abstract). In Proceedings of CONCUR’96, volume 1119 of LNCS, pages 98–114. Springer-Verlag, 1996.

[24] G. Winskel and M. Nielsen. Models for concurrency. In Handbook of logic in computer science, Vol. 4, Oxford Sci. Publ., pages 1–148. Oxford Univ. Press, 1995.

[25] G. Winskel and M. Nielsen. Models for concurrency. In Semantics and Logics of Computation. Cambridge University Press, 1997.

[26] G. Winskel and M. Nielsen. Presheaves as transition systems. In POMIV 96, volume 29 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 129–140. AMS, 1997.

Recent BRICS Report Series Publications

RS-99-14 Marcelo P. Fiore, Gian Luca Cattani, and Glynn Winskel. Weak Bisimulation and Open Maps. May 1999. To appear in Longo, editor, Fourteenth Annual IEEE Symposium on Logic in Computer Science, LICS ’99 Proceedings, 1999.

RS-99-13 Rasmus Pagh. Hash and Displace: Efficient Evaluation of Minimal Perfect Hash Functions. May 1999. 11 pp. A short version to appear in Algorithms and Data Structures: 6th International Workshop, WADS ’99 Proceedings, LNCS, 1999.

RS-99-12 Gerth Stølting Brodal, Rune B. Lyngsø, Christian N. S. Pedersen, and Jens Stoye. Finding Maximal Pairs with Bounded Gap. April 1999. 31 pp. To appear in Combinatorial Pattern Matching: 10th Annual Symposium, CPM ’99 Proceedings, LNCS, 1999.

RS-99-11 Ulrich Kohlenbach. On the Uniform Weak König’s Lemma. March 1999. 13 pp.

RS-99-10 Jon G. Riecke and Anders B. Sandholm. A Relational Account of Call-by-Value Sequentiality. March 1999. 51 pp. To appear in Information and Computation, LICS ’97 Special Issue. Extended version of an article appearing in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings, 1997, pages 258–267. This report supersedes the earlier BRICS report RS-97-41.

RS-99-9 Claus Brabrand, Anders Møller, Anders B. Sandholm, and Michael I. Schwartzbach. A Runtime System for Interactive Web Services. March 1999. 21 pp. Appears in Mendelzon, editor, Eighth International World Wide Web Conference, WWW8 Proceedings, 1999, pages 313–323 and Computer Networks, 31:1391–1401, 1999.

RS-99-8 Klaus Havelund, Kim G. Larsen, and Arne Skou. Formal Verification of a Power Controller Using the Real-Time Model Checker Uppaal. March 1999. 23 pp. To appear in Katoen, editor, 5th International AMAST Workshop on Real-Time and Probabilistic Systems, ARTS ’99 Proceedings, LNCS, 1999.

RS-99-7 Glynn Winskel. Event Structures as Presheaves—Two Representation Theorems. March 1999. 16 pp.