BRICS RS-97-4 Blute et al.: Bisimulation for Labelled Markov Processes BRICS

Basic Research in Computer Science

Bisimulation for Labelled Markov Processes

Richard Blute Josée Desharnais Abbas Edalat Prakash Panangaden

BRICS Report Series RS-97-4

ISSN 0909-0878 March 1997 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1997, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

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

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

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

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

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

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

This document in subdirectory RS/97/4/

Bisimulation for Labelled Markov Processes

Richard Blute^{∗}

Department of Mathematics

University of Ottawa Ottawa, Ontario, Canada

 rblute@mathstat.uottawa.ca

Abbas Edalat^{†}

Department of Computing

Imperial College London, UK

      ae@doc.ic.ac.uk

Josée Desharnais^{∗}

School of Computer Science McGill University Montreal, Quebec, Canada

                                   desharna@cs.mcgill.ca

Prakash Panangaden^{∗}^{‡}

BRICS Aarhus University Aarhus, Denmark

                                   prakash@cs.mcgill.ca

Full version of the paper presented at LICS 97

Abstract

In this paper we introduce a new class of labelled transition systems - Labelled Markov Processes - and define bisimulation for them. Labelled Markov processes are probabilistic labelled transition systems where the state space is not necessarily discrete, it could be the reals, for example. We assume that it is a Polish space (the underlying topological space for a complete separable metric space). The mathematical theory of such systems is completely new from the point of view of the extant literature on probabilistic process algebra; of course, it uses classical ideas from measure theory and Markov process theory. The notion of bisimulation builds on the ideas of Larsen and Skou and of Joyal, Nielsen and Winskel. The main result that we prove is that a notion of bisimulation for Markov processes on Polish spaces, which extends the Larsen-Skou definition for discrete systems, is indeed an equivalence relation. This turns out to be a rather hard mathematical result which, as far as we know, embodies a new result in pure probability theory. This work heavily uses continuous mathematics which is becoming an important part of work on hybrid systems.

∗Research supported in part by NSERC.

†Research supported by EPSRC, UK.

‡On Leave from McGill University.

1 Introduction

Computer Science has been increasingly expanding its borders to include subjects normally considered part of physics, dynamical systems or control theory, most notably in areas like “hybrid systems”. One can look at volume 1066 of Springer-Verlag Lecture Notes In Computer Science [AHS96] for examples of recent work on Hybrid systems. Ideas from continuous mathematics: differential equations, probability theory, stochastic processes, systems theory and others are becoming part of the mathematical toolkit of concurrency theorists. In the area of performance evaluation of computer systems the use of stochastic Petri nets is quite widespread, one of the early papers is [Sif77]. Hillston has pioneered the use of process algebra in performance evaluation [Hil94]. Systems like Hytech [HHWT95] and the Uppaal system [BLL^{+}96] have appeared based on hybrid systems and real-time systems respectively and use process equivalences very fruitfully.

A new ingredient offered by computer science (apart from the manifest idea of computability or effectiveness) to these subjects is compositionality. Thus while the theory of stochastic processes [CM65] is concerned with a detailed analysis of the time evolution of systems behaving according to probabilistic laws very little is ever done to analyze the behaviour of coupled systems in a systematic way. Computer scientists have stressed compositionality as a way to attack the formidable intricacy of the systems they have dealt with. For example, in Hillston’s work, compositionality is the key contribution of her approach to performance modelling.

The notion of bisimulation is central to the study of concurrent systems. While there are a bewildering variety of different equivalence relations between processes (two-way simulation, trace equivalence, failures equivalence and many more) bisimulation enjoys some fundamental mathematical properties, most notably its characterization as a fixed-point, which make it the most discussed process equivalence. Of course there are a lot of different variants of bisimulation itself! In the present paper we are not so much concerned with adjudicating between the rival claims of all these relations, but rather, we are concerned with showing how to extend these ideas to the world of continuous state spaces. As we shall see below, new mathematical techniques (from the point of view of extant work in process algebra) have to be incorporated to do this. Once the model and the new mathematical ideas have been assimilated, the whole gamut of process equivalences can be studied and argued about.

From an immediate practical point of view, bisimulation can be used to reason about probabilistic, continuous state-space systems (henceforth Markov processes) in the following simple way. One often “discretizes” a continuous system by partitioning the state space into a few equivalence classes. Usually one has some intuition that the resulting discrete system “behaves like” the original continuous system. This can be made precise by our notion of bisimulation. It is also the case that some systems cannot be discretized, once again, one can formalize what this means via bisimulation.

The present paper develops a notion of labelled Markov process which is meant ultimately to be part of a theory of interacting dynamical systems. The key technical contribution is the development of a notion of bisimulation for processes which have continuous state spaces but make discrete temporal steps. These are called discrete-time Markov processes. If the state space is also discrete the phrase “Markov chain” is used. The adjective “Markovian” signifies that the transitions are entirely governed by the present state rather than by the past history of the system. The interaction is governed by “labels” in the manner now familiar from process algebra [Hoa85, Mil80, Mil89].

In brief, a labelled Markov process is as follows. There is a set of states and a set of labels. The system is in a state at a point in time and moves between states. Which state it moves to is governed by which interaction with the environment is taking place and this is indicated by the labels. The system evolves according to a probabilistic law. If the system interacts with the environment by synchronizing on a label it makes a transition to a new state governed by a transition probability distribution. So far, this is essentially the model developed by Larsen and Skou [LS91] in their very important and influential work on probabilistic bisimulation. They specify the transitions by giving, for each label, a probability for going from one state to another. Bisimulation then amounts to matching the moves with matching probabilities as well.

In the case of a continuous state space, however, one cannot just specify transition probabilities from one state to another. In most interesting systems all such transition probabilities would be zero! Instead one must work with probability densities. In so doing, one has to confront the major issues that arose when probability theory was first formalized, such as the existence of subsets for which the notion of probability does not make sense. In the appendix we provide a rapid recapitulation of ideas from probability and measure theory. In the present case we have to introduce a notion of sets for which “probabilities make sense” (i.e. a σ-algebra) and instead of talking about probabilities of going from a state s to another state s′, we have to talk about going from a state s to a set of states A.

The notion of bisimulation for these systems is a generalization of the definition of Larsen and Skou, which, as we shall argue in the next section, is a compelling, natural notion. Unfortunately this definition cannot be adapted in any simple way to the continuous case. One cannot even use their basic terminology for bisimulation because their definition is inextricably wound up in the notion of state-to-state transition probabilities. Furthermore, once the correct generalization is given it turns out to be a formidable technical problem to even show that bisimulation is an equivalence relation. This is solved by a construction due to Edalat and is given in detail in an appendix. In fact the construction heavily relies on properties that are not true for measure spaces in general. We have assumed a Polish space structure. A Polish space is a topological space which can be given a metric structure which generates the topology and such that the metric is complete and separable, i.e. there is a countable basis for the topology. In the classical study of Markov processes metric ideas play a significant role [Par67]. In any example of physical interest, the spaces will have this Polish structure, indeed they will usually come as metric spaces. Any discrete space is Polish and any of the closed subspaces of ℝ^{n} will be as well.

The definition of bisimulation is inspired by the paper of Joyal, Nielsen and Winskel [JNW96] which provides a general categorical view of what bisimulation is in terms of certain special morphisms called open maps. It is not straightforward to adapt this to the probabilistic case. For discrete systems this has been done by Cheng and Nielsen [CN95] using infinitesimals^{1}. Unfortunately one still needs to know how to construct pullbacks in the underlying category and for this one has to rely on the basic construction given in [Eda96]. It also turns out that our notion of bisimulation is precisely the notion of coalgebra homomorphism [dVR].

The rest of this paper is organized as follows. We describe some examples of systems with continuous state spaces in the next section. We then recapitulate the work of Larsen and Skou on discrete systems. The next two sections are concerned with the definition of labelled Markov processes and bisimulation. The last sections discuss related work and conclusions.

1One can actually do this without talking about infinitesimals [Win96].

2 Two Examples of Processes

We begin with a simple example, more for introducing terminology than for any intrinsic interest. Imagine a system with two labels {a, b}. The state space is the real plane, ℝ^{2}. When the system makes an a-move from state (x_{0}, y_{0}) it jumps to (x, y_{0}) where the probability distribution for x is given by the density K_{α} exp(−α(x − x_{0})^{2}), where K_{α} = \sqrt{α/π} is the normalizing factor. When it makes a b-move it jumps from state (x_{0}, y_{0}) to (x_{0}, y) where the distribution of y is given by the density function K_{β} exp(−β(y − y_{0})^{2}). The meaning of these densities is as follows. The probability of jumping from (x_{0}, y_{0}) to a state with x-coordinate in the interval [s, t] under an amove is ∫_{s}^{t} K_{α} exp(−α(x − x_{0})^{2})dx. Note that the probability of jumping to any given point is, of course, 0. In this system the interaction with the environment controls whether the jump is along the x-axis or along the y-axis but the actual extent of the jump is governed by a probability distribution. Interestingly, this system is bisimilar to a one-state system which can make a or b moves. Thus, from the point of view of an external observer, this system has an extremely simple behaviour. The more complex internal behaviour is not externally visible. The point of a theory of bisimulation that encompasses such systems is to say this sort of thing. Of course this example is already familiar from the nonprobabilistic setting; if there is a system in which all trasitions are always enabled it will be bisimilar (in the traditional sense) to a system with one state.

Now we consider a system which cannot be reduced to a discrete system. There are three labels {a, b, c}. The state space is ℝ. The following physical description is for “local colour” and is mathematically unimportant. The state gives the pressure of a gaseous mixture in a tank in a chemical plant. The environment can interact by (a) simply measuring the pressure, or (b)it can inject some gas into the tank, or (c) it can pump some gas from the tank. The pressure fluctuates according to some thermodynamic laws depending on the reactions taking place in the tank. With each interaction, the pressure changes according to three different probability density functions, say f(p_{0}, p), g(p_{0}, p) and h(p_{0}, p) respectively, with nontrivial dependence on p_{0}. There are in addition two threshold values p_{h} and p_{l}. When the pressure rises above p_{h} the interaction labelled b is disabled, and when the pressure drops below p_{l} the interaction labelled c is disabled. It is tempting to model this as a three state system, with the continuous state space partitioned by the threshold values. Unfortunately one cannot assign unique transition probabilities to these sets of states for any choices of f, g and h; only if very special uniformity conditions are obeyed can one do this.

3 Discrete Probabilistic Systems

In this section we recapitulate the Larsen-Skou definition of probabilistic bisimulation [LS91]. The systems that they consider will be referred to as labelled Markov chains in the present paper.

Definition 3.1 A labelled Markov chain is a quadruple (S, L, C_{l}, P_{l}), where S is a countable set of states, L is a set of labels, and for each l ∈ L we have a subset C_{l} of S, a function, P_{l}, called a transition probability matrix,

P_{l} : C_{l} × S ⟶ [0, 1]

satisfying the normalization condition

∀l ∈ L, s ∈ C_{l}.Σ_{s′∈S}P_{l}(s, s′) = 1.

If we have the weaker property

∀l ∈ L, s ∈ C_{l}.Σ_{s′∈S}P_{l}(s, s′) ≤ 1

we call the system a partial labelled Markov chain.

The sets C_{l} are the sets of states that can do an l-action. If we have partial labelled Markov chains then we can just dispense with the C_{l} sets. In what follows we suppress the label set, i.e. we assume a fixed label set given once and for all.

Definition 3.2 Let T = (S, P_{l}) be a labelled Markov chain. Then a probabilistic bisimulation ≡_{p}, is an equivalence on S such that, whenever s ≡_{p} t, the following holds:

∀l ∈ L.∀A ∈ S/ ≡_{p}, Σ_{s′∈A}P_{l}(s, s′) = Σ_{s′∈A}P_{l}(t, s′).

Two states s and t are said to be probabilistically bisimilar (s ∼_{LS} t) in case (s, t) is contained in some probabilistic bisimulation.

Intuitively we can read this as saying that two states are bisimilar if we get the same probability when we add up the transition probabilities to all the states in an equivalence class of bisimilar states. The adding up is crucial – the probabilities are not just another label. The subtlety in the definition is that one has to somehow know what states are probabilistically bisimilar in order to know what the equivalence classes are, which in turn one needs in order to compute the probabilities to match them appropriately. In fact a very natural notion of probabilistic synchronization trees yields a model of a probabilistic version of CCS with both probabilistic branching and nondeterministic branching. If one looks just at probabilistic branching, equality is precisely the Larsen-Skou notion of bisimulation [BK96].

The paper by Larsen and Skou does much more than just define bisimulation. They introduce the notion of testing a probabilistic process and associating probabilities with the possible outcomes. They then introduce a notion of testable properties. The link with probabilistic bisimulation is that two processes are probabilistically bisimilar precisely when they agree with the results of all tests. They also introduce a probabilistic modal logic and show that bisimulation holds exactly when two processes satisfy the same formulas.

One slight awkwardness in the Larsen-Skou definition is that when one compares two processes one has to combine the state sets and define probabilistic bisimulation on the combined states. This is a minor point but the reader should keep this in mind when reading the proofs below.

4 A Category of Markov Processes

A Markov process is a transition system with the property that the transition probabilities depend only on the current state and not on the past history of the process. We will consider systems where there is an interaction with the environment described by a set of labels as in process algebra. For each fixed label the system may undergo a transition governed by a transition probability. One could have a new set of possible states at every instant but, for simplicity, we restrict to a single state space.

We will organize the theory in categorical terms with objects being transition systems and morphisms being simulations. Bisimulation is most easily thought of in these terms. This presentation will also allow us to compare the theory with the more traditional theory of non-probabilistic processes, see, for example, the handbook article by Winskel and Nielsen [WN95].

In formulating the notion of Markov processes we need to refine two concepts that were used in the discrete case. First we cannot just define transition probabilities between states; except in rare cases such transition probabilities are zero. We have to define transition probabilities between a state and a set of states. Second, we cannot define transition probabilities to any arbitrary set of states; we need to identify a family of sets for which transition probabilities can be sensibly defined. These are the measurable sets. Thus in addition to specifying a set of states we need to specify a σ-algebra on the set of states [Ash72, Bil79, Hal74, KT66, Rud66]

A key ingredient in the theory is the transition probability function.

Definition 4.1 A transition probability function on a measurable space (X, Σ) is a function T : X × Σ ⟶ [0, 1] such that for each fixed x ∈ X, the set function T (x, ·) is a (sub)probability measure and for each fixed A ∈ Σ the function T (·, A) is a measurable function.

One interprets T (x, A) as the probability of the system starting in state x making a transition into one of the states in A. The transition probability is really a conditional probability; it gives the probability of the system being in one of the states of the set A after the transition, given that it was in the state x before the transition.

It will turn out to be convenient to work with sub-probability functions; i.e. with functions where T (x, X) ≤ 1 rather than T (x, X) = 1. The mathematical results go through in this extended case and the resulting categories are often nicer but the stochastic systems studied in the literature are usually only the very special version where T (x, X) is either 1 or 0. In fact what is often done is that a state x with no possibility of making a transition is modelled by having a transition back to itself. For questions concerning which states will eventually be reached (the bulk of the analysis in the traditional literature) this is convenient. If, however, we are modelling the interactions that the system has with its environment it is essential that we make a distinction between a state which can make a transition and one which cannot.

The key mathematical construction requires a Polish space structure on the set of states. Thus instead of imposing an arbitrary σ-algebra structure on the set of states we will require that the set of states be a Polish space and the σ-algebra be the Borel algebra generated by the topology.

Definition 4.2 A partial, labelled, Markov process with label set L is a structure (S, Σ, {k_{l} | l ∈ L}), where S is the set of states, which is assumed to be a Polish space, and Σ is the Borel σ-algebra on S, and

∀l ∈ L, k_{l} : S × Σ ⟶ [0, 1]

is a transition sub-probability function. We are usually interested in the following special case called a labelled Markov process. We have a partial, labelled, Markov process as above and a predicate Can on S × L such that for every (x, l) ∈ Can we have k_{l}(x, X) = 1 and for every (x, l) ∉ Can we have k_{l}(x, X) = 0.

We will fix the label set to be some L once and for all. The resulting theory is not seriously restricted by this. We will write just (S, Σ, k_{l}) for partial, labelled, Markov processes instead of the more precise (S, Σ, ∀l ∈ L.k_{l}). In case we are talking about discrete systems we will use the phrase “labelled Markov chain” rather than “discrete, labelled, Markov process”.

In a (partial), labelled, Markov chain the set of states is countable, one can easily define a metric so that each point is an open set and the space is complete and obviously seperable, the Borel σ-algebra is then the entire powerset and the transition probabilities are given by a L-indexed family of functions ∀l ∈ L.P_{l} : S × S ⟶ [0, 1] satisfying the conditions required of a (sub)probability distribution. From this presentation we can construct the k_{l} in the following way k_{l}(s, σ) =^{def} ∑_{s′∈σ} P_{l}(s, s′). We use the phrase “transition function” for an object of type S × Σ ⟶ [0, 1] and “transition matrix” for an object of type S × S ⟶ [0, 1]. A probabilistic transition system as defined by Larsen and Skou is precisely a labelled Markov chain. The partial notion has been used by Cheng and Nielsen [CN95] to give an open maps [JNW96] presentation of bisimulation.

In order to define a category of Markov processes we define simulation morphisms between processes. Intuitively a simulation says that a simulating process can make all the transitions of the simulated process with greater probability than in the process being simulated.

Definition 4.3 A simulation morphism f between two partial, labelled, Markov processes, (S, Σ, k_{l}) and (S′, Σ′, k′_{l}) is a measurable function f : (S, Σ) ⟶ (S′, Σ′) such that

∀l ∈ L.∀x ∈ S.∀σ′ ∈ Σ′.k_{l}(x, f^{−1}(σ′)) ≤ k′_{l}(f(x), σ′).

One could have defined simulation to be continuous, however, the simulations play a secondary role in the present paper and we will just require them to be measurable ^{2} We do at least require this for the definition to make sense since without f being measurable we would not be guaranteed that f^{−1}(σ′) is measurable.

This notion extends the standard notion of simulation of labelled transition systems [WN95] in the following way. Given a partial, labelled, Markov chain, (S, P_{l}) we can define a labelled transition system (lts) with the same label set as follows. We take the same set of states S and we define a labelled transition relation →⊆ (S × L × S) by (s, l, s′) ∈→ ⟺ P_{l}(s, s′) > 0. Given two labelled transition systems, (S_{1}, →_{1}) and (S_{2}, →_{2}), a function f : S_{1} ⟶ S_{2} is a simulation morphism if ∀s ∈ S_{1}.s ⟶^{l} s′ ⇒ f(s) ⟶^{l} f(s′). We cannot do this for Markov processes because we can easily have systems where all the point-to-point transition probabilities are zero but the Markov process is nontrivial because the transition probabilities are nonzero to “larger” sets.

Proposition 4.4 Given two partial, labelled, Markov chains, a simulation morphism between them is also a simulation morphism between the associated labelled transition systems.

Proof (sketch). Suppose that we have two partial, labelled, Markov chains (S, Σ, k_{l}) and (S′, Σ′, k′_{l}) with f a simulation morphism from S to S′. Now suppose that in the associated lts the transition s_{1} ⟶^{l} s_{2} is possible. This means that k_{l}(s_{1}, {s_{2}}) > 0 so since f is a morphism we must have that k′_{l}(f(s_{1}), {f(s_{2})}) ≥ k_{l}(s, f^{−1}(f(s_{2}))) ≥ k_{l}(s_{1}, {s_{2}}) > 0; hence in the lts s_{1} ⟶^{l} s_{2} is possible.

5 Bisimulation for Markov Processes

The definition of bisimulation is very heavily influenced by the ideas of Joyal, Nielsen and Winskel [JNW96]. The idea is to identify a class of special systems called “observations” or “observable paths” or better still “observable path shapes”, and to define bisimulation as a relation satisfying a kind of path lifting property, the so-called “open maps”.

2In older texts, such as Halmos [Hal74] or Rudin [Rud66] measurable is defined to mean that the inverse image of an open set is measurable. This means that the composite of two measurable functions need not be measurable. Our definitions are standard and, of course with this definition the composite of two measurable functions is measurable.

What one can prove for ordinary labelled transition systems is that if we take paths to be labelled paths in the usual sense then the open maps are morphisms that satisfy a condition called the “zigzag” condition^{3}. We essentially want to say that there is a “zigzag relation”. One can talk about relations by talking about spans. A span in any category between an object S_{1} and another object S_{2} is a third object T together with morphisms from T to both S_{1} and S_{2}. One can think of this in the category fo Sets as viewing a relation as a set of ordered pairs with the morphisms being the projections.

Bisimulation is then defined to hold between two systems if they are connected by a span of zigzags. In our case the zigzag condition is easy to state and it is easy to see that it corresponds to Larsen-Skou bisimulation in the case of partial, labelled Markov chains. For partial, labelled Markov processes it will be our definition of bisimulation. From now on, we assume that all systems are partial and we will stop writing the adjective “partial” explicitly.

Definition 5.1 The objects of the category LMP are labelled Markov processes, having L as set of labels, with simulations as the morphisms. The category of labelled, Markov chains is written LMC and is the full subcategory of LMP that includes only the labelled, Markov chains as objects.

The key concept is the following.

Definition 5.2 A morphism f from (S, Σ, k_{l}) to (S′, Σ′, k′_{l}) is a zigzag morphism if it satisfies the properties:

1. f is surjective;

2. f is continuous;

3. ∀l ∈ L, s ∈ S, σ′ ∈ Σ′, k_{l}(s, f^{−1}(σ′)) = k′_{l}(f(s), σ′).

Asking f to be surjective allows us to avoid introducing initial states and worrying about reachable states. Note that we are now taking the topological structure seriously and requiring zigzag morphisms to be continuous. One can immediately check that the identity morphism is a zigzag.

3The name arises from modal logic, see, for example, [Pop94].

We often refer to a labelled Markov process by its set of states. Following Joyal, Nielsen and Winskel ([JNW96]) we define bisimulation as the existence of a span of zigzag morphisms.

Definition 5.3 Let T and T′ be two labelled Markov processes. T is probabilistically bisimilar to T′ (written T ∼ T′) if there is a span of zigzag morphisms between them, i.e. there exists a labelled Markov process S and zigzag morphisms f and g such that

S
[figure: f; g]
T  T′

Notice that if there is a zigzag morphism between two systems, they are bisimilar since the identity is a zigzag morphism.

It is interesting to note that we can take a coalgebraic view of bisimulation [AM89, Rut95, dVR] as well. We can view a labelled Markov process as a coalgebra of a suitable functor; in fact it is a functor introduced by Giry [Gir81] in order to define a monad on Mes analogous to the powerset monad. From this point of view, bisimulation is a span of coalgebra homomorphisms. But if one checks what this means, these are precisely zigzag morphisms.

We want bisimulation to be an equivalence, so we need to prove transitivity of the existence of span, since it is obviously reflexive and symmetric. Proving transitivity presents formidable difficulties. In particular, it probably isn’t true for probabilistic transition systems without the assumption of Polish structure. The proof works only for Polish spaces^{4} The main result proved in detail in the appendix is the following.

Theorem 5.4 The category with labelled Markov processes as objects and zigzag morphisms as the morphisms has pullbacks.

Corollary 5.5 Bisimulation defined as above (i.e. with Polish space structure on the sets of states and with zigzag morphisms assumed to be continuous) on labelled Markov processes is an equivalence relation.

4We have recently extended it to analytic spaces.

Before outlining the proof it is worth discussing why this isn’t trivial. A naive idea might be to mimic the construction for the discrete case but this is too closely tied to the idea of there being probabilities defined for point-to-point transitions. Consider the situation in the diagram below.

S_{1}  S_{2}
[figure: f_{1}; f_{2}]
S

where f_{1} and f_{2} are zigzags. Then we want to show that we can find a system, say U, such that the following diagram commutes.

U
[figure: g_{1}; g_{2}]
S_{1}  S_{2}
[figure: f_{1}; f_{2}]
S

It is natural to mimic the pullback construction in Set, thus, we take U to be the collection of all pairs (s_{1}, s_{2}) from S_{1} × S_{2} such that f_{1}(s_{1}) = f_{2}(s_{2}), and g_{1} and g_{2} to be the obvious projections, π_{1} and π_{2}. The set U inherits a σ-algebra from the product σ-algebra on S_{1} × S_{2}. Now we have to define a transition probability h : U × Σ_{U} ⟶ [0, 1]. The requirement that π_{1} and π_{2} are zigzags forces us to define h((s_{1}, s_{2}), (σ_{1} × S_{2}) ∩ U) = k_{1}(s_{1}, σ_{2}) and similarly for π_{2}. Unfortunately sets of the form σ_{1} × S_{2} and S_{1} × σ_{2} are not enough to determine a measure on all of Σ_{U}. Roughly speaking we need the values on all the rectangles not just on the “strips”. Worse yet, given a set of the form (σ_{1} × σ_{2}) ∩ U we do not have σ_{1} and σ_{2} unambiguously determined; there could be two unrelated sets σ′_{1} and σ′_{2} with

(σ_{1} × σ_{2}) ∩ U = (σ′_{1} × σ′_{2}) ∩ U

so we cannot really use σ_{1} and σ_{2} to define h.

The actual construction uses two key ideas. The first is to forget about U for the moment and define a transition probability on S_{1} × S_{2} but instead of just taking the product system we condition the probabilities on the transitions agreeing when their images are looked at in S. Now we can define the transition probability on “rectangles” and extend to all of the space. The conditioning automatically makes the measure live just on U rather than on all of S_{1} × S_{2}. This finesses the ambiguities of the naive approach.

Proof. The fact that the identity morphism is a zigzag immediately implies that bisimulation is reflexive and the fact that it is defined by spans gives symmetry trivially. In order to prove transitivity we need to show that given two spans we can construct a composite span. If we had pullbacks we can of course compose spans. In fact pullbacks do exist if we look at the (obviously nonfull) subcategory of zigzag morphisms. The proof of this is given in detail in the appendix. It should not be assumed that the complete proof is uninteresting or unimportant; indeed it can be formulated as a theorem of pure probability theory.

Three objects

S_{1} = (S_{1}, Σ_{1}, k_{1} : S_{1} × Σ_{1} → [0, 1]),
S_{2} = (S_{2}, Σ_{2}, k_{2} : S_{2} × Σ_{2} → [0, 1]),
S = (S, Σ, k : S × Σ → [0, 1])

and morphisms f_{1} : S_{1} → S and f_{2} : S_{2} → S are given.

Let U = {(s_{1}, s_{2}) ∈ S_{1} ×S_{2} | f_{1}(s_{1}) = f_{2}(s_{2})} equipped with the subspace topology of the product topology on S_{1} × S_{2}. The Borel σ-algebra Σ_{U} on U is generated by the set {(σ_{1} × σ_{2}) ∩ U | σ_{1} ∈ Σ_{1}, σ_{2} ∈ Σ_{2}}. Let π_{1} : U → S_{1} and π_{2} : U → S_{2} be the projection maps. Since f_{1} and f_{2} are surjective, U is not empty. We want to construct h : U × Σ_{U} → [0, 1] so that (U, Σ_{U}, h) is an object and π_{1} : U → S_{1} and π_{2} : U → S_{2} are morphisms. For an element x of a set X, an element y of a set Y, subsets A ⊆ X, B ⊆ Y and a function f : X → Y, we sometimes write x instead of {x}, fx instead of f(x), fA instead of f(A), and f^{−1}B instead of f^{−1}(B).

We fix (s_{1}, s_{2}) ∈ U, i.e. s_{1} ∈ S_{1} and s_{2} ∈ S_{2} with f_{1}s_{1} = f_{2}s_{2}, throughout this proof. The index i always takes the values 1 and 2. The variable ω_{i} always runs through S_{i} whereas the variable s runs through S.

For i = 1, 2, we have the probability measures k_{i}(s_{i}, −) : Σ_{i} → [0, 1] on the space (S_{i}, Σ_{i}). Also Σ′_{i} = {f_{i}^{−1}σ | σ ∈ Σ} ⊆ Σ_{i} is a sub-σ-algebra of Σ_{i} (i = 1, 2). We therefore have, for a given σ_{i} ∈ Σ_{i}, the conditional probability distribution P ((s_{i}, σ_{i})|Σ′_{i}) : S_{i} → [0, 1] of the probability measure k_{i}(s_{i}, −) given the sub-σ-algebra Σ′_{i} ⊆ Σ_{i}. Since S_{i} is a Polish space we can assume [Dud89, Theorem 10.2.2] that P ((s_{i}, σ_{i})|Σ′_{i})(−) is a regular conditional probability distribution, i.e.

(i) P ((s_{i}, σ_{i})|Σ′_{i}) : S_{i} → [0, 1] is Σ′_{i} measurable and integrable.

(ii) For all γ′_{i} ∈ Σ′_{i}, we have

∫_{γ′_{i}} P ((s_{i}, σ_{i})|Σ′_{i})(ω_{i})k_{i}(s_{i}, dω_{i}) = k_{i}(s_{i}, σ_{i} ∩ γ′_{i}).

(iii) For k_{i}(s_{i}, −)-almost all ω_{i} ∈ S_{i}, P ((s_{i}, −)|Σ′_{i})(ω_{i}) : Σ_{i} → [0, 1] is a probability measure on S_{i}.

A regular conditional probability distribution, like a conditional probability distribution, is unique up to a set of measure zero, i.e. any two functions satisfying the above three properties are equal for k_{i}(s_{i}, −)-almost all ω_{i} ∈ S_{i}.

One should think of P ((s_{i}, σ_{i})|Σ′_{i})(ω_{i}) as the probability that s_{i} makes a transition to σ_{i} given that s_{i} makes a transition to f_{i}^{−1}f_{i}ω_{i}, or equivalently as the probability that s_{i} makes a transition to σ_{i} given that f_{i}s_{i} makes a transition to f_{i}ω_{i}.

By a standard method we can obtain the conditional probability distribution

P ((s_{i}, σ_{i})|Σ) : S → [0, 1].

Here, P ((s_{i}, σ_{i})|Σ)(s) gives the probability that s_{i} makes a transition to σ_{i} given that s_{i} makes a transition to some ω_{i} with f_{i}(ω_{i}) = s or equivalently the probability that s_{i} makes a transition to σ_{i} given that f_{i}s_{i} makes a transition to s.

In order to define h((s_{1}, s_{2}), −) : Σ_{U} → [0, 1] we first define a probability measure g((s_{1}, s_{2}), −) : Σ_{S_{1}×S_{2}} → [0, 1] on the product space (S_{1}×S_{2}, Σ_{S_{1}×S_{2}}) where Σ_{S_{1}×S_{2}} is the Borel σ-algebra of S_{1} × S_{2}. We will then show in the next section that g((s_{1}, s_{2}), −) is supported on U, i.e. g((s_{1}, s_{2}), U) = 1. We will finally define h((s_{1}, s_{2}), α ∩ U) = g((s_{1}, s_{2}), α).

Let R = Σ_{1} × Σ_{2} be the collection of all “rectangles” σ_{1} × σ_{2} ∈ Σ_{S_{1}×S_{2}}; R is a semi-ring. For σ_{1} × σ_{2} ∈ R and s ∈ S, put

ρ((s_{1}, s_{2}), σ_{1} × σ_{2})(s) = P ((s_{1}, σ_{1})|Σ)(s)P ((s_{2}, σ_{2})|Σ)(s).

Since for k(f_{1}s_{1}, −)-almost all s ∈ S, P ((s_{1}, −)|Σ)(s) and P ((s_{2}, −)|Σ)(s) are probability measures on S_{1} and S_{2} respectively, we have:

Proposition 5.6 [Dud89, Theorem 4.4.1]

For k(f_{1}s_{1}, −)-almost all s ∈ S, ρ((s_{1}, s_{2}), −)(s) is countably additive on R.

For σ_{1} × σ_{2} ∈ R, put

g((s_{1}, s_{2}), σ_{1} × σ_{2}) = ∫_{S} P ((s_{1}, σ_{1})|Σ)(s)P ((s_{2}, σ_{2})|Σ)(s)k(f_{1}s_{1}, ds). (1)

Now we can show the following result.

Proposition 5.7 g((s_{1}, s_{2}), −) has a unique extension to a probability measure on (S_{1} × S_{2}, Σ_{S_{1}×S_{2}}).

The measure g is defined on all of S_{1}×S_{2} not just on U. But the following remarkable proposition says that in fact g is only supported on U.

Proposition 5.8 For any σ_{1} ∈ Σ_{1} and σ_{2} ∈ Σ_{2} with U ∩ (σ_{1} × σ_{2}) = ∅ we have g((s_{1}, s_{2}), σ_{1} × σ_{2}) = 0.

This proof used some subtle facts about Borel sets and continuous functions from Polish spaces to Hausdorff spaces and in given in detail in the appendix. From this result we can easily define

h((s_{1}, s_{2}), α ∩ U) = g((s_{1}, s_{2}), α).

We can now complete the proof by checking the following statement. (U, Σ_{U}, h : U × Σ_{U} → [0, 1]) is an object of the category and π_{i} : U → S_{i} are morphisms.

The verification of the last statement is as follows. Clearly U is a Polish space as it is a closed subset of the Polish space S_{1} × S_{2}. We have already shown that h((s_{1}, s_{2}), −) is a probability measure on U for any (s_{1}, s_{2}) ∈ U. Finally, for any σ_{1} ∈ Σ_{1} we have:

h((s_{1}, s_{2}), π_{1}^{−1}σ_{1})

= h((s_{1}, s_{2}), (σ_{1} × S_{2}) ∩ U)

= g((s_{1}, s_{2}), σ_{1} × S_{2})

= ∫_{S} P ((s_{1}, σ_{1})|Σ)(s)P ((s_{2}, S_{2})|Σ)(s)k(f_{1}s_{1}, ds)

= ∫_{S} P ((s_{1}, σ_{1})|Σ)(s)k(f_{1}s_{1}, ds)  P ((s_{2}, S_{2})|Σ)(s) = 1 a.e.

= k_{1}(s_{1}, f_{1}^{−1}(s) ∩ σ_{1}) = k_{1}(s_{1}, σ_{1}).

Therefore π_{1} is a morphism. Similarly π_{2} is a morphism.

We close this section with some examples. The first example is technically trivial but conceptually crucial.

Example 5.9 We let the label set be the one element set. Consider a system (S, Σ, k) with S an arbitrarily complicated states space and Σ a σ-algebra generated by some Polish space structure on S. For example, S could be ℝ, the reals with the Borel algebra. We define the transition function, k(s, σ) in any manner we please subject only to the conditions of the definition of a transition function and to the condition that ∀s ∈ S.k(s, S) = 1; i.e. for every s, the distribution k(s, ·) is a probability measure. Consider the trivial labelled Markov chain with just one label, one state and one transition from the state to itself with probability 1. These two systems are bisimilar!

This example allows us to clarify the discussion in the introduction. All of conventional stochastic process theory is described by systems like the first system above. From our point of view they are trivial. This is to be expected, as we are modelling interaction and all such systems are indeed trivial from the point of view of interaction. In order to get nontrivial examples one has to consider systems with richer label sets, and which are not always capable of making transitions with every label. Note also that many continuous systems are bisimilar to discrete ones. If we know this we can use the (presumably simpler) discrete system when reasoning about composite systems. Without our framework this would not be possible.

Example 5.10 Consider the labelled Markov chain over a one-element label set ({a, b, c}, P) where the transition matrix, P is given by P (a, b) = P (a, c) = 1/2 with all other entries being zero. Consider another system over the same label set with 4 states {w, x, y, z} and with transition matrix Q given by Q(w, x) = Q(w, y) = Q(w, z) = 1/3. These two systems are bisimilar. One can easily verify this by constructing the obvious “product” system and checking that the projections are zigzags. On the other hand there is no zigzag morphism between the two systems. These systems are small enough to check this by hand.

The last example shows that bisimulation really does have to be defined in terms of spans, i.e. it really is a relation.

Example 5.11 The next example illustrates a continuous system. Consider the labelled Markov process, over the trivial label set, defined as follows S = (ℝ, B, k), i.e. the states are real numbers, the measurable sets are Borel sets and the transition function is defined on intervals (and then extended to arbitrary Borel sets) as follows:

k(x, [r, s]) = \begin{cases}λ/2 ∫_{r}^{s} e^{−λ|x−y|}dy & if x ≥ 0, \\ 0 & otherwise. \end{cases}

where the constant factor of λ/2 chosen to make k be 1 on the whole space. Intuitively this is a system where a particle makes random jumps with probability exponentially distributed with the length. However, there is an “absorbing wall” at the point x = 0 so that if the system jumps to the left of this point it gets stuck there. Note that every positive state has a different probability density for jumping to a negative state. Now consider the system U = (ℝ^{2}, B^{2}, h) defined as

h((x, y), [r, s] × [p, q]) = k(x, [r, s])P ([p, q]),

where P is some arbitrary probability measure over ℝ. This system should behave “observably” just like the first system because, roughly speaking, the first coordinate behaves just like the first system and the second system has trivial dynamics, i.e. it is bisimilar to the one-state, one-transition system. Indeed these two systems are bisimilar with the projection from the second to the first being a zigzag.

The next example illustrates a possible objection to our definition.

Example 5.12 Suppose that we have two systems, (ℝ, B, {a, b}, k_{l}) and (ℝ, B, {a, b}, h_{l}). In the first system we have the following transitions

k_{a}(x, S) = μ(S ∩ [x − 0.5, x + 0.5])

and

k_{b}(x, S) = μ(S ∩ [x + 0.5, x + 1.5])

where S is a Borel set and μ is Lebesgue measure. For the other system we have

h_{a}(x, S) = \begin{cases}μ(S ∩ [x − 0.5, x + 0.5]) & if x is irrational \\ 0 & if x is rational. \end{cases}

the b transitions are the same as those for the first system. These two systems are not bisimilar by our definition. The first one is bisimilar to the trivial one-state system with both a and b enabled all the time while the second one is has states in which a gets disabled. However, the probability of landing in one of these states is 0. Thus, in some sense, the difference is visible only on a set of probability 0. Should they be distinguished?

6 Discrete Systems Revisited

In this section we reconsider discrete systems (Markov chains) from the point of view of the bisimulation notion that we have defined for general partial, labelled, Markov processes. We show that the Larsen-Skou definition coincides with the “span of zigzags” definition. First, we have to say what it means for two Markov chains to be Larsen-Skou bisimilar, since the Larsen-Skou definition involves states of a single process rather than states of two different processes, and so doesn’t apply without an appropriate interpretation. Roughly speaking, if there were an initial state in every Markov chain, then we would say that two Markov chains are Larsen-Skou bisimilar if and only if in a system “combining” them, their initial states are Larsen-Skou bisimilar. We have chosen not to equip Markov chains with initial states, instead we will use the following as a definition of Larsen-Skou bisimulation between two Markov processes.

Definition 6.1 Let (S_{1}, P_{l}^{1}), (S_{2}, P_{l}^{2}), be two Markov chains and (T, H_{l}), their disjoint union, that is, T is the disjoint union of the two sets S_{1} and S_{2}, and for s, t ∈ T, H_{l}(s, t) = P_{l}^{i}(s, t) if s, t are both in S_{i} (i = 1, 2) and zero otherwise. We will say that S_{1} ∼_{LS} S_{2} if in T there is a probabilistic bisimulation ≡_{p} such that for every state s_{i} of S_{i} there is a state s_{j} of S_{j} such that s_{i} ≡_{p} s_{j} (i, j ∈ {1, 2}, i ≠ j).

We assume that all systems are partial in this section. Recall that we can always define a topology in which all the sets are open and hence all functions are continuous. Since the space is countable the topology is clearly Polish. Thus, we can forget about the topology in this section but we keep in mind that discrete systems are a special case of the formalism of the previous section.

Proposition 6.2 Let (S, P_{l}) and (S′, P′_{l}) be two labelled Markov chains. (S, P_{l}) ∼_{LS} (S′, P′_{l})′ if and only if there exists a span of zigzag morphisms f and f′:

U
[figure: f; f′]
S  S′

Proof. We write k_{l} and k′_{l} for the two transition functions induced by the transition matrices P_{l} and P′_{l} respectively.

⇐: We first show that if S →^{f} S′, where f is a zigzag morphism, then S ∼_{LS} S′. Let (t, H_{l}) be the disjoint union of (S, P_{l}) and (S′, P′_{l}), and h_{l} be the transition function induced by the transition matrix H_{l}. Now f defines the following equivalence relation, R, on T:

s_{1}Rs_{2} ⟺ (s_{1} = s_{2}) ∨ (f(s_{1}) = s_{2}) ∨ (f(s_{1}) = f(s_{2})).

The equivalence classes are of the form {s′} ∪ f^{−1}(s′) for each s′ ∈ S′; thus each equivalence class can be represented uniquely by an element of S′. Let l ∈ L, s_{1}, s_{2} ∈ T such that s_{1}Rs_{2}, and choose any t′ ∈ S′ that represents the equivalence class {t′}∪f^{−1}(t′). We want to show that h_{l}(s_{1}, −) and h_{l}(s_{2}, −) agree on {t′} ∪ f^{−1}(t′).

First assume s_{1} ∈ S and s_{2} ∈ S′, meaning that f(s_{1}) = s_{2}. Then

h_{l}(s_{1}, {t′} ∪ f^{−1}(t′)) = k_{l}(s_{1}, f^{−1}(t′)) since s_{1} ∈ S
= k′_{l}(f(s_{1}), {t′}) since f is a zigzag morphism
= h_{l}(s_{2}, {t′} ∪ f^{−1}(t′)),

which is precisely the condition for Larsen-Skou bisimulation. Now if s_{1} and s_{2} are both in S (and still R-related), they have the same image, so s_{1} R f(s_{1}) = f(s_{2}) R s_{2} and we can simply apply the above calculation. Finally we have the trivial case where s_{1} and s_{2} are both in S′, they are then equal and we are done since, f being a surjective function, every state of S is R-equivalent to a state of S′ are vice versa. Since we know that Larsen-Skou bisimulation is an equivalence relation it follows that whenever we have a span of zigzags connecting two labelled Markov chains they are Larsen-Skou bisimilar.

⇒: Assume (S, P_{l}) ∼_{LS} (S′, P′_{l}), with ≡_{p} the probabilistic bisimulation over (T, H_{l}) the disjoint union of (S, P_{l}) and (S′, P′_{l}). We need to construct a span of zigzag morphisms

U
[figure: f; f′]
S  S′

To do this, let U = (U, (Q_{l})_{l∈L}) where U = {(s, s′) ∈ S × S′ : s ∼_{LS} s′ in T } and where the transition matrix Q is given by, for l ∈ L,

Q_{l}((s, s′), (t, t′)) = \frac{P_{l}(s, t) P′_{l}(s′, t′)}{h_{l}(s, [t]_{∼_{LS}})}

where [t]_{∼_{LS}} denotes the equivalence class containing t in T, and h_{l} is the transition function induced by the transition matrix H_{l}. Since s ∼_{LS} s′ and t ∼_{LS} t′, we have by definition of ∼_{LS} that h_{l}(s, [t]_{∼_{LS}}) = h_{l}(s′, [t]_{∼_{LS}}) = h_{l}(s′, [t′]_{∼_{LS}}).

To prove that U is a partial, labelled, Markov chain, we need that for any (s, s′) ∈ U,

∑_{(t,t′)∈U} Q_{l}((s, s′), (t, t′)) ≤ 1.

This will follow from the proof that we have zigzag morphisms from U to S and S′. As morphisms f : U → S and f′ : U → S′, we simply take the left and right projections which are surjective by definition of Larsen-Skou probabilistic bisimulation. We prove that they are zigzag morphisms. We write q_{l} for the transition function derived from the transition matrix Q_{l}. First note that

∀t ∈ S.f^{−1}(t) = {t} × (S′ ∩ [t]_{∼_{LS}}).

For any l ∈ L, (s, s′) ∈ U, t ∈ S, we have

q_{l}((s, s′), f^{−1}(t)) = ∑_{t′∈S′∩[t]_{∼_{LS}}} Q_{l}((s, s′), (t, t′))

= ∑_{t′∈S′∩[t]_{∼_{LS}}} \frac{P_{l}(s, t) P′_{l}(s′, t′)}{h_{l}(s, [t]_{∼_{LS}})}

= \frac{P_{l}(s, t)}{h_{l}(s′, [t]_{∼_{LS}})} ∑_{t′∈S′∩[t]_{∼_{LS}}} P′_{l}(s′, t′)

= \frac{P_{l}(s, t)}{k′_{l}(s, [t]_{∼_{LS}} ∩ S)}k′_{l}(s′, [t]_{∼_{LS}} ∩ S′)
= P_{l}(s, t) = k_{l}(f(s, s′), {t}).

and f is thus a zigzag morphism. The same argument applies to f′.

7 Testing equivalences

In this section we examine the relationship between a notion of testing equivalence, 2-way simulation and probabilistic bisimulation.

The tests we consider are simple sequences of experiments, each just described by a label. As usual, let L be the fixed set of labels describing the interaction of processes with their environments.

Definition 7.1 A test over L is a finite sequence of labels of L. Given a labelled Markov process S = (S, Σ_{S}, k_{l}), a state s_{0} of S and a test T, the probability p(s_{0}; T) of success is defined in the following way;

\begin{matrix}p(s_{0}; ϵ) = 1 \\ p(s_{0}; a.T) = ∫_{S} p(s; T)k_{a}(s_{0}, ds) \end{matrix}

where ϵ is the empty string. Let (S, Σ, k_{l}) and (S′, Σ′, k′_{l}) be two labelled Markov processes. We say that S test-simulates S′ if, for every s′ ∈ S′, there exists s ∈ S such that for all test T,

p(s′; T) ≤ p(s; T).

We say that S and S′ are test-equivalent, written S ∼_{T} S′ if they testsimulate each other.

It is easily seen that p(·; T) : S ⟶ ℜ is a measurable function and that test-equivalence is indeed an equivalence relation.

Proposition 7.2 Let (S, Σ, k_{l}) and (S′, Σ′, k′_{l}) be labelled Markov processes. If there is a simulation morphism from S to S′, then S′ test-simulates S. Moreover, if the morphism is a zigzag morphism, then S and S′ are testequivalent.

Proof. We prove the second part since the first one can be easily proved in almost the same way, essentially by replacing the equalities by inequalities. Let f : S ⟶ S′ be a zigzag morphism. We show that for all s ∈ S, for all tests T, p(s; T) = p(f(s); T) by induction on the length of tests. Since f is a surjective function, this will prove that S ∼_{T} S′. We trivially have p(s; ϵ) = p(f(s); ϵ) = 1 for all s ∈ S. Now assume the assertion is true for tests of length n. Let s ∈ S and let aT be a test of length n + 1 . We have by induction hypothesis and from the definition of zigzag expressed in the following from,

k_{a}(s, ·) ∘ f^{−1} = k′_{a}(f(s), ·),

that

p(s; a.T) = ∫_{S} p(t; T)k_{a}(s, dt)
= ∫_{S} p(f(t); T)k_{a}(s, dt)
= ∫_{S′} p(s′; T)k′_{a}(f(s), ds′)
= p(f(s); a.T).

Corollary 7.3 If there is a 2-way simulation between S and S′, then S and S′ are test-equivalent.

Corollary 7.4 If S and S′ are bisimilar, then S and S′ are test-equivalent.

Note that the converse is not true, that is there exist two stochastic transition systems that are test-equivalent but not stochastic bisimilar.

These results are not meant to be a serious analysis of testing notions. They are only meant to give some feeling for what zigzag means. In future work we intend to analyze testing thoroughly.

8 Towards A Modal Logic for Bisimulation

In this section we begin the study of logics that characterize bisimulation. For discrete systems, indeed even if only one system is discrete, we can define a simple logic which plays the role of Hennessy-Milner logic. In practice one often wants to know that a continuous system can be discretized, i.e. is bisimilar to some discrete system, and this fact will be useful to determine that. We follow the treatment of Larsen and Skou [LS91] closely in terms of the definition of the logic but not in terms of proofs. The key difference is that we use negation.

We take as the syntax the following formulas:

T |¬ϕ|ϕ_{1} ∧ ϕ_{2}|⟨a⟩_{q}ϕ

where a is an action from the fixed set of actions L and q is a rational number. Given a labelled Markov process (S, Σ, k_{a}) we write s ⊧ ϕ to mean that the state s satisfies the formula ϕ. The definition of the relation ⊧ is given by induction on formulas. The definition is obvious for the propositional constants and connectives. We say s ⊧ ⟨a⟩_{q}ϕ iff ∃A ∈ Σ.∀s′ ∈ A.s′ ⊧ ϕ∧k_{a}(s, A) ≥ q. In other words, s can make an a-move to a state that satisfies ϕ with probability greater than q. We write ϕ for the set {s ∈ S|s ⊧ ϕ}. If we have two systems , say S, S′, in mind and we want to distinguish them we write ϕ _{S}.

The first proposition below says that sets of states definable by formulas are always measurable.

Proposition 8.1 For all formulas ϕ, we have ϕ ∈ Σ.

Proof. We proceed by structural induction on ϕ. The base cases corresponding to T is trivial since S ∈ Σ. The propositional connectives are trivial because a σ-algebra is closed under countable union and complementation, by definition. Finally we have ⟨a⟩_{q}ϕ = k_{a}(·, ϕ )^{−1}([q, 1]) ∈ Σ. To justify this first note that, by hypothesis, ϕ ∈ Σ so k_{a}(s, ϕ ) is meaningful. Secondly, k_{a} is a measurable function in its first argument and finally intervals are Borel.

The next proposition links zigzag morphisms with formulas in the logic.

Proposition 8.2 If f is a zigzag morphism from S to S′ then for all formulas ϕ,

s ⊧ ϕ ⟺ f(s) ⊧ ϕ.

Proof. We proceed by structural induction on ϕ. The only nontrivial cases correspond to the modal formulas. We proceed as follows; s ⊧ ⟨a⟩_{q}ϕ means k_{a}(s, ϕ _{S}) ≥ q. By the inductive hypothesis we have that f^{−1}( ϕ _{S′}) = ϕ _{S}. Thus we have

q ≤ k_{a}(s, ϕ _{S}) = k_{a}(s, f^{−1}( ϕ _{S′})) = k′_{a}(f(s), ϕ _{S′}).

But the last equality means f(s) ⊧ ⟨a⟩_{q}ϕ.

From this we get the immediate corollary, but first we need to define bisimilarity of states. We say s ∈ S and s′ ∈ S′ are bisimilar if S and S′ are bisimilar and for some span of morphisms f : T ⟶ S and f′ : T ⟶ S′ there exists t ∈ T with f(t) = s and f′(t) = s′. Now this defines an equivalence relation. In anticipation of this we write, s ∼ s′ when two states are bisimilar. To check the claim suppose that for s ∈ S, s′ ∈ S′ and s′′ ∈ S′′ we have s ∼ s′ and s′ ∼ s′′. Then we have f : T ⟶ S and f′ : T ⟶ S′ and g : T′ ⟶ S′ and g′ : T′ ⟶ S′′ with the required properties and we can use the pullback (h : U ⟶ T, k : U ⟶ T′) of f′ : T ⟶ S′ and g : T′ ⟶ S′ to obtain p : U ⟶ S and q : U ⟶ S′′. In order to show that s ∼ s′′ we proceed as follows. By assumption there exists t ∈ T and t′ ∈ T′ such that f(t) = s, f′(t) = s′, g(t′) = s′ and g′(t′) = s′′. Now (t, t′) ∈ U since f′(t) = s′ and g(t′) = s′. Therefore, putting p = f ∘ h and q = g′ ∘ k we have p((t, t′)) = f(t) = s and q((t, t′)) = g′(t′) = s′′. Thus s ∼ s′′.

Corollary 8.3 If s and s′ are bisimilar states of S and S′ respectively then they satisfy the same formulas.

Now one can show that the transition probabilities to definable sets are determined completely by the formulas, independently of the system. Suppose that (S, Σ, k_{a}) and (S′, Σ′, k′_{a}) are two systems. We say that they satisfy all the same formulas if ∀s ∈ S∃s′ ∈ S′ such that s and s′ satisfy all the same formulas and the same with s and s′ interchanged. We write S ▷◁ S′ if this is the case.

Proposition 8.4 Suppose that (S, Σ, k_{a}) ▷◁ (S′, Σ′, k′_{a}) then for all formulas ϕ and all pairs (s, s′) such that s and s′ satisfy all the same formulas, we have k_{a}(s, ϕ _{S}) = k′_{a}(s′, ϕ _{S′}).

Proof. Suppose that the equation does not hold. Then, say, for some ϕ, k_{a}(s, ϕ _{S}) < k′_{a}(s′, ϕ _{S′}). Now we choose a rational number q between these values. Now it follows that s′ ⊧ ⟨a⟩_{q}ϕ but s |̸= ⟨a⟩_{q}ϕ, which contradicts the assumption that s and s′ satisfy all the same formulas.

Now we would like to show that if two systems satisfy all the same formulas they must be bisimilar. Instead of defining a span of zigzags directly, we can define a cospan and use the pullback property to infer that a span must exist. Given two systems (S, Σ, k_{a}) ▷◁ (S′, Σ′, k′_{a}) we first construct a system, (T, Σ_{T} , j_{a}), called the direct sum of S and S′, as follows. We set T = S ⊎ S′ with the evident σ-algebra. We define the transition probabilities as follows: j_{a}(s, A⊎A′) = k_{a}(s, A) if s ∈ S and j_{a}(s′, A⊎A′) = k′_{a}(s′, A′) if s′ ∈ S′ where A ∈ Σ and A′ ∈ Σ′. There are the evident canonical injections ι, ι′ which are not zigzags because they are not surjective. Now we define an equivalence relation on the states of T by saying that two states are equivalent iff they satisfy all the same formulas. We write s ≈ s′. We define a quotient system (V, Σ_{V} , h_{a}) as follows. The states of V are the equivalence classes and the topology is the greatest one making the canonical surjection r : T ⟶ V continuous (and hence measurable). The set T is a Polish space since it is discrete. The composites r ∘ ι and r ∘ ι′ are continuous and surjective, henceforth we call them q and q′ respectively. To see that q, q′ are surjective we recall that an equivalence class must, by hypothesis, include members of both S and S′. If we can define h_{a} so as to make q, q′ both zigzag we will be done.

Proposition 8.5 If we have (S, Σ, k_{a}) ▷◁ (S′, Σ′, k′_{a}) and s ≈ s′ then for all t ∈ T, defined as above, we have k_{a}(s, [t] ∩ S) = k′_{a}(s′, [t] ∩ S′).

Proof. Let {ϕ_{i}|i ∈ ℕ} be an enumeration of the formulas satisfied by the members of [t]. If s is any state such that s ▷◁ t, s must satisfy any formula satisfied by t, so s is in the intersection. Conversely, if s ▷̸◁ t, there is a formula ϕ that distinguishes s and t, hence either s ∉ ϕ and t ∈ ϕ or s ∈ ϕ and t ∉ ϕ ; since the latter is equivalent to saying s ∉ ¬ϕ and t ∈ ¬ϕ , we have in both cases that s is not in the intersection of the ϕ_{i}’s.

Let ∀i ∈ ℕ.ψ_{i} =^{def} ⋀_{l=1}^{i} ϕ_{l}. We show that [t] = ∩_{i=1}^{∞} ψ_{i} . The sets ψ_{i} _{S} and ψ_{i} _{S′} are both measurable for all i and decrease as i increases. Furthermore, these decreasing chains converge to [t] ∩ S and [t] ∩ S′ respectively. By the monotone convergence property of measures we have

k_{a}(s, [t] ∩ S) = lim_{i⟶∞} k_{a}(s, ψ_{i} _{S}),

by the previous proposition we have

= lim_{i⟶∞} k′_{a}(s′, ψ_{i} _{S′}) = k′_{a}(s′, [t] ∩ S′).

We can define h_{a} as follows. We only need to specify the point to point transition probabilities since, in the discrete case, these determine all the transition probabilities. Now we set h_{a}([s], [t]) =^{def} k_{a}(s, q^{−1}([t])). Clearly the representative of the [s] equivalence class does not matter. Furthermore by proposition 8.5, we can see that h_{a}([s], [t]) = k′_{a}(s′, q′^{−1}([t])). The morphisms are now zigzags. Thus we have proved the following proposition

Proposition 8.6 If we have two systems and one of them is discrete then they are bisimilar iff they obey the same formulas.

Note that this implies the result for discrete systems without using the minimum deviation assumption used by Larsen and Skou.

9 Related Work

There has been a substantial amount of work on probabilistic transition systems and their associated equivalences. As far as we are aware, none of them have looked at bisimulation for continuous state spaces.

The starting point of work in the area of probabilistic semantics are the fundamental papers of Saheb-Djahromi [SD78, SD80] and of Kozen [Koz81, Koz85]. These are concerned with domain theory and programming languages rather than with process equivalences but they both introduced nontrivial measure-theoretic ideas. Kozen also noticed a very interesting duality between state-transformer semantics as described by stochastic kernels and a probabilistic predicate-transformer semantics in which programs are seen as inducing linear continuous maps on the Banach algebra of bounded measurable functions.

The one paper with an abstract categorical approach to stochastic processes is by Giry [Gir81] but she studies categorical constructions rather than process equivalences. Of course her work, inspired originally by Lawvere, does provide some of the mathematical underpinnings of our ideas. In particular she shows that the stochastic kernels (conditional probability distributions) that we use to define transition probabilities arise as the Kleisli category of a monad, which is a natural generalization of the powerset monad to the probabilistic case. If we recall that the category Rel of sets and relations is the Kleisli category of the powerset monad, we see that the stochastic kernels can reasonably be viewed as the probabilistic analogues of relations. This makes the analogy between labelled Markov processes and ordinary transitions quite striking.

The starting point of our investigations has been the pioneering paper of Larsen and Skou [LS91] which gave the first compelling analysis of probabilistic bisimulation. As we have mentioned before their work is couched in terms of state-to-state transition probabilities so there were both conceptual as well as technical obstacles to overcome. The work of Joyal, Nielsen and Winskel [JNW96] and of Cheng and Nielsen [CN95] provided vital clues. Following Joyal et. al. we define probabilistic bisimulation as spans of zigzags.

From the point of view of applications there have been a number of very interesting results. The most interesting work, in our opinion, is the work of Jane Hillston [Hil94] on developing a process algebra for performance evaluation. Her work is not comparable to ours at present because she works with continuous-time Markov chains, i.e. with continuous time and a discrete state space. Nevertheless it is our hope that as our own work evolves we will make contact with her approach.

The group at Oxford has been developing an extensive theory of probabilistic systems; see the collection of reports available from the web [Pro]. The focus has been on equational laws satisfied by processes. From the semantic point of view they have extensively developed and enriched Kozen’s [Koz85] predicate-transformer view. They have looked at continuous state-space systems and have incorporated nondeterminism in their framework. As with the earlier work of Kozen [Koz81, Koz85] stochastic kernels play an important role.

Finally we mention a sample of the large amount of work on various notions of testing [CSZ92, Chr90, JY95], simulations [SL94], specification [JL91], model checking [HK96], generative processes [vGSST90] and other variations which, for example, allow one to have both probability and nondeterminism. It should be possible to develop analogous notions for a variety of continuous state-space systems once the mathematical foundations are in place. With the present work the mathematical apparatus needed is in place though of course a significant amount of work remains to determine which models and equivalences are useful in practice.

10 Conclusions

In this paper we have two main contributions. First, we develop a notion of labelled Markov process as a model of interacting Markov processes. The state space may have complex structure but the interactions are simple synchronizations. Unlike the classical theory of Markov processes, which asks about the evolution of the system in state space, we study behavioural equivalences from the point of view of observing interactions. This kind of system is exactly what is studied in much of hybrid systems – simple finite-state controllers interacting with a complex dynamical system. Of course the stochastic versions of such systems have not been studied very much as yet.

Secondly we develop a notion of bisimulation for probabilistic processes which applies to systems where the state space can be continuous. The essential limitation, met in all examples known in physics, control theory or computing, is that the state space be equipped with the structure of a Polish space. The fundamental technical contribution is the proof that this is indeed an equivalence relation. This requires a fairly hard proof which can be seen as a theorem of Markov processes in its own right. In particular no previous study of probabilistic bisimulation has had to deal with these technical questions. We expect that future studies of such systems will use either this technique or ones very like it.

The secondary results of this paper are 1. that we have shown how this notion of bisimulation extends the defi-

nition of Larsen and Skou [LS91] for the discrete case

2. and that we have a logical characterization of bisimulation which works even when only one of the systems is discrete and does not use the minimum deviation assumption.

The important questions to answer for the future are the following.

1. The notion of bisimulation in the probabilistic case can be, and should be, debated. For example suppose there are two systems which have different behaviours but these differences are only visible with probability 0, do we want to say that they are or are not bisimilar. In the present paper we would say that they are not bisimilar.

2. What is the general logical characterization of bisimulation? We might have to adopt the point of view that formulas are measurable functions and that the satisfaction “relation” has to be generalized to mean integration. Kozen has already used such ideas [Koz85] in his study of probabilistic PDL.

3. What is the right notion of testing and can we exhibit bisimulation as a testing equivalence? The bisimulation relation that we introduce in this paper is, like Larsen and Skou’s, sensitive to small changes in the probabilities. This makes the development of the appropriate testing notions important in order to discuss what one might plausibly test for in a continuous state space setting. In particular it should allow us to initiate a serious study of stability of systems.

4. What is the right notion of simulation? What will happen to simulation and bisimulation in the presence of nondeterminism? These questions have been studied extensively in the discrete case.

5. What are the right calculi for such systems? This is completely wide open at this point.

6. Can we extend these ideas to continuous time? This certainly should be possible and really bring this work into contact with extant work on hybrid systems.

Acknowledgements

Abbas Edalat would like to thank Terry Lyons for helpful discussions and EPSRC (UK) for support. Prakash Panangaden would like to thank Samson Abramsky, Christel Baier, Luca Cattani, Jørgen Hoffman-Jørgensen, Alan Jeffrey, Jan Rutten, Ian Stark, Colin Stirling and Glynn Winskel for helpful discussions and BRICS for its hospitality during the course of this work. Richard Blute, Josée Desharnais and Prakash Panangaden thank NSERC (Canada) for its support. Richard Blute and Prakash Panangaden acknowledge the support of an Ontario-Québec Bilateral Exchange grant.

A A Review of Measure Theory

For completeness we give the basic definitions in this section. We only discuss positive measures. We assume, however, that the reader knows the basic ideas of measure theory and probability as expounded in, for example “Probability and Measure” by Billingsley [Bil79] or “Real Analysis and Probability” by Ash [Ash72] or the book with the same title by Dudley [Dud89] or “Introduction to Measure and Probability” by Kingman and Taylor [KT66].

The basic concept is that of a σ-algebra on a set. These are the sets for which a notion of “measure” or “size” can be defined.

Definition A.1 A σ-algebra on a set X is a family of subsets of X which includes X itself and which is closed under complementation and countable unions.

A set equipped with a σ-algebra is called a measurable space. For simple situations we can usually take the σ-algebra to be all the subsets but when we get to sets like the real line (or closed intervals of the real line) we cannot any longer work with this σ-algebra because one cannot consistently define probabilities (measures) sensibly on all subsets.

Fact A.2 The intersection of an arbitrary collection of σ-algebras is a σalgebra.

Thus, given an arbitrary collection of subsets of a set we can define the σalgebra generated by the collection. For example, given a topological space (X, T ), we can define the σ-algebra, often written B, generated by the open sets. This is usually called the Borel algebra.

The notion of measure generalizes the concept of “length of an interval” to arbitrary σ-algebras.

Definition A.3 Given a σ-algebra (X, Σ), a (probability) measure on X is a ([0, 1]-valued) [0, ∞]-valued set function, μ, defined on Σ such that

• μ(∅) = 0,

• for a pairwise disjoint, countable collection of sets, {A_{i}|i ∈ I}, in Σ, we require

μ(⋃_{i∈I} A_{i}) = ∑_{i∈I} μ(A_{i}).

In addition for probability measures we require μ(X) = 1.

The second property above is called countable additivity. A probability space is a set X equipped with a σ-algebra Σ and a measure P such that P (X) = 1.

Example A.4 The key example in the subject is provided by Lebesgue measure on the real line. Let R stand for the real numbers. The elements of the σ-algebra generated by the open intervals are called the Borel sets. There is a measure defined on these sets which on intervals agrees with the intuitive notion of length. This is the Lebesgue measure. It may be calculated as follows. Suppose that A is a Borel set. We take a family of intervals, J, (not necessarily pairwise disjoint) which covers A. We define the length of J as the sum of the lengths of all the intervals in J. Now we take the inf of the lengths over all J which cover A. One can verify that single points have measure zero and that any countable set has measure zero. The Cantor set gives an example of an uncountable set of measure zero. The set of all irrationals between 0 and 1 has measure 1. This measure is translation invariant and is in fact the unique translation-invariant measure which assigns 1 to the interval [0, 1]. The fact that makes this entire theory so complicated is the existence of nonmeasurable sets.

Functions between measurable spaces are called measurable functions.

Definition A.5 A function f : (X, Σ_{X}) ⟶ (Y, Σ_{Y}) between measurable spaces is said to be measurable if ∀B ∈ Σ_{Y} .f^{−1}(B) ∈ Σ_{X}.

This resembles the topological notion of continuity. The fundamental difference is that limits of sequences of measurable functions is measurable; the analogous property certainly does not hold for continuity. Measurable spaces and measurable functions form a category called Mes. This category has countable coproducts and all finite limits (in particular products and equalizers).

We now define Lebesgue integration. We assume that we are given a measure space (X, Σ, μ). Let f : X ⟶ ℝ be a real-valued measurable function defined on X. Instead of carving up the domain space as is done in Riemann integration we carve up the range. More precisely we define a simple, real-valued function on X to be a function whose range is finite. Any simple function, say s, can be expressed as a linear combination of characteristic functions

s = ∑_{i=i}^{n} r_{i}χ_{A_{i}}

where r_{i} are real numbers (the values assumed by s) and A_{i} are the sets on which s assumes the value r_{i}. The A_{i} have to be measurable for s to be measurable. It is clear what the integral of such a simple function should be

∫ sdμ =^{def} ∑_{i=1}^{n} r_{i}μ(A_{i}).

Let us assume that f, the function we wish to integrate is positive. Now a fundamental (but easy) result of measure theory is that a positive measurable functions f can be approximated pointwise by an increasing sequence of simple functions

s_{1} ≤ s_{2} ≤ … ≤ s_{n} ≤ … ≤ f.

We use this as the basis of the definition of the integral of f

∫ fdμ = lim_{j⟶∞} ∫ s_{j}dμ

where the limit on the right is assumed to exist. If the limit does exist we say that the function is integrable and the value of the limit is the value of the integral. It is not difficult to show that the value is independent of the approximating sequence of simple functions. The integral of a general function is defined by breaking it up into positive and negative pieces and defining the two integrals separately. The Lebesgue theory has much better convergence behaviour than the Riemann theory. In particular we have the

Theorem A.6 (Monotone Convergence Theorem) If {f_{i}|i ∈ I} is a sequence of measurable functions with ∀i.f_{i} ≤ f_{i+1} and f = sup_{i∈I}f_{i} then

∫ fdμ = lim_{i⟶∞} ∫ f_{i}dμ.

There are much stronger convergence theorems available.

A key result in classical measure theory is the Radon-Nikodym theorem. We write μ << ν if ν(A) = 0 ⇒ μ(A) = 0 for any measurable set A. We say that μ is absolutely continuous with respect to ν. The Radon-Nikodym says that if the measures are finite^{5} then there is a measurable function h such that for any measurable set A we have

μ(A) = ∫_{A} hdν.

Furthermore this function is unique almost everywhere; in other words, if there is another function h′ with the same property it can only differ from h on a set of ν measure 0. This theorem gives a notion of differentiating one measure by another. One often calls h the Radon-Nikodym derivative of μ with respect to ν.

An important application of the Radon-Nikodym theorem is to construct conditional probability distributions. Conditional probabilities relate probabilistic information with definite information and are the key to probabilistic reasoning. In the discrete case the conditional probability can be defined as follows

P (A|B) =^{def} \frac{P (A ∩ B)}{P (B)}.

This should be read as “the probability of A being true given that B is true”. Of course, this makes sense only if P (B) ≠ 0. In the continuous case most of the probabilities are 0, so conditional probabilities have to be defined more subtly.

5Actually a much weaker condition suffices but the present result is all one needs for probability.

Suppose that we have a probability space (X, Σ, P). Suppose that Σ′ is a sub σ-algebra of Σ. Suppose that A is a measurable set in Σ. We wish to know the following kind of information. We do an experiment and find out in which subset of Σ′ a point lies; now we want to know how to estimate probabilities that the point lies in A. We can define a new probability measure Q by Q(B) = P (A ∩ B) for B ∈ Σ′. Now using the Radon-Nikodym theorem we can define a conditional probability density function P (A|Σ′) : X ⟶ [0, 1] with the properties:

1. P (A|Σ′)(·) is measurable with respect to Σ′ and integrable as well;

2. for a set B in Σ′ we have

∫_{B} P (A|Σ′)(x)dP (x) = P (A ∩ B).

This density replaces the naive conditional probabilities of the previous paragraph.

B Proof that Spans of Zigzags Can Be Composed

In this section we give a self-contained proof that we can compose spans of zigzag morphisms. In fact we will prove slightly more. In the category where the morphisms are zigzags we can construct pullbacks.

B.1 Introduction

Consider the following category. Objects are of the form

S = (S, Σ, k : S × Σ → [0, 1]),

where S is a Polish space, i.e. a topologically complete separable metrizable space, Σ is the Borel σ-algebra on S and k is a transition probability function, i.e. for each s ∈ S, k(s, −) : Σ → [0, 1] is a bounded Borel measure which we assume is extended to all measurable subsets of S. A morphism f : S → S′, where S = (S, Σ, k : S × Σ → [0, 1]) and S′ = (S′, Σ′, k′ : S′ × Σ′ → [0, 1]), is a continuous surjection which preserves transition probabilities, i.e. it satisfies, k(x, f^{−1}(σ′)) = k′(f(x), σ′) for all x ∈ S and σ′ ∈ Σ′. It is easy to see that this gives a category. The composition of two morphisms, when it exists, is given by the composition of the two continuous maps. A diagram of morphisms will commute if and only if the corresponding diagram commutes in Sets.

Three objects

S_{1} = (S_{1}, Σ_{1}, k_{1} : S_{1} × Σ_{1} → [0, 1]),

S_{2} = (S_{2}, Σ_{2}, k_{2} : S_{2} × Σ_{2} → [0, 1]),

S = (S, Σ, k : S × Σ → [0, 1])

and morphisms f_{1} : S_{1} → S and f_{2} : S_{2} → S are given. We will show that the pullback of f_{1} and f_{2} exists.

Let U = {(s_{1}, s_{2}) ∈ S_{1} ×S_{2} | f_{1}(s_{1}) = f_{2}(s_{2})} equipped with the subspace topology of the product topology on S_{1} × S_{2}. The Borel σ-algebra Σ_{U} on U is generated by the set {(σ_{1} × σ_{2}) ∩ U | σ_{1} ∈ Σ_{1}, σ_{2} ∈ Σ_{2}}. Let π_{1} : U → S_{1} and π_{2} : U → S_{2} be the projection maps. Since f_{1} and f_{2} are surjective, U is not empty. We want to construct h : U × Σ_{U} → [0, 1] so that (U, Σ_{U}, h) is an object and π_{1} : U → S_{1} and π_{2} : U → S_{2} are morphisms. For an element x of a set X, an element y of a set Y, subsets A ⊆ X, B ⊆ Y and a function f : X → Y, we sometimes write x instead of {x}, fx instead of f(x), fA instead of f(A), and f^{−1}B instead of f^{−1}(B).

B.2 The conditional probabilities

We fix (s_{1}, s_{2}) ∈ U, i.e. s_{1} ∈ S_{1} and s_{2} ∈ S_{2} with f_{1}s_{1} = f_{2}s_{2}, throughout this paper. The index i always takes the values 1 and 2. The variable ω_{i} always runs through S_{i} whereas the variable s runs through S.

For i = 1, 2, we have the probability measures k_{i}(s_{i}, −) : Σ_{i} → [0, 1] on the space (S_{i}, Σ_{i}). Also Σ′_{i} = {f_{i}^{−1}σ | σ ∈ Σ} ⊆ Σ_{i} is a sub-σ-algebra of Σ_{i} (i = 1, 2). We therefore have, for a given σ_{i} ∈ Σ_{i}, the conditional probability distribution P ((s_{i}, σ_{i})|Σ′_{i}) : S_{i} → [0, 1] of the probability measure k_{i}(s_{i}, −) given the sub-σ-algebra Σ′_{i} ⊆ Σ_{i}. Since S_{i} is a Polish space we can assume [Dud89, Theorem 10.2.2] that P ((s_{i}, σ_{i})|Σ′_{i})(−) is a regular conditional probability distribution, i.e.

(i) P ((s_{i}, σ_{i})|Σ′_{i}) : S_{i} → [0, 1] is Σ′_{i} measurable and integrable.

(ii) For all γ′_{i} ∈ Σ′_{i}, we have

∫_{γ′_{i}} P ((s_{i}, σ_{i})|Σ′_{i})(ω_{i})k_{i}(s_{i}, dω_{i}) = k_{i}(s_{i}, σ_{i} ∩ γ′_{i}).

(iii) For k_{i}(s_{i}, −)-almost all ω_{i} ∈ S_{i}, P ((s_{i}, −)|Σ′_{i})(ω_{i}) : Σ_{i} → [0, 1] is a probability measure on S_{i}.

A regular conditional probability distribution, like a conditional probability distribution, is unique up to a set of measure zero, i.e. any two functions satisfying the above three properties are equal for k_{i}(s_{i}, −)-almost all ω_{i} ∈ S_{i}.

One should think of P ((s_{i}, σ_{i}), Σ′_{i})(ω_{i}) as the probability that s_{i} makes a transition to σ_{i} given that s_{i} makes a transition to f_{i}^{−1}f_{i}ω_{i}, or equivalently as the probability that s_{i} makes a transition to σ_{i} given that f_{i}s_{i} makes a transition to f_{i}ω_{i}.

By the standard method in the theory of conditional probability (see for example [Bil79, Exercise 33.5]), we can obtain the conditional probability distribution

P ((s_{i}, σ_{i})|Σ) : S → [0, 1].

Here, P ((s_{i}, σ_{i})|Σ)(s) gives the probability that s_{i} makes a transition to σ_{i} given that s_{i} makes a transition to some ω_{i} with f_{i}(ω_{i}) = s or equivalently the probability that s_{i} makes a transition to σ_{i} given that f_{i}s_{i} makes a transition to s. For the sake of completeness, we explain how this is obtained.

Since P ((s_{i}, σ_{i})|Σ′_{i}) : S_{i} → [0, 1] is constant on f_{i}^{−1}s for any σ ∈ S we can define

P ((s_{i}, σ_{i})|Σ) : S → [0, 1]

by P ((s_{i}, σ_{i})|Σ)(s) = P ((s_{i}, σ_{i})|Σ′_{i})(ω_{i}) for any ω_{i} ∈ f_{i}^{−1}s. Hence, P ((s_{i}, σ_{i})|Σ) ∘ f_{i} = P ((s_{i}, σ_{i})|Σ′_{i}), and P ((s_{i}, σ_{i})|Σ) has the following properties which are equivalent to the above three properties for P ((s_{i}, σ_{i})|Σ′_{i}):

(i) P ((s_{i}, σ_{i})|Σ) is Σ-measurable and integrable.

(ii) Since k_{i}(s_{i}, −) ∘ f_{i}^{−1} = k(f_{i}s_{i}, −), we have, for all σ ∈ Σ:

∫_{σ} P ((s_{i}, σ_{i})|Σ)k(f_{i}s_{i}, ds) = ∫_{f_{i}^{−1}σ} P ((s_{i}, σ_{i})|Σ′_{i})k_{i}(s_{i}, dω_{i}) = k_{i}(s_{i}, σ_{i} ∩ f_{i}^{−1}σ).

(iii) For k(f_{i}s_{i}, −)-almost all s, we have a probability measure

P ((s_{i}, −)|Σ)(s) : Σ_{i} → [0, 1]

on S_{i}.

As before, P ((s_{i}, σ_{i})|Σ) is unique up to a set of k(f_{i}s_{i}, −)-measure zero. Note that one can define

P ((s_{i}, σ_{i})|Σ) : S → [0, 1]

directly with the Radon-Nykodym derivative rather than using

P ((s_{i}, σ_{i})|Σ′_{i}) : S_{i} → [0, 1]

.

B.3 Construction of a probability measure on S_{1} × S_{2}

In order to define h((s_{1}, s_{2}), −) : Σ_{U} → [0, 1] we first define a probability measure g((s_{1}, s_{2}), −) : Σ_{S_{1}×S_{2}} → [0, 1] on the product space (S_{1}×S_{2}, Σ_{S_{1}×S_{2}}) where Σ_{S_{1}×S_{2}} is the Borel σ-algebra of S_{1} × S_{2}. We will then show in the next section that g((s_{1}, s_{2}), −) is supported on U, i.e. g((s_{1}, s_{2}), U) = 1. We will finally define h((s_{1}, s_{2}), α ∩ U) = g((s_{1}, s_{2}), α).

Let R = Σ_{1} × Σ_{2} be the collection of all “rectangles” σ_{1} × σ_{2} ∈ Σ_{S_{1}×S_{2}}; R is a semi-ring. For σ_{1} × σ_{2} ∈ R and s ∈ S, put

ρ((s_{1}, s_{2}), σ_{1} × σ_{2})(s) = P ((s_{1}, σ_{1})|Σ)(s)P ((s_{2}, σ_{2})|Σ)(s).

Since for k(f_{1}s_{1}, −)-almost all s ∈ S, P ((s_{1}, −)|Σ)(s) and P ((s_{2}, −)|Σ)(s) are probability measures on S_{1} and S_{2} respectively, we have:

Proposition B.1 [Dud89, Theorem 4.4.1]

For k(f_{1}s_{1}, −)-almost all s ∈ S, ρ((s_{1}, s_{2}), −)(s) is countably additive on R.

For σ_{1} × σ_{2} ∈ R, put

g((s_{1}, s_{2}), σ_{1} × σ_{2}) = ∫_{S} P ((s_{1}, σ_{1})|Σ)(s)P ((s_{2}, σ_{2})|Σ)(s)k(f_{1}s_{1}, ds). (2)

Proposition B.2 g((s_{1}, s_{2}), −) has a unique extension to a probability measure on (S_{1} × S_{2}, Σ_{S_{1}×S_{2}}).

Proof. We check that g((s_{1}, s_{2}), −) is countably additive on R. Let σ_{1}×σ_{2} = ⋃_{j∈J} σ_{j1} × σ_{j2} be the disjoint union of a countable set of rectangles. Then,

g((s_{1}, s_{2}), σ_{1} × σ_{2})

= ∫_{S} P ((s_{1}, σ_{1})|Σ)(s)P ((s_{2}, σ_{2})|Σ)(s)k(f_{1}s_{1}, ds)

= ∫_{S} ∑_{j∈J} P ((s_{1}, σ_{j1})|Σ)(s)P ((s_{2}, σ_{j2})|Σ)(s)k(f_{1}s_{1}, ds) by Proposition B.1
= ∑_{j∈J} ∫_{S} P ((s_{1}, σ_{j1})|Σ)(s)P ((s_{2}, σ_{j_{2}})|Σ)(s)k(f_{1}s_{1}, ds) monotone convergence

= ∑_{j∈J} g((s_{1}, s_{2}), σ_{j1} × σ_{j2}).

This establishes countable additivity. We next extend g((s_{1}, s_{2}), −) in the usual way [Dud89, page 102] to the ring A generated by the rectangles in R, i.e to the collection of all unions of finitely many disjoint elements of R: For a finite set of disjoint rectangles σ_{j1} × σ_{j2}, j = 1, ⋯, n, we put

g((s_{1}, s_{2}), ⋃_{1≤j≤n} σ_{j1} × σ_{j2}) = ∑_{1≤j≤n} g((s_{1}, s_{2}), σ_{j1} × σ_{j2}).

In fact A is an algebra of subsets of S_{1} × S_{2} since it contains S_{1} × S_{2}. Furthermore,

g((s_{1}, s_{2}), S_{1} × S_{2})

= ∫_{S} P ((s_{1}, S_{1})|Σ)(s)P ((s_{2}, S_{2})|Σ)(s)k(f_{1}s_{1}, ds)

= ∫_{S} k(f_{1}s_{1}, ds)  since P ((s_{2}, S_{2})|Σ)(s) = 1 a.e.

= 1.

Therefore by standard results in measure theory [Dud89, Theorems 3.1.4 and 3.1.10], g((s_{1}, s_{2}), −) has a unique extension to Σ_{S_{1}×S_{2}}, i.e., the σ-algebra generated by R or A.

B.4 Construction of h((s_{1}, s_{2}), −)

We will now show that g((s_{1}, s_{2}), U^{c}) = 0, where U^{c} is the complement of the set U. First note that U ⊆ S_{1} × S_{2} is a closed subset of the product topology on S_{1} × S_{2}. In fact, the diagonal D = {(s, s) | s ∈ S} is a closed subset of S × S equipped with the product topology and the function

(f_{1}, f_{2}) : S_{1} × S_{2} → S × S

with (f_{1}, f_{2})(ω_{1}, ω_{2}) = (f_{1}ω_{1}, f_{2}ω_{2}) is continuous. Hence, U is closed since it is the inverse image of the closed set D under the continuous map (f_{1}, f_{2}).

It follows that (S_{1} × S_{2}) \ U is an open subset of S_{1} × S_{2}. Since S_{i} is a Polish space, it has a countable basis B_{i} ⊆ Ω_{i} ⊆ Σ_{i} of open subsets, where Ω_{i} is the lattice of open subsets of S_{i} (i = 1, 2). Then B_{1} ×B_{2} forms a countable basis of open subsets of S_{1} × S_{2}. Therefore, (S_{1} × S_{2}) \ U is the countable union of open rectangles σ_{1} × σ_{2} with σ_{i} ∈ B_{i} (i = 1, 2). Hence, in order to show that U has full g((s_{1}, s_{2}), −)-measure, it is sufficient to prove

Proposition B.3 For any σ_{1} ∈ Σ_{1} and σ_{2} ∈ Σ_{2} with U ∩ (σ_{1} × σ_{2}) = ∅ we have g((s_{1}, s_{2}), σ_{1} × σ_{2}) = 0.

We prove the above Proposition by using the following technical lemmas. For the time being, we fix σ_{1} ∈ Σ and σ_{2} ∈ Σ_{2}. For convenience we use the notation μ(−) = k(f_{1}s_{1}, −).

Lemma B.4 The set f_{i}σ_{i} (and therefore its complement S_{i} \ f_{i}σ_{i}) is μmeasurable (i = 1, 2).

Proof. This follows from the fact that the continuous image of any Borel subset of a Polish space into any Hausdorff space Y is measurable (in particular) with respect to any Borel measure on Y [Fed69, statement 2.2.13].

Lemma B.5 There exists a measurable subset B_{i} ⊆ S \ f_{i}σ_{i} with μ(B_{i}) = μ(S \ f_{i}σ_{i}) such that for all s ∈ B_{i} we have P ((s_{i}, σ_{i})|Σ)(s) = 0.

Proof. Since, by Lemma B.4, S \ f_{i}σ_{i} is μ-measurable, there exists a Borel subset C_{i} ∈ Σ with C_{i} ⊆ S \ f_{i}σ_{i} such that μ(C_{i}) = μ(S \ f_{i}σ_{i}). Hence,

∫_{C_{i}} P ((s_{i}, σ_{i})|Σ)(s)μ(ds) = ∫_{C_{i}} P ((s_{i}, σ_{i})|Σ)(s)k(f_{i}s_{i}, ds)
= k_{i}(s_{i}, σ_{i} ∩ f_{i}^{−1}C_{i})
= 0,

since (σ_{i} ∩ f_{i}^{−1}C_{i}) ⊆ (σ_{i} ∩ f_{i}^{−1}(S \ f_{i}σ_{i})) = ∅. Therefore, there exists a μmeasurable subset B_{i} with B_{i} ⊆ C_{i} and μ(B_{i}) = μ(C_{i}) = μ(S \ f_{i}σ_{i}) such that P ((s_{i}, σ_{i})|Σ)(s) = 0 for all s ∈ B_{i}.

Proof of Proposition B.3 Since (σ_{1} ×σ_{2})∩U = ∅, we have f_{1}σ_{1} ∩f_{2}σ_{2} = ∅ or equivalently

(S \ f_{1}σ_{1}) ∪ (S \ f_{2}σ_{2}) = S.

It follows, by Lemma B.5, that μ(S \ (B_{1} ∪ B_{2})) = 0. Therefore, for μ-almost all s we have P ((s_{1}, σ_{1})|Σ)(s) = 0 or P ((s_{2}, σ_{2})|Σ)(s) = 0. In other words, for μ-almost all s, we have P ((s_{1}, σ_{1})|Σ)(s)P ((s_{2}, σ_{2})|Σ)(s) = 0. Hence,

g((s_{1}, s_{2}), σ_{1} × σ_{2}) = ∫_{S} P ((s_{1}, σ_{1})|Σ)(s)P ((s_{2}, σ_{2})|Σ)(s)μ(ds) = 0,

as required.

Corollary B.6 g((s_{1}, s_{2}), (S_{1} × S_{2}) \ U) = 0.

Proof. By Proposition B.3, g((s_{1}, s_{2}), (S_{1} × S_{2}) \ U) = 0, since (S_{1} × S_{2}) \ U) is the countable union of rectangles disjoint from U.

Any element of Σ_{U} is of the form α ∩ U with α ∈ Σ_{S_{1}×S_{2}}. We now define h((s_{1}, s_{2}), α ∩ U) = g((s_{1}, s_{2}), α).

Theorem B.7 (U, Σ_{U}, h : U × Σ_{U} → [0, 1]) is an object of the category and π_{i} : U → S_{i} are morphisms.

Proof. Clearly U is a Polish space as it is a closed subset of the Polish space S_{1} × S_{2}. We have already shown that h((s_{1}, s_{2}), −) is a probability measure on U for any (s_{1}, s_{2}) ∈ U. Finally, for any σ_{1} ∈ Σ_{1} we have:

h((s_{1}, s_{2}), π_{1}^{−1}σ_{1})

= h((s_{1}, s_{2}), (σ_{1} × S_{2}) ∩ U)

= g((s_{1}, s_{2}), σ_{1} × S_{2})

= ∫_{S} P ((s_{1}, σ_{1})|Σ)(s)P ((s_{2}, S_{2})|Σ)(s)k(f_{1}s_{1}, ds)

= ∫_{S} P ((s_{1}, σ_{1})|Σ)(s)k(f_{1}s_{1}, ds)  P ((s_{2}, S_{2})|Σ)(s) = 1 a.e.

= k_{1}(s_{1}, f_{1}^{−1}(s) ∩ σ_{1}) = k_{1}(s_{1}, σ_{1}).

Therefore π_{1} is a morphism. Similarly π_{2} is a morphism.

Remark B.8 If we are dealing with discrete processes, i.e. if S_{1}, S_{2} and S are countable discrete spaces, then Equation 2 reduces to a sum and we get

\begin{aligned}h((s_{1}, s_{2}), (σ_{1} × σ_{2}) ∩ U) & = & g((s_{1}, s_{2}), σ_{1} × σ_{2}) \\ & = & ∑_{s∈S}P ((s_{1}, σ_{1})|Σ)(s)P ((s_{2}, σ_{2})|Σ)(s)k(f_{1}s_{1}, s). \end{aligned}

Since, for k(f_{i}s_{i}, s) ≠ 0 we have

P ((s_{i}, σ_{i})|Σ)(s) = \frac{k_{i}(s_{i}, σ_{i})}{k(f_{i}s_{i}, s)},

we obtain

P ((s_{1}, σ_{1})|Σ)(s)P ((s_{2}, σ_{2})|Σ)(s)k(f_{1}s_{1}, s) = \{ \begin{matrix}\frac{k_{1}(s_{1}, σ_{1})k_{2}(s_{2}, σ_{2})}{k(f_{1}s_{1}, s)} & if k(f_{1}s_{1}, s) ≠ 0 \\ 0 & otherwise. \end{matrix}

B.5 The pullback property

We show that (U, Σ_{U}, h : U × Σ_{U} → [0, 1]) and π_{i} : U → S_{i} (i = 1, 2) give the pullback of f_{i} : S_{i} → S (i = 1, 2).

Let (T, Σ_{T} , r : T × Σ_{T} → [0, 1]) be an object and g_{i} : T → S_{i} (i = 1, 2) be morphisms such that f_{1} ∘ g_{1} = f_{2} ∘ g_{2}. Let t ∈ T and σ_{i} ∈ Σ_{i} (i = 1, 2).

Lemma B.9 For k(f_{i}g_{i}t, −)-almost all s ∈ S,

P ((g_{i}t, σ_{i})|Σ)(s) = P ((t, g_{i}^{−1}σ_{i})|Σ)(s).

Proof. We have, for any σ ∈ Σ,

∫_{σ} P ((g_{i}t, σ_{i})|Σ)(s)k(f_{i}g_{i}t, ds) = k_{i}(g_{i}t, σ_{i} ∩ f_{i}^{−1}σ),

and also

∫_{σ} P ((t, g_{i}^{−1}σ_{i})|Σ)(s)k(f_{i}g_{i}t, ds) = r(t, (g_{i}^{−1}σ_{i}) ∩ (g_{i}^{−1}f_{i}^{−1}σ))
= r(t, g_{i}^{−1}(σ_{i} ∩ f_{i}^{−1}σ))
= k_{i}(g_{i}t, σ_{i} ∩ f_{i}^{−1}σ).

It follows that the conditional probability P ((g_{i}t, σ_{i})|Σ)(−) is a version of P ((t, g_{i}^{−1}σ_{i})|Σ)(−) and hence they are equal for k(f_{i}g_{i}t, −)-almost all s ∈ S.

Theorem B.10 (U, Σ_{U}, h(−, −)) with π_{i} : U → S_{i} (i = 1, 2) is the pullback of f_{i} : S_{i} → S (i = 1, 2).

Proof. Let q : T → U be given by q(t) = (g_{1}t, g_{2}t). We show that q : (T, Σ_{T} , r) → (U, Σ_{U}, h) is a morphism and is the unique mediating morphism making the pullback diagram commute. To show that q is a morphism, we need to check that

r(t, q^{−1}α) = h((g_{1}t, g_{2}t), α),  (3)

for all α ∈ Σ_{U}. The sub-σ-algebra Σ′_{T} = {q^{−1}α|α ∈ Σ_{U}} ⊆ Σ_{T} is isomorphic with Σ_{U}. By Proposition B.2, h((s_{1}, s_{2}), −) is uniquely determined by its values on Σ′_{U} = {(σ_{1} × σ_{2}) ∩ U|σ_{i} ∈ Σ_{i}}. Hence, r(t, −) : Σ′_{T} → [0, 1] is uniquely determined by its values on q^{−1}(Σ′_{U}). It therefore suffices to show that Equation (3) holds for all α ∈ Σ′_{U}. Let α = (σ_{1} × σ_{2}) ∩ U with σ_{1} ∈ Σ_{1} and σ_{2} ∈ Σ_{2}. Note that

q^{−1}(α) = {t ∈ T |g_{1}t ∈ σ_{1}, g_{2}t ∈ σ_{2}} = (g_{1}^{−1}σ_{1}) ∩ (g_{2}^{−1}σ_{2}).

Therefore,

r(t, q^{−1}α)

= r(t, g_{1}^{−1}σ_{1} ∩ g_{2}^{−1}σ_{2})

= ∫_{S} P ((t, g_{1}^{−1}σ_{1})|Σ)(s)P ((t, g_{2}^{−1}σ_{2})|Σ)(s)k(f_{1}g_{1}t, ds)

= ∫_{S} P ((g_{1}t, σ_{1})|Σ)(s)P ((g_{2}t, σ_{2})|Σ)(s)k(f_{1}g_{1}t, ds)  by Lemma B.9

= h((g_{1}t, g_{2}t), α).

This shows that q is a morphism. Its uniqueness follows from the corresponding uniqueness in Sets. Finally, g_{i} = π_{i} ∘ q (i = 1, 2) follows from the corresponding equality in Sets.

References

[AHS96] R. Alur, T. Henzinger, and E. Sontag, editors. Hybrid Systems III, number 1066 in Lecture Notes in Computer Science. Springer-Verlag, 1996.

[AM89] P. Aczel and N. Mendler. A final-coalgebra theorem. In Category Theory and Computer Science, Lecture Notes In Computer Science, pages 357–365, 1989.

[Ash72] R. B. Ash. Real Analysis and Probability. Academic Press, 1972.

[Bil79] P. Billingsley. Probability and Measure. Wiley-Interscience, 1979.

[BK96]  C. Baier and M. Kwiatkowska.  Domain equations

for probabilistic processes. Available from URL http://www.cs.bham.ac.uk/ mzk/, March 1996.

[BLL^{+}96] J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Uppaal: A tool suite for automatic verification of real-time systems. In R. Alur, T. Henzinger, and E. Sontag, editors, Hybrid Systems III, number 1066 in Lecture Notes In Computer Science, pages 232–243, 1996.

[Chr90] I. Christoff. Testing equivalences and fully abstract models for probabilistic processes. In CONCUR 90, number 458 in Lecture Notes In Computer Science. Springer-Verlag, 1990.

[CM65] D. R. Cox and H. Miller. An Introduction to the Theory of Stochastic Processes. Dunno, 1965.

[CN95] A. Cheng and M. Nielsen. Open maps at work. In P. S. Thiagarajan, editor, Proceedings of the 15th Annual Conference on Foundations of Software Technology and Theoretical Computer Science, volume 1026 of Lecture Notes In Computer Science. Springer-Verlag, 1995.

[CSZ92] R. Cleaveland, S. Smolka, and A. Zwarico. Testing preorders for probabilistic processes. In Proceedings of the International Colloquium On Automata Languages And Programming 1992, number 623 in Lecture Notes In Computer Science. Springer-Verlag, 1992.

[Dud89] R. M. Dudley. Real Analysis and Probability. Wadsworth and Brookes/Cole, 1989.

[dVR] E. de Vink and J. J. M. M. Rutten. Probabilistic bisimulation for metric transition systems. In preparation.

[Eda96] A. Edalat. The category of markov processes on polish spaces with transition probability preserving continuous surjections has pullbacks. Available from theory.doc.ic.ac.uk in the direc-

tory /people/Edalat/markov.ps, 1996.

[Fed69] H. Federer. Geometric Measure Theory. Springer-Verlag, 1969.

[Gir81] Michèle Giry. A categorical approach to probability theory. In B. Banaschewski, editor, Categorical Aspects of Topology and Analysis, number 915 in Lecture Notes In Mathematics, pages 68–85. Springer-Verlag, 1981.

[Hal74] P. Halmos. Measure Theory. Number 18 in Graduate Texts in Mathematics. Springer-Verlag, 1974. Originally published in 1950.

[HHWT95] T. Henzinger, P.-H. Ho, and H. Wong-Toi. Hytech: the next generation. In Proceedings of the 16th Annual Real-time Systems Symposium, pages 55–65. IEEE Computer Society Press, 1995.

[Hil94] Jane Hillston. A Compositional Approach to Performance Modelling. PhD thesis, University of Edinburgh, 1994. To be published as a Distinguished Dissertation by Cambridge University Press.

[HK96] M. Huth and M. Kwiatkowska. On probabilistic model checking. Technical Report CSR-96-15, University of Birmingham, 1996. available from http://www.cs.bham.ac.uk/ mzk/.

[Hoa85] C. A. R. Hoare. Communicating Sequential Processes. Series in Computer Science. Prentice-Hall International, London, 1985.

[JL91] B. Jonsson and K. Larsen. Specification and refinement of probabilistic processes. In Proceedings of the 6th Annual IEEE Symposium On Logic In Computer Science, 1991.

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

[JY95] B. Jonsson and W. Yi. Compositional testing preorders for probabilistic processes. In Proceedings of the 10th Annual IEEE Symposium On Logic In Computer Science, 1995.

[Koz81] D. Kozen. Semantics of probabilistic programs. Journal of Computer and Systems Sciences, 22:328–350, 1981.

[Koz85] D. Kozen. A probabilistic PDL. Journal of Computer and Systems Sciences, 30(2):162–178, 1985.

[KT66] J. F. C. Kingman and S. J. Taylor. Introduction to Measure and Probability. Cambridge University Press, 1966.

[LS91] K. G. Larsen and A. Skou. Bisimulation through probablistic testing. Information and Computation, 94:1–28, 1991.

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

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

[Par67] K. R. Parthasarathy. Probability Measures on Metric Spaces. Academic Press, 1967.

[Pop94] Sally Popkorn. First Steps in Modal Logic. Cambridge University Press, 1994.

[Pro]  Probabilistic systems group, collected reports.  Avail-

able from www.comlab.ox.ac.uk in the directory

/oucl/groups/probs/bibliography.html.

[Rud66] W. Rudin. Real and Complex Analysis. McGraw-Hill, 1966.

[Rut95] J. J. M. M. Rutten. A calculus of transition systems (towards universal coalgebra). In A. Ponse, M. de Rijke, and Y. Venema, editors, Modal Logic and Process Algebra, a bisimulation perspective, number 53 in CSLI Lecture Notes, 1995. Available electronically from www.cwi.nl/~janr.

[SD78] N. Saheb-Djahromi. Probabilistic LCF. In Mathematical Foundations Of Computer Science, number 64 in Lecture Notes In Computer Science. Springer-Verlag, 1978.

[SD80] N. Saheb-Djahromi. Cpos of measures for nondeterminism. Theoretical Computer Science, 12(1):19–37, 1980.

[Sif77] J. Sifakis. Use of petri nets for performance evaluation. In H. Beilner and E. Gelenbe, editors, Measuring, Modeling and Evaluating Computer Systems, pages 75–93. North-Holland, 1977.

[SL94] R. Segala and N. Lynch. Probabilistic simulations for probabilistic processes. In B. Jonsson and J. Parrow, editors, Proceedings of CONCUR94, number 836 in Lecture Notes In Computer Science, pages 481–496. Springer-Verlag, 1994.

[vGSST90] R. van Glabbeek, S. Smolka, B. Steffen, and C. Tofts. Reactive generative and stratified models for probabilistic processes. In Proceedings of the 5th Annual IEEE Symposium On Logic In Computer Science, 1990.

[Win96] G. Winskel. Unpublished notes. Private Communication, 1996.

[WN95] G. Winskel and M. Nielsen. Handbook of Logic in Computer Science, volume 4, chapter Models for Concurrency. Oxford University Press, 1995.

Recent BRICS Report Series Publications

RS-97-4 Richard Blute, Josée Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for Labelled Markov Processes. March 1997. 48 pp. To appear in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings.

RS-97-3 Carsten Butz and Ieke Moerdijk. A Definability Theorem for First Order Logic. March 1997. 10 pp.

RS-97-2 David A. Schmidt. Abstract Interpretation in the Operational Semantics Hierarchy. March 1997. 33 pp.

RS-97-1 Olivier Danvy and Mayer Goldberg. Partial Evaluation of the Euclidian Algorithm (Extended Version). January 1997. 16 pp. To appear in the journal Lisp and Symbolic Computation.

RS-96-62 P. S. Thiagarajan and Igor Walukiewicz. An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces. December 1996. i+13 pp. To appear in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings.

RS-96-61 Sergei Soloviev. Proof of a Conjecture of S. Mac Lane. December 1996. 53 pp. Extended abstract appears in Pitt, Rydeheard and Johnstone, editors, Category Theory and Computer Science: 6th International Conference, CTCS ’95 Proceedings, LNCS 953, 1995, pages 59–80.

RS-96-60 Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal in 1995. December 1996. 5 pp. Appears in Margaria and Steffen, editors, Tools and Algorithms for The Construction and Analysis of Systems: 2nd International Workshop, TACAS ’96 Proceedings, LNCS 1055, 1996, pages 431–434.

RS-96-59 Kim G. Larsen, Paul Pettersson, and Wang Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. December 1996. 12 pp. Appears in 16th IEEE Real-Time Systems Symposium, RTSS ’95 Proceedings, 1995.

RS-96-58 Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal — a Tool Suite for Automatic Verification of Real–Time Systems. December 1996. 12 pp. Appears in Alur, Henzinger and Sontag, editors, DIMACS