BRICS

Basic Research in Computer Science

Probabilistic Event Structures and Domains

Daniele Varacca Hagen Völzer Glynn Winskel BRICS Report Series RS-04-10 ISSN 0909-0878 June 2004 BRICS RS-04-10 Varacca et al.: Probabilistic Event Structures and Domains Copyright \begin{matrix}c \\ ◯ \end{matrix} 2004, Daniele Varacca & Hagen Völzer & Glynn

Winskel. BRICS, Department of Computer Science University of Aarhus. All rights reserved.

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

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

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

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

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

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

This document in subdirectory RS/04/10/

Probabilistic Event Structures and Domains

Daniele Varacca^{1}^{⋆}, Hagen Völzer^{2}, and Glynn Winskel^{3}

1 LIENS - École Normale Supérieure, France 2 Institut für Theoretische Informatik - Universität zu Lübeck, Germany 3 Computer Laboratory - University of Cambridge, UK

Abstract. This paper studies how to adjoin probability to event structures, leading to the model of probabilistic event structures. In their simplest form probabilistic choice is localised to cells, where conflict arises; in which case probabilistic independence coincides with causal independence. An application to the semantics of a probabilistic CCS is sketched. An event structure is associated with a domain—that of its configurations ordered by inclusion. In domain theory probabilistic processes are denoted by continuous valuations on a domain. A key result of this paper is a representation theorem showing how continuous valuations on the domain of a confusion-free event structure correspond to the probabilistic event structures it supports. We explore how to extend probability to event structures which are not confusion-free via two notions of probabilistic runs of a general event structure. Finally, we show how probabilistic correlation and probabilistic event structures with confusion can arise from event structures which are originally confusion-free by using morphisms to rename and hide events.

1 Introduction

There is a central divide in models for concurrent processes according to whether they represent parallelism by nondeterministic interleaving of actions or directly as causal independence. Where a model stands with respect to this divide affects how probability is adjoined. Most work has been concerned with probabilistic interleaving models [LS91,Seg95,DEP02]. In contrast, we propose a probabilistic causal model, a form of probabilistic event structure.

An event structure consists of a set of events with relations of causal dependency and conflict. A configuration (a state, or partial run of the event structure) consists of a subset of events which respects causal dependency and is conflict free. Ordered by inclusion, configurations form a special kind of Scott domain [NPW81].

The first model we investigate is based on the idea that all conflict is resolved probabilistically and locally. This intuition leads us to a simple model based on confusionfree event structures, a form of concrete data structures [KP93], but where computation proceeds by making a probabilistic choice as to which event occurs at each currently accessible cell. (The probabilistic event structures which arise are a special case of those studied by Katoen [Kat96]—though our concentration on the purely probabilistic case and the use of cells makes the definition simpler.) Such a probabilistic event structure

⋆ Work partially done as PhD student at BRICS

immediately gives a “probability” weighting to each configuration got as the product of the probabilities of its constituent events. We characterise those weightings (called configuration valuations) which result in this way. Understanding the weighting as a true probability will lead us later to the important notion of probabilistic test.

Traditionally, in domain theory a probabilistic process is represented as a continuous valuation on the open sets of a domain, i.e., as an element of the probabilistic powerdomain of Jones and Plotkin [JP89]. We reconcile probabilistic event structures with domain theory, lifting the work of [NPW81] to the probabilistic case, by showing how they determine continuous valuations on the domain of configurations. In doing so however we do not obtain all continuous valuations. We show that this is essentially for two reasons: in valuations probability can “leak” in the sense that the total probability can be strictly less than 1; more significantly, in a valuation the probabilistic choices at different cells need not be probabilistically independent. In the process we are led to a more general definition of probabilistic event structure from which we obtain a key representation theorem: continuous valuations on the domain of configurations correspond to the more general probabilistic event structures.

How do we adjoin probabilities to event structures which are not necessarily confusion-free? We argue that in general a probabilistic event structure can be identified with a probabilistic run of the underlying event structure and that this corresponds to a probability measure over the maximal configurations. This sweeping definition is backed up by a precise correspondence in the case of confusion-free event structures. Exploring the operational content of this general definition leads us to consider probabilistic tests comprising a set of finite configurations which are both mutually exclusive and exhaustive. Tests do indeed carry a probability distribution, and as such can be regarded as finite probabilistic partial runs of the event structure.

Finally we explore how phenomena such as probabilistic correlation between choices and confusion can arise through the hiding and relabeling of events. To this end we present some preliminary results on “tight” morphisms of event structures, showing how, while preserving continuous valuations, they can produce such phenomena.

2 Probabilistic Event Structures

2.1 Event Structures

An event structure is a triple E = ⟨E, ≤, #⟩ such that

• E is a countable set of events;

• ⟨E, ≤⟩ is a partial order, called the causal order, such that for every e ∈ E, the set of events ↓ e is finite;

• # is an irreflexive and symmetric relation, called the conflict relation, satisfying the following: for every e_{1}, e_{2}, e_{3} ∈ E if e_{1} ≤ e_{2} and e_{1} # e_{3} then e_{2} # e_{3}.

We say that the conflict e_{2} # e_{3} is inherited from the conflict e_{1} # e_{3}, when e_{1} < e_{2}. Causal dependence and conflict are mutually exclusive. If two events are not causally dependent nor in conflict they are said to be concurrent.

A configuration x of an event structure E is a conflict-free downward closed subset of E, i.e., a subset x of E satisfying: (1) whenever e ∈ x and e′ ≤ e then e′ ∈ x and (2) for every e, e′ ∈ x, it is not the case that e # e′. Therefore, two events of a configuration are either causally dependent or concurrent, i.e., a configuration represents a run of an event structure where events are partially ordered. The set of configurations of E, partially ordered by inclusion, is denoted as L(E). The set of finite configurations is written by L_{fin}(E). We denote the empty configuration by ⊥.

If x is a configuration and e is an event such that e ∉ x and x∪{e} is a configuration, then we say that e is enabled at x. Two configurations x, x′ are said to be compatible if x ∪ x′ is a configuration. For every event e of an event structure E, we define [e] := ↓ e, and [e) := [e] \ {e}. It is easy to see that both [e] and [e) are configurations for every event e and that therefore any event e is enabled at [e).

We say that events e_{1} and e_{2} are in immediate conflict, and write e_{1} #_{μ} e_{2} when e_{1} # e_{2} and both [e_{1}) ∪ [e_{2}] and [e_{1}] ∪ [e_{2}) are configurations. Note that the immediate conflict relation is symmetric. It is also easy to see that a conflict e_{1} # e_{2} is immediate if and only if there is a configuration where both e_{1} and e_{2} are enabled. Every conflict is either immediate or inherited from an immediate conflict.

Lemma 2.1. In an event structure, e # e′ if and only if there exist e_{0}, e′_{0} such that e_{0} ≤ e, e′_{0} ≤ e′, e_{0} #_{μ} e′_{0}.

Proof. Consider the set ([e] × [e′]) ∩ # consisting of the pairs of conflicting events, and order it componentwise. Consider a minimal such pair (e_{0}, e′_{0}). By minimality, any event in [e_{0}) is not in conflict with any event in [e′_{0}]. Since they are both lower sets we have that [e_{0}) ∪ [e′_{0}] is a configuration. Analogously for [e_{0}] ∪ [e′_{0}). By definition e_{0} #_{μ} e′_{0}. The other direction follows from the definition of #. □

2.2 Confusion-free Event Structures

The most intuitive way to add probability to an event structure is to identify “probabilistic events”, such as coin flips, where probability is associated locally. A probabilistic event can be thought of as probability distribution over a cell, that is, a set of events (the outcomes) that are pairwise in immediate conflict and that have the same set of causal predecessors. The latter implies that all outcomes are enabled at the same configurations, which allows us to say that the probabilistic event is either enabled or not enabled at a configuration.

Definition 2.2. A partial cell is a set c of events such that e, e′ ∈ c implies e #_{μ} e′ and [e) = [e′). A maximal partial cell is called a cell.

We will now restrict our attention to event structures where each immediate conflict is resolved through some probabilistic event. That is, we assume that cells are closed under immediate conflict. This implies that cells are pairwise disjoint.

Definition 2.3. An event structure is confusion-free if its cells are closed under immediate conflict.

Proposition 2.4. An event structure is confusion-free if and only if the reflexive closure of immediate conflict is transitive and inside cells, the latter meaning that e #_{μ} e′ ⟹ [e) = [e′).

Proof. Take an event structure E. Suppose it is confusion-free. Consider three events e, e′, e′′ such that e #_{μ} e′ and e′ #_{μ} e′′. Consider a cell c containing e (there exists one by Zorn’s lemma). Since c is closed under immediate conflict, it contains e′. By definition of cell [e) = [e′). Also, since c contains e′, it must contain e′′. By definition of cell, e #_{μ} e′′.

For the other direction we observe that if the immediate conflict is transitive, the reflexive closure of immediate conflict is an equivalence. If immediate conflict is inside cells, the cells coincide with the equivalence classes. In particular they are closed under immediate conflict. □

In a confusion-free event structure, if an event e ∈ c is enabled at a configuration x, all the events of c are enabled as well. In such a case we say that the cell c is accessible at x. The set of accessible cells at x is denoted by Acc(x). Confusion-free event structures correspond to deterministic concrete data structures [NPW81,KP93] and to confusionfree occurrence nets [NPW81].

We find it useful to define cells without directly referring to events. To this end we introduce the notion of covering.

Definition 2.5. Given two configurations x, x′ ∈ L(E) we say that x′ covers x (written x ◁ x′) if there exists e ∉ x such that x′ = x ∪ {e}. For every finite configuration x of a confusion-free event structure, a partial covering at x is a set of pairwise incompatible configurations that cover x. A covering at x is a maximal partial covering at x.

Proposition 2.6. In a confusion-free event structure if C is a covering at x, then c = {e | x ∪ {e} ∈ C} is a cell accessible at x. Conversely, if c is accessible at x, then C := {x ∪ {e} | e ∈ c} is a covering at x.

Proof. See Appendix B. □

In confusion-free event structures, we extend the partial order notation to cells by writing e < c′ if for some event e′ ∈ c′ (and therefore for all such) e < e′. We write c < c′ if for some (unique) event e ∈ c, e < c′. By [c) we denote the set of events e such that e < c.

2.3 Probabilistic Event Structures with Independence

Once an event structure is confusion-free, we can associate a probability distribution with each cell. Intuitively it is as if we have a die local to each cell, determining the probability with which the events at that cell occur. In this way we obtain our first definition of a probabilistic event structure, a definition in which dice at different cells are assumed probabilistically independent.

Definition 2.7. When f : X → [0, +∞] is a function, for every Y ⊆ X, we define f[Y] := ∑_{x∈Y} f(x). A cell valuation on a confusion-free event structure ⟨E, ≤, #⟩ is a function p : E → [0, 1] such that for every cell c, we have p[c] = 1.

Assuming probabilistic independence of all probabilistic events, every finite configuration can be given a “probability” which is obtained as the product of probabilities of its constituent events. This gives us a function L_{fin}(E) → [0, 1] which we can characterise in terms of the order-theoretic structure of L_{fin}(E) by using coverings.

Proposition 2.8. Let p be a cell valuation and let v : L_{fin}(E) → [0, 1] be defined by v(x) = Π_{e∈x}p(e). Then we have

(a) (Normality) v(⊥) = 1;

(b) (Conservation) if C is a covering at x, then v[C] = v(x);

(c) (Independence) if x, y are compatible, then v(x) · v(y) = v(x ∪ y) · v(x ∩ y).

Proof. Straightforward. □

Definition 2.9. A configuration valuation with independence on a confusion-free event structure E is a function v : L_{fin}(E) → [0, 1] that satisfies normality, conservation and independence. The configuration valuation associated with a cell valuation p as in Prop. 2.8 is denoted by v_{p}.

Lemma 2.10. If v : L_{fin}(E) → [0, 1] satisfies conservation, then it is contravariant, i.e.:

x ⊆ x′ ⟹ v(x) ≥ v(x′) .

Proof. By induction on the cardinality of x′ \ x. If x = x′ then v(x) = v(x′). Take x ⊆ x′ and consider a maximal event e in x′ \ x. Let x′′ := x′ \ {e}. By induction hypothesis v(x) ≥ v(x′′). Let c be the cell of e and C be the c-covering of x′′. By conservation, ∑_{y∈C} v(y) = v(x′′). Since for every y ∈ C we have that v(y) ≥ 0, then it must also be that v(y) ≤ v(x′′). But x′ ∈ C so that v(x′) ≤ v(x′′) ≤ v(x). □

Proposition 2.11. If v is a configuration valuation with independence and p : E → [0, 1] is a mapping such that v([e]) = p(e) · v([e)) for all e ∈ E, then p is a cell valuation such that v_{p} = v.

Proof. See Appendix B. □

Independence is essential to prove Proposition 2.11. We will show later (Theorem 5.3) the sense in which this condition amounts to probabilistic independence.

We give an example. Take the following confusion-free event structure E_{1}: E_{1} = {a, b, c, d} with the discrete causal ordering and with a #_{μ} b and c #_{μ} d. We represent immediate conflict by a curly line.

[figure: a; b; c; d]

We define a cell valuation on E_{1} by p(a) = 1/3, p(b) = 2/3, p(c) = 1/4, p(d) = 3/4. The corresponding configuration valuation is defined as

• v_{p}(⊥) = 1;

• v_{p}({a}) = 1/3, v_{p}({b}) = 2/3, v_{p}({c}) = 1/4, v_{p}({d}) = 3/4;

• v_{p}({a, c}) = 1/12, v_{p}({b, c}) = 1/6, v_{p}({a, d}) = 1/4, v_{p}({b, d}) = 1/2.

In the event structure above, a covering at ⊥ consists of {a}, {b}, while a covering at {a} consists of {a, c}, {a, d}.

We conclude this section with a definition of a probabilistic event structure. Though, as the definition indicates, we will consider a more general definition later, one in which there can be probabilistic correlations between the choices at different cells.

Definition 2.12. A probabilistic event structure with independence consists of a confusion-free event structure together with a configuration valuation with independence.

3 A Process Language

Confusion-freeness is a strong requirement. But it is still possible to give a semantics to a fairly rich language for probabilistic processes in terms of probabilistic event structures with independence. The language we sketch is a probabilistic version of value passing CCS. Following an idea of Milner, used in the context of confluent processes [Mil89], we restrict parallel composition so that there is no ambiguity as to which two processes can communicate at a channel; parallel composition will then preserve confusion-freeness.

Assume a set of channels L. For simplicity we assume that a common set of values V may be communicated over any channel a ∈ L. The syntax of processes is given by:

P ::= 0 | ∑_{v∈V} a!(p_{v}, v).P_{v} | a?(x).P | P_{1}∥P_{2} | P \ A |

P [f] | if b then P_{1} else P_{2} | X | rec X.P

Here x ranges over value variables, X over process variables, A over subsets of channels and f over injective renaming functions on channels, b over boolean expressions (which make use of values and value variables). The coefficients p_{v} are real numbers such that ∑_{v∈V} p_{v} = 1.

A closed process will denote a probabilistic event structure with independence, but with an additional labelling function from events to output labels a!v, input labels a?v where a is a channel and v a value, or τ. At the cost of some informality we explain the probabilistic semantics in terms of CCS constructions on the underlying labelled event structures, in which we treat pairs of labels consisting of an output label a!v and input label a?v as complementary. (See e.g. the handbook chapter [WN95] or [Win82,Win87] for an explanation of the event structure semantics of CCS.) For simplicity we restrict attention to the semantics of closed process terms.

The nil process 0 denotes the empty probabilistic event structure. A closed output process ∑_{v∈V} a!(p_{v}, v).P_{v} can perform a synchronisation at channel a, outputting a value v with probability p_{v}, whereupon it resumes as the process P_{v}. Each P_{v}, for v ∈ V, will denote a labelled probabilistic event structure with underlying labelled event structure E[[P_{v}]]. The underlying event structure of such a closed output process is got by the juxtaposition of the family of prefixed event structures

a!v.E[[P_{v}]] ,

with v ∈ V, in which the additional prefixing events labelled a!v are put in (immediate) conflict; the new prefixing events labelled a!v are then assigned probabilities p_{v} to obtain the labelled probabilistic event structure.

A closed input process a?(x).P synchronises at channel a, inputting a value v and resuming as the closed process P [v/x]. Such a process P [v/x] denotes a labelled probabilistic event structure with underlying labelled event structure E[[P [v/x]]]. The underlying labelled event structure of the input process is got as the parallel juxtaposition of the family of prefixed event structures

a?v.E[[P [v/x]]] ,

with v ∈ V; the new prefixing events labelled a?v are then assigned probabilities 1.

The probabilistic parallel composition corresponds to the usual CCS parallel composition followed by restricting away on all channels used for communication. In order for the parallel composition P_{1}∥P_{2} to be well formed the set of input channels of P_{1} and P_{2} must be disjoint, as must be their output channels. So, for instance, it is not possible to form the parallel composition

∑_{v∈V} a!(p_{v}, v).0∥a?(x).P_{1}∥a?(x).P_{2} .

In this way we ensure that no confusion is introduced through synchronisation.

We first describe the effect of the parallel composition on the underlying event structures of the two components, assumed to be E_{1} and E_{2}. This is got by CCS parallel composition followed by restricting away events in a set S:

(E_{1} | E_{2}) \ S

where S consists of all labels a!v, a?v for which a!v appears in E_{1} and a?v in E_{2}, or vice versa. In this way any communication between E_{1} and E_{2} is forced when possible. The newly introduced τ-events, corresponding to a synchronisation between an a!vevent with probability p_{v} and an a?v-event with probability 1, are assigned probability p_{v}.

A restriction P \ A has the effect of the CCS restriction

E[[P]] \ {a!v, a?v | v ∈ V & a ∈ A}

on the underlying event structure; the probabilities of the events which remain stay the same. A renaming P [f] has the usual effect on the underlying event structure, probabilities of events being maintained. A closed conditional (if b then P_{1} else P_{2}) has the denotation of P_{1} when b is true and of P_{2} when b is false.

The recursive definition of probabilistic event structures follows that of event structures [Win87] carrying the extra probabilities along. Though care must be taken to ensure that a confusion-free event structure results: one way to ensure this is to insist that for rec X.P to be well-formed the process variable X may not occur under a parallel composition.

4 Probabilistic Event Structures and Domains

The configurations ⟨L(E), ⊆⟩ of a confusion-free event structure E, ordered by inclusion, form a domain, specifically a distributive concrete domain (cf. [NPW81,KP93]). In traditional domain theory, a probabilistic process is denoted by a continuous valuation. Here we show that, as one would hope, every probabilistic event structure with independence corresponds to a unique continuous valuation. However not all continuous valuations arise in this way. Exploring why leads us to a more liberal notion of a configuration valuation, in which there may be probabilistic correlation between cells. This provides a representation of the normalised continuous valuations on distributive concrete domains in terms of probabilistic event structures. (Appendix A includes a brief survey of the domain theory we require and some of the rather involved proofs of this section. All proofs of this section can be found in [Var03].)

4.1 Domains

The configurations of an event structure form a coherent ω-algebraic domain, whose compact elements are the finite configurations [NPW81]. The domain of configurations of a confusion free has an independent equivalent characterisation as distributive concrete domain (for a formal definition of what this means, see [KP93]).

The probabilistic powerdomain of Jones and Plotkin [JP89] consists of continuous valuations, to be thought of as denotations of probabilistic processes. A continuous valuation on a DCPO D is a function ν defined on the Scott open subsets of D, taking values on [0, +∞], and satisfying:

• (Strictness) ν(∅) = 0;

• (Monotonicity) U ⊆ V ⟹ ν(U) ≤ ν(V);

• (Modularity) ν(U) + ν(V) = ν(U ∪ V) + ν(U ∩ V);

• (Continuity) if J is a directed family of open sets, ν( ⋃ J ) = sup_{U∈J} ν(U).

A continuous valuation ν is normalised if ν(D) = 1. Let V^{1}(D) denote the set of normalised continuous valuations on D equipped with the pointwise order: ν ≤ ξ if for all open sets U, ν(U) ≤ ξ(U). V^{1}(D) is a DCPO [JP89,Eda95].

The open sets in the Scott topology represent observations. If D is an algebraic domain and x ∈ D is compact, the principal set ↑ x is open. Principal open sets can be thought of as basic observations. Indeed they form a basis of the Scott topology.

Intuitively a normalised continuous valuation ν assigns probabilities to observations. In particular we could think of the probability of a principal open set ↑ x as representing the probability of x.

4.2 Continuous and Configuration Valuations

As can be hoped, a configuration valuation with independence on a confusion-free event structure E corresponds to a normalised continuous valuation on the domain ⟨L(E), ⊆⟩, in the following sense.

Proposition 4.1. For every configuration valuation with independence v on E there is a unique normalised continuous valuation ν on L(E) such that for every finite configuration x, ν(↑ x) = v(x).

Proof. The claim is a special case of the subsequent Theorem 4.4. □

While a configuration valuation with independence gives rise to a continuous valuation, not every continuous valuation arises in this way. As an example, consider the event structure E_{1} as defined in Section 2.3. Define

• ν(↑{a}) = ν(↑{b}) = ν(↑{c}) = ν(↑{d}) = 1/2;

• ν(↑{a, d}) = ν(↑{b, c}) = 1/2;

• ν(↑{a, c}) = ν(↑{b, d}) = 0;

and extend it to all open sets by modularity. It is easy to verify that it is indeed a continuous valuation on L(E_{1}). Define a function v : L_{fin}(E_{1}) → [0, 1] by v(x) := ν(↑ x). This is not a configuration valuation with independence; it does not satisfy condition (c) of Proposition 2.8. If we consider the compatible configurations x := {a}, y := {c} then v(x ∪ y) · v(x ∩ y) = 0 < 1/4 = v(x) · v(y).

Also continuous valuations “leaking” probability do not arise from probabilistic event structures with independence.

Definition 4.2. Denote the set of maximal elements of a DCPO D by Ω(D). A normalised continuous valuation ν on D is non-leaking if for every open set O ⊇ Ω(D), we have ν(O) = 1.

This definition is new, although inspired by a similar concept in [Eda95]. For the simplest example of a leaking continuous valuation, consider the event structure E_{2} consisting of one event e only, and the valuation defined as ν(∅) = 0, ν(↑ ⊥) = 1, ν(↑{e}) = 1/2. The corresponding function v : L_{fin}(E_{2}) → [0, 1] violates condition (b) of Proposition 2.8. The probabilities in the cell of e do not sum up to 1.

We analyse how valuations without independence and leaking valuations can arise in the next two sections.

4.3 Valuations Without Independence

Definition 2.12 of probabilistic event structures assumes the probabilistic independence of choice at different cells. This is reflected by condition (c) in Proposition 2.8 on which it depends. In the first example above, the probabilistic choices in the two cells are not independent: once we know the outcome of one of them, we also know the outcome of the other. This observation leads us to a more general definition of a configuration valuation and probabilistic event structure.

Definition 4.3. A configuration valuation on a confusion-free event structure E is a function v : L_{fin}(E) → [0, 1] such that:

(a) v(⊥) = 1;

(b) if C is a covering at x, then v[C] = v(x).

A probabilistic event structure consists of a confusion-free event structure together with a configuration valuation.

Now we can generalise Proposition 4.1, and provide a converse:

Theorem 4.4. For every configuration valuation v on E there is a unique normalised continuous valuation ν on L(E) such that for every finite configuration x, ν(↑ x) = v(x). Moreover ν is non-leaking.

Proof. See Appendix C. □

Theorem 4.5. Let ν be a non-leaking continuous valuation on L(E). The function v : L_{fin}(E) → [0, 1] defined by v(x) = ν(↑ x) is a configuration valuation.

Proof. See Appendix C. □

Using this representation result, we are also able to characterise the maximal elements in V^{1}(L(E)) as precisely the non-leaking valuations—a fact which is not known for general domains.

Theorem 4.6. Let E be a confusion-free event structure and let ν ∈ V^{1}(L(E)). Then ν is non-leaking if and only if it is maximal.

Proof. See [Var03], Prop. 7.6.3 and Thm. 7.6.4. □

4.4 Leaking Valuations

There remain leaking continuous valuations, as yet unrepresented by any probabilistic event structures. At first sight it might seem that to account for leaking valuations it would be enough to relax condition (b) of Definition 4.3 to the following

(b’) if C is a covering at x, then v[C] ≤ v(x).

However, it turns out that this is not the right generalisation, as the following example shows. Consider the event structure E_{3} where E_{3} = {a, b} with the flat causal ordering and no conflict. Define a “leaking configuration valuation” on E_{3} by v(⊥) = v({a}) = v({b}) = 1, v({a, b}) = 0. The function v satisfies conditions (a) and (b’), but it cannot be extended to a continuous valuation on the domain of configurations. However, we can show that the leaking of probability is attributable to an “invisible” event.

Definition 4.7. Consider a confusion-free event structure E = ⟨E, ≤, #⟩. For every cell c we consider a new “invisible” event ∂_{c} such that ∂_{c} ∉ E and if c ≠ c′ then ∂_{c} ≠ ∂_{c′}. Let ∂ = {∂_{c} | c is a cell}. We define E_{∂} to be ⟨E_{∂}, ≤_{∂}, #_{∂}⟩, where

• E_{∂} = E ∪ ∂;

• ≤_{∂} is ≤ extended by e ≤_{∂} ∂_{c} if for all e′ ∈ c, e ≤ e′;

• #_{∂} is # extended by e #_{∂} ∂_{c} if there exists e′ ∈ c, e′ ≤ e.

So E_{∂} is E extended by an extra invisible event at every cell. Invisible events can absorb all leaking probability, as shown by Theorem 4.9 below.

Definition 4.8. Let E be a confusion-free event structure. A generalised configuration valuation on E is a function v : L_{fin}(E) → [0, 1] that can be extended to a configuration valuation on E_{∂}.

It is not difficult to prove that, when such an extension exists, it is unique.

Theorem 4.9. Let E be a confusion-free event structure. Let v : L_{fin}(E) → [0, 1]. There exists a unique normalised continuous valuation ν on L(E) with v(x) = ν(↑ x), if and only if v is a generalised configuration valuation.

Proof. See [Var03], Thm. 6.5.3. □

The above theorem completely characterises the normalised continuous valuations on distributive concrete domains in terms of probabilistic event structures.

5 Probabilistic Event Structures as Probabilistic Runs

In the rest of the paper we investigate how to adjoin probabilities to event structures which are not confusion-free. In order to do so, we find it useful to introduce two notions of probabilistic run.

Configurations represent runs (or computation paths) of an event structure. What is a probabilistic run (or probabilistic computation path) of an event structure? One would expect a probabilistic run to be a form of probabilistic configuration, so a probability distribution over a suitably chosen subset of configurations. As a guideline we consider the traditional model of probabilistic automata [Seg95], where probabilistic runs are represented in essentially two ways: as a probability measure over the set of maximal runs [Seg95], and as a probability distribution over finite runs of the same length [dAHJ01].

The first approach is readily available to us, and where we begin. As we will see, according to this view probabilistic event structures over an underlying event structure E correspond precisely to the probabilistic runs of E.

The proofs of the results in this section are to be found in the appendix.

5.1 Probabilistic Runs of an Event Structure

The first approach suggests that a probabilistic run of an event structure E be taken to be a probability measure on the maximal configurations of L(E).

Some basic notion of measure theory can be found in Appendix A. Let D be an algebraic domain. Recall that Ω(D) denotes the set of maximal elements of D and that for every compact element x ∈ D the principal set ↑ x is Scott open. The set K(x) := ↑ x ∩ Ω(D) is called the shadow of x. We shall consider the σ-algebra S on Ω(D) generated by the shadows of the compact elements.

Definition 5.1. A probabilistic run of an event structure E is a probability measure on ⟨Ω(L(E)), S⟩, where S is the σ-algebra generated by the shadows of the compact elements.

There is a tight correspondence between non-leaking valuations and probabilistic runs.

Theorem 5.2. Let ν be a non-leaking normalised continuous valuation on a coherent ω-algebraic domain D. Then there is a unique probability measure μ on S such that for every compact element x, μ(K(x)) = ν(↑ x). Let μ be a probability measure on S. Then the function ν defined on open sets by ν(O) = μ(O ∩ Ω(D)) is a non-leaking normalised continuous valuation.

Proof. See Appendix C. □

According to the result above, probabilistic event structures over a common event structure E correspond precisely to the probabilistic runs of E. Among these we can characterise probabilistic event structures with independence in terms of the standard measure-theoretic notion of independence. In fact, for such a probabilistic event structure, every two compatible configurations are probabilistically independent, given the common past:

Proposition 5.3. Let v be a configuration valuation on a confusion-free event structure E. Let μ_{v} be the corresponding measure as of Propositions 4.1 and Theorem 5.2. Then, v is a configuration valuation with independence iff for every two finite compatible configurations x, y

μ_{v}(K(x) ∩ K(y) | K(x ∩ y)) = μ_{v}(K(x) | K(x ∩ y)) · μ_{v}(K(y) | K(x ∩ y)) .

Proof. See Appendix C. □

Note that the definition of probabilistic run of an event structure does not require that the event structure is confusion-free. It thus suggests a general definition of a probabilistic event structure as an event structure with a probability measure μ on its maximal configurations, even when the event structure is not confusion-free. This definition, in itself, is however not very informative and we look to an explanation in terms of finite probabilistic runs.

5.2 Finite Runs

What is a finite probabilistic run? Following the analogy heading this section, we want it to be a probability distribution over finite configurations. But which sets are suitable to be the support of such distribution? In interleaving models, the sets of runs of the same length do the job. For event structures this won’t do.

To see why consider the event structure with only two concurrent events a, b. The only maximal run assigns probability 1 to the maximal configuration {a, b}. This corresponds to a configuration valuation which assigns 1 to both {a} and {b}. Now these are two configurations of the same size, but their common “probability” is equal to 2! The reason is that the two configurations are compatible: they do not represent alternative choices. We therefore need to represent alternative choices, and we need to represent them all. This leads us to the following definition.

Definition 5.4. Let E be an event structure. A partial test of E is a set C of pairwise incompatible configurations of E. A test is a maximal partial test. A test is finitary if all its elements are finite.

Maximality of a partial test C can be characterised equivalently as completeness: for every maximal configuration z, there exists x ∈ C such that x ⊆ z. The set of tests, endowed with the Egli-Milner order has an interesting structure: the set of all tests is a complete lattice, while finitary tests form a lattice.

Tests were designed to support probability distributions. So given a sensible valuation on finite configurations we expect it to restrict to probability distributions on tests.

Definition 5.5. Let v be a function L_{fin}(E) → [0, 1]. Then v is called a test valuation if for all finitary tests C we have v[C] = 1.

Theorem 5.6. Let μ be a probabilistic run of E. Define v : L_{fin}(E) → [0, 1] by v(x) = μ(K(x)). Then v is a test valuation.

Proof. See Appendix C. □

Note that Theorem 5.6 is for general event structures. We unfortunately do not have a converse in general. However, there is a converse when the event structure is confusion-free:

Theorem 5.7. Let E be a confusion-free event structure. Let v be a function L_{fin}(E) → [0, 1]. Then v is a configuration valuation if and only if it is a test valuation.

Proof. See Appendix C. □

The proof of this theorem hinges on a property of tests. The property is that of whether partial tests can be completed. Clearly every partial test can be completed to a test (by Zorn’s lemma), but there exist finitary partial tests that cannot be completed to finitary tests.

Definition 5.8. A finitary partial test is honest if it is part of a finitary test. A finite configuration is honest if it is honest as partial test.

Proposition 5.9. If E is a confusion-free event structure and if x is a finite configuration of E, then x is honest in L(E).

Proof. See Appendix C. □

So confusion-free event structures behave well with respect to honesty. For general event structures, the following is the best we can do at present:

Theorem 5.10. Let v be a test valuation on E. Let H be the σ-algebra on Ω(L(E)) generated by the shadows of honest finite configurations. Then there exists a unique measure μ on H such that μ(K(x)) = v(x) for every honest finite configuration x.

Proof. See Appendix C. □

Theorem 5.11. If all finite configurations are honest, then for every test valuation v there exists a unique continuous valuation ν, such that ν(↑ x) = v(x).

Proof. See Appendix C. □

But, we do not know whether in all event structures, every finite configuration is honest. We conjecture this to be the case. If so this would entail the general converse to Theorem 5.6 and so characterise probabilistic event structures, allowing confusion, in terms of finitary tests.

6 Morphisms

It is relatively straightforward to understand event structures with independence. But how can general test valuations on a confusion-free event structures arise? More generally how do we get runs of arbitrary event structures? We explore one answer in this section. We show how to obtain test valuations as “projections” along a morphism from a configuration valuation with independence on a confusion-free event structure. The use of morphisms shows how general valuations are obtained through the hiding and renaming of events.

6.1 Definitions

Definition 6.1 ([Win82,WN95]). Given two event structures E, E′, a morphism f : E → E′ is a partial function f : E → E′ such that

• whenever x ∈ L(E) then f(x) ∈ L(E′);

• for every x ∈ L(E), for all e_{1}, e_{2} ∈ x if f(e_{1}), f(e_{2}) are both defined and f(e_{1}) = f(e_{2}), then e_{1} = e_{2}.

Such morphisms define a category ES. The operator L extends to a functor ES → DCPO by L(f)(x) = f(x), where DCPO is the category of DCPO’s and continuous functions.

A morphism f : E → E′ expresses how the occurrence of an event in E induces a synchronised occurrence of an event in E′. Some events in E are hidden (if f is not defined on them) and conflicting events in E may synchronise with the same event in E′ (if they are identified by f).

The second condition in the definition guarantees that morphisms of event structures “reflect” reflexive conflict, in the following sense. Let ⋆ be the relation (# ∪ Id_{E}), and let f : E → E′. If f(e_{1}) ⋆ f(e_{2}), then e_{1} ⋆ e_{2}. We now introduce morphisms that reflect tests; such morphisms enable us to define a test valuation on E′ from a test valuation on E. To do so we need some preliminary definitions. Given a morphism f : E → E′, we say that an event of E is f-invisible, if it is not in the domain of f. Given a configuration x of E we say that it is f-minimal if all its maximal events are f-visible. That is x is f-minimal, when is minimal in the set of configurations that are mapped to f(x). For any configuration x, define x_{f} to be the f-minimal configuration such that x_{f} ⊆ x and f(x) = f(x_{f}).

Definition 6.2. A morphism of event structures f : E → E′ is tight when

• if y = f(x) and if y′ ⊇ y, there exists x′ ⊇ x_{f} such that y′ = f(x′);

• if y = f(x) and if y′ ⊆ y, there exists x′ ⊆ x_{f} such that y′ = f(x′);

• all maximal configurations are f-minimal (no maximal event is f-invisible).

Tight morphisms have the following interesting properties:

Proposition 6.3. A tight morphism of event structures is surjective on configurations. Given f : E → E′ tight, if C′ is a finitary test of E′ then the set of f-minimal inverse images of C′ along f is a finitary test in E.

Proof. The f-minimal inverse images form always a partial test because morphisms reflect conflict. Tightness is needed to show completeness. □

We now study the relation between valuations and morphisms. Given a function v : L_{fin}(E) → [0, +∞] and a morphism f : E → E′ we define a function f(v) : L_{fin}(E′) → [0, +∞] by f(v)(y) = ∑{v(x) | f(x) = y and x is f-minimal}. We have:

Proposition 6.4. Let E, E′ be confusion-free event structures, v a generalised configuration valuation on E and f : E → E′ a morphism. Then f(v) is a generalised configuration valuation on E′.

See [Var03] for the proof. More straightforwardly:

Proposition 6.5. Let E, E′ be event structures, v be a test valuation on E, and f : E → E′ a tight morphism. Then the function f(v) is a test valuation on E′.

Therefore we can obtain a run of a general event structure by projecting a run of a probabilistic event structure with independence. Presently we don’t know whether every run can be generated in this way.

6.2 Morphisms at work

The use of morphisms allows us to make interesting observations. Firstly we can give an interpretation to probabilistic correlation. Consider the following event structures E_{1} = ⟨E_{1}, ≤, #⟩, E_{4} = ⟨E_{4}, ≤, #⟩ where E_{4} is defined as follows:

• E_{4} = {a_{1}, a_{2}, b_{1}, b_{2}, c_{1}, c_{2}, d_{1}, d_{2}, e_{1}, e_{2}};

• e_{1} ≤ a_{1}, b_{1}, c_{1}, d_{1}, e_{2} ≤ a_{2}, b_{2}, c_{2}, d_{2};

• e_{1} #_{μ} e_{2}, a_{i} #_{μ} b_{i}, c_{i} #_{μ} d_{i} for i = 1, 2.

[figure: a_{1}; b_{1}; c_{1}; d_{1}; a_{2}; b_{2}; c_{2}; d_{2}; e_{1}; e_{2}]

Above, curly lines represent immediate conflict, while the causal order proceeds upwards along the straight lines. The event structure E_{1} was defined in Section 2.3: E_{1} = {a, b, c, d} with the discrete ordering and with a #_{μ} b and c #_{μ} d.

[figure: a; b; c; d]

The map f : E_{4} → E_{1} defined as f(x_{i}) = x, x = a, b, c, d, i = 1, 2 is a tight morphism of event structures.

Now suppose we have a global valuation with independence v on E_{4}. We can define it as cell valuation p, by p(e_{i}) = \frac{1}{2}, p(a_{1}) = p(c_{1}) = p(b_{2}) = p(d_{2}) = 1, p(a_{2}) = p(c_{2}) = p(b_{1}) = p(d_{1}) = 0. It is easy to see that v′ := f(v), is the test valuation defined in Section 4.2. For instance

v′(\{a\}) = v(\{e_{1}, a_{1}\}) + v(\{e_{2}, a_{2}\}) = \frac{1}{2} ;

v′({a, d}) = v({e_{1}, a_{1}, d_{1}}) + v({e_{2}, a_{2}, d_{2}}) = 0 .

Therefore v′ is not a global valuation with independence: the correlation between the cell {a, b} and the cell {c, d} can be interpreted by saying that it is due to a hidden choice between e_{1} and e_{2}.

In the next example a tight morphism takes us out of the class of confusion free event structures. Consider the event structures E_{5} = ⟨E_{5}, ≤, #⟩, E_{6} = ⟨E_{6}, ≤, #⟩ where E_{5} = {a_{1}, a_{2}, b, c, d}; a_{1} ≤ b, a_{2} ≤ c, d; a_{1} #_{μ} a_{2};

[figure: b; c; d; a_{1}; a_{2}]

while E_{6} = {b, c, d}; b #_{μ} c, d.

[figure: c; b; d]

Note the E_{6} is not confusion free: it is in fact the simplest example of symmetric confusion [RE96]. The map f : E_{5} → E_{6} defined as f(x) = x, x = b, c, d is a tight morphism of event structures. A test valuation on an event structure with confusion is obtained as a projection along a tight morphism from a probabilistic event structure with independence. Again this is obtained by hiding a choice.

In the next example we again restrict attention to confusion free event structures, but we use a non-tight morphism. Such morphisms allow us to interpret conflict as probabilistic correlation. Consider the event structures E_{7} = ⟨E_{7}, ≤, #⟩, E_{3} = ⟨E_{3}, ≤ , #⟩ where

• E_{7} = {a, b}: a #_{μ} b;

• E_{3} = {a, b} with no conflict.

The map f : E_{7} → E_{3} defined as f(x) = x, x = a, b is a morphism of event structures. It is not tight, because it is not surjective on configurations: the configuration {a, b} is not in the image of f.

Consider the test valuation v on E_{7} defined as v({a}) = v({b}) = 1/2. The generalised global valuation v′ = f(v) is then defined as follows: v′({a}) = v′({b}) = 1/2, v′({a, b}) = 0. It is not a test valuation, but by Theorem 4.9, we can extend it to a test valuation on E_{7,∂}:

[figure: ∂_{a}; a; ∂_{b}; b]

The (unique) extension is defined as follows:

• v′({∂_{a}}) = v′({∂_{b}}) = v′({a}) = v′({b}) = 1/2;

• v′({∂_{a}, ∂_{b}}) = v′({a, b}) = 0;

• v′({∂_{a}, b}) = v′({a, ∂_{b}}) = 1/2.

The conflict between a and b in E_{7} is seen in E_{3} as a correlation between their cells. Either way, we cannot observe a and b together.

7 Related and Future Work

In his PhD thesis, Katoen [Kat96] defines a notion of probabilistic event structure which includes our probabilistic event structures with independence. But his concerns are more directly tuned to a specific process algebra. So in one sense his work is more general—his event structures also possess nondeterminism—while in another it is much more specific in that it does not look beyond local probability distributions at cells. Völzer [Voe01] introduces similar concepts based on Petri nets and a special case of Theorem 5.10. Benveniste et al. have an alternative definition of probabilistic Petri nets in [BFH03], and there is clearly an overlap of concerns though some significant differences which require study.

We have explored how to add probability to the independence model of event structures. In the confusion-free case, this can be done in several equivalent ways: as valuations on configurations; as continuous valuations on the domain of configurations; as probabilistic runs (probability measures over maximal configurations); and in the simplest case, with independence, as probability distributions existing locally and independently at cells. Work remains to be done on a more operational understanding, in particular on how to understand probability adjoined to event structures which are not confusion-free. This involves relating probabilistic event structures to interleaving models like Probabilistic Automata [Seg95] and Labelled Markov Processes [DEP02].

Acknowledgments

The first author wants to thank Mogens Nielsen, Philippe Darondeau, Samy Abbes and an anonymous referee.

References

[AJ94] Samson Abramsky and Achim Jung. Domain theory. In Handbook of Logic in Computer Science, volume 3. Clarendon Press, 1994.

[AM00] Mauricio Alvarez-Manilla. Measure Theoretic Results for Continuous Valuations on Partially Ordered Spaces. PhD thesis, University of London - Imperial College of Science, Technology and Medicine, September 2000.

[AES00] Mauricio Alvarez-Manilla, Abbas Edalat, and Nasser Saheb-Djaromi. An extension result for continuous valuations. Journal of the London Mathematical Society, 61(2):629–640, 2000.

[BFH03] Albert Benveniste, Eric Fabre, and Stefan Haar. Markov nets: Probabilistic models for distributed and concurrent systems. IEEE Transactions on Automatic Control, 48(11):1936–1950, 2003.

[dAHJ01] Luca de Alfaro, Thomas A. Henzinger, and Ranjit Jhala. Compositional methods for probabilistic systems. In Proc. 12th CONCUR, volume 2154 of LNCS, pages 351–365, 2001.

[DEP02] Josée Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for labelled markov processes. Information and Computation, 179(2):163–193, 2002.

[Eda95] Abbas Edalat. Domain theory and integration. Theoretical Computer Science, 151(1):163–193, 1995.

[Hal50] Paul Halmos. Measure Theory. van Nostrand, 1950. New edition by Springer in 1974.

[JP89] Claire Jones and Gordon D. Plotkin. A probabilistic powerdomain of evaluations. In Proceedings of 4th LICS, pages 186–195, 1989.

[Kat96] Joost-Pieter Katoen. Quantitative and Qualitative Extensions of Event Structures. PhD thesis, University of Twente, 1996.

[KP93] Gilles Kahn and Gordon D. Plotkin. Concrete domains. Theoretical Computer Science, 121(1-2):187–277, 1993.

[Law97] Jimmie D. Lawson. Spaces of maximal points. Mathematical Structures in Computer Science, 7(5):543–555, 1997.

[LS91] Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1–28, 1991.

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

[NPW81] Mogens Nielsen, Gordon D. Plotkin, and Glynn Winskel. Petri nets, event structures and domains, part I. Theoretical Computer Science, 13(1):85–108, 1981.

[RE96] Grzegorz Rozenberg and Joost Engelfriet. Elementary net systems. In Dagstuhl Lecturs on Petri Nets, volume 1491 of LNCS, pages 12–121. Springer, 1996.

[Seg95] Roberto Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, M.I.T., 1995.

[Voe01] Hagen Völzer. Randomized non-sequential processes. In Proceedings of 12th CON-CUR, volume 2154 of LNCS, pages 184–201, 2001. Extended version as Technical Report 02-28 - SVRC - University of Queensland, 2002.

[Var03] Daniele Varacca. Probability, nondeterminism and Concurrency. Two denotational models for probabilistic computation. PhD thesis, BRICS - Aarhus University, 2003. Available at http://www.brics.dk/∼varacca.

[Win82] Glynn Winskel. Event structure semantics for CCS and related languages. In Proceedings of 9th ICALP, volume 140 of LNCS, pages 561–576. Springer, 1982.

[Win87] Glynn Winskel. Event structures. In Advances in Petri Nets 1986, Part II; Proceedings of an Advanced Course, Bad Honnef, September 1986, volume 255 of LNCS, pages 325–392. Springer, 1987.

[WN95] Glynn Winskel and Mogens Nielsen. Models for concurrency. In Handbook of logic in Computer Science, volume 4. Clarendon Press, 1995.

A Domain Theory and Measure Theory—Basic Notions

A.1 Domain Theory

We briefly recall some basic notions of domain theory (see e.g. [AJ94]). A directed complete partial order (DCPO) is a partial order where every directed set Y has a least upper bound ⨆ Y. An element x of a DCPO D is compact (or finite) if for every directed Y and every x ≤ ⨆ Y there exists y ∈ Y such that x ≤ y. The set of compact elements is denoted by Cp(D). A DCPO is an algebraic domain if or every x ∈ D, x is the directed least upper bound of ↓ x ∩ Cp(D). It is ω-algebraic if Cp(D) is countable.

In a partial order, two elements are said to be compatible if they have a common upper bound. A subset of a partial order is consistent if every two of its elements are compatible. A partial order is coherent if every consistent set has a least upper bound.

The Egli-Milner order on subsets of a partial order is defined by X ≤ Y if for all x ∈ X there exists y ∈ Y, x ≤ y and for all y ∈ Y there exists x ∈ X, x ≤ y. A subset X of a DCPO is Scott open if it is upward closed and if for every directed set Y whose least upper bound is in X, then Y ∩ X ≠ ∅. Scott open sets form the Scott topology.

A.2 Measure Theory

A σ-algebra on a set Ω is a family of subsets of X which is closed under countable union and complementation and which contains ∅. The intersection of an arbitrary family of σ-algebras is again a σ-algebra. In particular if S ⊆ P(Ω), and Ξ := {F | F is a σ-algebra & S ⊆ F}, then ⋂ Ξ is again a σ-algebra and it belongs to Ξ. We call ⋂ Ξ the smallest σ-algebra containing S.

If S is a topology, the smallest σ-algebra containing S is called the Borel σ-algebra of the topology. Note that although a topology is closed under arbitrary union, its Borel σ-algebra need not be.

A measure space is a triple (Ω, F, ν) where F is a σ-algebra on Ω and ν is a measure on F that is a function ν : F → [0, +∞] satisfying:

• (Strictness) ν(∅) = 0;

• (Countable additivity) if (A_{n})_{n∈ℕ} is a countable family of pairwise disjoint sets of F, then ν(⋃_{n∈ℕ} A_{n}) = ∑_{n∈ℕ} ν(A_{n}) .

Finite additivity follows by putting A_{n} = ∅ for all but finitely many n.

Among the various results of measure theory we state two that we will need later.

Theorem A.1 ([Hal50] Theorem 9.E). Let ν be a measure on a σ-algebra F, and let A_{n} be a decreasing sequence of sets in F, that is A_{n+1} ⊆ A_{n}, such that ν(A_{0}) < ∞. Then

ν ( ⋂_{n∈ℕ} A_{n}) = lim_{n→∞} ν(A_{n}) .

One may ask when it is possible to extend a valuation on a topology to a measure on the Borel σ-algebra. This problem is discussed in Mauricio Alvarez-Manilla’s thesis [AM00]. The result we need is the following. It can also be found in [AES00], as Corollary 4.3.

Theorem A.2. Any normalised continuous valuation on a continuous DCPO extends uniquely to a measure on the Borel σ-algebra.

B Proofs from Section 2

Proposition 2.6. In a confusion-free event structure if C is a covering at x, then c = {e | x ∪ {e} ∈ C} is a cell accessible at x. Conversely, if c is accessible at x, then C := {x ∪ {e} | e ∈ c} is a covering at x.

Proof. Let C be a covering at x, and let c be defined as above. Then for every distinct e, e′ ∈ c, we have e # e′, otherwise x∪{e} and x∪{e′} would be compatible. Moreover as [e), [e′) ⊆ x, we have that [e] ∪ [e′) ⊆ x ∪ {e} so that [e] ∪ [e′) is a configuration. Analogously [e) ∪ [e′] is a configuration so that e #_{μ} e′. Now take e ∈ c and suppose there is e′ ∉ c such that e #_{μ} e′. Since #_{μ} is transitive, then for every e′′ ∈ c, e′ #_{μ} e′′. Therefore x ∪ {e′} is incompatible with every configuration in C, and x ◁ x ∪ {e′}. Contradiction.

Conversely, take a cell c ∈ Acc(x), and define C as above. Then clearly for every x′ ∈ C, x ◁ x′ and also for every x′, x′′ ∈ C, x′, x′′ are incompatible. Now consider a configuration y, such that x ◁ y. This means y = x ∪ {e} for some e. If e ∈ c then y ∈ C and y is compatible with itself. If e ∉ c then for every e′ ∈ c, e, e′ are not in immediate conflict. Suppose e # e′, then, by lemma 2.1 there are d ≤ e, d′ ≤ e′ such that d #_{μ} d′. Suppose d < e then [e) ∪ [e′] would not be a conflict free. But that is not possible as [e) ∪ [e′] ⊆ x ∪ {e′} and the latter is a configuration. Analogously it is not the case that d′ < e′. This implies that e #_{μ} e′, a contradiction. Therefore for every x ∈ C, y and x are compatible. □

Proposition 2.11. If v is a configuration valuation with independence and p : E → [0, 1] is a mapping such that v([e]) = p(e) · v([e)) for all e ∈ E, then p is a cell valuation such that v_{p} = v.

Proof. Consider now a cell c. Then the set C := {[c) ∪ {e} | e ∈ c} is a covering at [c). Remember that if e ∈ c, then [e) = [c). Therefore if v([e)) ≠ 0 we have

∑_{e∈c} p(e) = ∑_{e∈c} v([e])/v([e))

= ∑_{e∈c} v([e])/v([c)) = ∑_{x∈C} v(x)/v([c)) = 1 .

We discuss later the case v([e)) = 0. In order to show that v_{p} = v we proceed by induction on the size of the configurations. Because of normality, we have that

v_{p_{v}}(∅) = ∏_{e∈∅} p_{v}(e) = 1 = v(∅) .

Now assume that for every configuration y of size n, v_{p}(y) = v(y), take a configuration x of size n + 1. Take a maximal event e ∈ x so that y := x \ {e} is still a configuration. Since x is a configuration, it must be that [e] ⊆ x and thus [e) ⊆ y. Therefore [e) = y ∩ [e]. First suppose v([e)) ≠ 0

v_{p}(x) = ∏_{e′∈x} p(e′) = p(e) · ∏_{e′∈y} p(e′)

= p(e) · v_{p}(y)

By induction hypothesis this is equal to

= p(e) · v(y) = (v([e])/v([e))) · v(y)
= v([e]) · v(y)/v([e)) = v([e]) · v(y)/v(y ∩ [e])

And because of independence this is equal to

= v(y ∪ [e]) = v(x) .

If v([e)) = 0, by contravariance we have v(x) = v(y) = 0

v_{p}(x) = ∏_{e′∈x} p(e′) = p(e) · ∏_{e′∈y} p(e′)

= p(e) · v_{p}(y)

By induction hypothesis this is equal to

= p(e) · v(y) = 0 = v(x) .

Note that when v([e)) = 0 it does not matter what values p assumes on the events in c. Thus we can assume that p[c] = 1. □

C Proofs of the Main Results

We provide here the proofs of Sections 4 and 5. The order in which these proofs are presented does not follow the order in which they are introduced in the main body of the paper.

C.1 Configuration and Continuous Valuations

Theorem 4.4. For every configuration valuation v on E there is a unique normalised continuous valuation ν on L(E) such that for every finite configuration x, ν(↑ x) = v(x). Moreover ν is non-leaking.

The proof of Theorem 4.4 will require various intermediate results. In the following proofs we will write x̂ for ↑ x. We will use lattice notation for configurations. That is, we will write x ≤ y for x ⊆ y, x ∨ y for x ∪ y, and ⊥ for the empty configuration. To avoid complex case distinctions we also introduce a special element ⊤ representing an impossible configuration. If x, y are incompatible, the expression x ∨ y will denote ⊤. Also, for every configuration valuation v, v(⊤) = 0, finally ˆ⊤ = ∅. The finite configurations together with ⊤ form a ∨-semilattice.

We have to define a function from the Scott open sets of L(E) to the unit interval. This value of ν on the principal open sets is determined by ν(x̂) = v(x). We first define ν on finite unions of principal open sets. Since L(E) is algebraic, such sets form a basis of the Scott topology of L(E). We will then be able to define ν on all open sets by continuity.

Let P n be the set of principal open subsets of L(E). That is

P n = {x̂ | x ∈ L_{fin}(E)} ∪ {∅} .

Notice that P n is closed under finite intersection because x̂ ∩ ŷ = { \atop x ∨ y}. (If x, y are not compatible then x̂ ∩ ŷ = ∅ = ˆ⊤ = { \atop x ∨ y}.) The family P n is, in general, not closed under finite union.

Let Bs be the set of finite unions of elements of P n. That is

Bs = {x̂_{1} ∪ … ∪ x̂_{n} | x̂_{i} ∈ P n, 1 ≤ i ≤ n} .

Using distributivity of intersection over union it is easy to prove the following. Lemma C.1. The structure ⟨Bs, ∪, ∩⟩ is a distributive lattice with top and bottom. Since the ν has to be modular, it will also satisfy the inclusion-exclusion principle. We exploit this to define ν. Let us define ν_{0} : Bs → ℝ as follows

ν_{0} (x̂_{1} ∪ … ∪ x̂_{n}) = ∑_{∅≠I⊆I_{n}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i}) .

We have first to make sure that ν_{0} is well defined: If two expressions x̂_{1} ∪ … ∪ x̂_{n} and ŷ_{1} ∪ … ∪ ŷ_{m} represent the same set, then

∑_{∅≠I⊆I_{n}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i}) = ∑_{∅≠J⊆I_{m}}(−1)^{|J|−1}v ( ⋁_{j∈J} y_{j}) .

Lemma C.2. We have x̂ ⊆ x̂_{1} ∪ … ∪ x̂_{n} if and only if there exists i such that x_{i} ≤ x.

Proof. Straightforward. □ Lemma C.3. If x_{n} ≤ x_{n+1} then

∑_{∅≠I⊆I_{n}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i}) = ∑_{∅≠I⊆I_{n+1}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i}) .

Proof. When x_{n} ≤ x_{n+1} we have that x_{n} ∨ x_{n+1} = x_{n+1}. Now

∑_{∅≠I⊆I_{n+1}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i})

= ∑_{∅≠I⊆I_{n}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i})

+ ∑_{{I⊆I_{n+1} \atop n,n+1∈I}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i})

+ ∑_{{I⊆I_{n+1} \atop n∉I,n+1∈I}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i}) .

We claim that

∑_{{I⊆I_{n+1} \atop n,n+1∈I}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i}) + ∑_{{I⊆I_{n+1} \atop n∉I,n+1∈I}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i}) = 0

and this would prove our lemma. To prove the claim

∑_{{I⊆I_{n+1} \atop n,n+1∈I}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i})

= ∑_{I⊆I_{n−1}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i} ∨ x_{n} ∨ x_{n+1})

= ∑_{I⊆I_{n−1}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i} ∨ x_{n+1})

= − ∑_{I⊆I_{n−1}}(−1)^{|I|}v (⋁_{i∈I} x_{i} ∨ x_{n+1})

= − ∑_{{I⊆I_{n+1} \atop n∉I,n+1∈I}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i})

□

Therefore we can safely remove “redundant” components from a finite union until we are left with a minimal expression. The next lemma says that such minimal expression is unique, up to the order of the components.

Lemma C.4. Let x̂_{1} ∪ … ∪ x̂_{n} = ŷ_{1} ∪ … ∪ ŷ_{m}, and let such expressions be minimal. Then n = m and there exists a permutation σ of I_{n} such that x_{i} = y_{σ(i)}.

Proof. By lemma C.2, for every i ∈ I_{n} there exist some j ∈ I_{m} such that y_{j} ≤ x_{i}. Let σ : I_{n} → I_{m} be a function choosing one such j. Symmetrically let τ : I_{m} → I_{n} be such that x_{τ(j)} ≤ y_{j}. Now I claim that for every i, τ(σ(i)) = i. In fact x_{τ(σ(i))} ≤ y_{σ(i)} ≤ x_{i}. The minimality of the x_{i}’s implies the claim. Symmetrically σ(τ(j)) = j, so that σ is indeed a bijection. □

Finally we observe that in the definition of ν_{0}, the order of the x_{i} does not matter. This concludes the proof of that ν_{0} is well-defined.

Next we state a lemma saying that ν_{0} : Bs → ℝ is a valuation on the lattice ⟨Bs, ∪, ∩⟩. This is the crux of the proof of Theorem 4.4.

Lemma C.5. The function ν_{0} : Bs → ℝ satisfies the following properties:

• (Strictness) ν_{0}(∅) = 0;

• (Monotonicity) U ⊆ V ⟹ ν_{0}(U) ≤ ν_{0}(V);

• (Modularity) ν_{0}(U) + ν_{0}(V) = ν_{0}(U ∪ V) + ν_{0}(U ∩ V).

In particular, since ˆ⊥ = L(E), for every U ∈ Bs, we have 0 = ν_{0}(∅) ≤ ν_{0}(U) ≤ ν_{0}(L(E)) = ν_{0}(ˆ⊥) = v(⊥) = 1. So in fact ν_{0} : Bs → [0, 1].

Proof. Strictness is obvious.

We prove monotonicity in steps. First we prove a special case, that is for every ntuple of finite configurations (x_{i}) and for every finite configuration y, if x̂_{1} ∪…∪x̂_{n} ⊆ ŷ, then ν_{0} (x̂_{1} ∪ … ∪ x̂_{n}) ≤ ν_{0}(ŷ). We will do it by induction on n.

The basis requires that 0 = ν_{0}(∅) ≤ ν_{0}(ŷ) = v(y) which is true. Suppose now that x̂_{1}∪…∪{ \atop x_{n+1}} ⊆ ŷ. Fix y and consider all n+1-tuples (z_{i}) such that ẑ_{1}∪…∪{ \atop z_{n+1}} ⊆ ŷ and order them componentwise. That is (z_{i}) ≤ (z′_{i}) if for every i, z_{i} ≤ z′_{i}. Note that if (z_{i}) > (z′_{i}) then some of the (z′_{i}) must be strictly smaller than some of the z_{i}. As every z_{i} is finite this order is well founded. Suppose by contradiction that there exist an n + 1-tuples for which

ν_{0} (ẑ_{1} ∪ … ∪ { \atop z_{n+1}}) > ν_{0}(ŷ)

and take a minimal such. If this is the case, then all z_{i} must be strictly greater than y. We argue that there is a cell c, such that y does not fill c, some of the z_{i}’s fill c and for all z_{i} that do, the event e ∈ c ∩ z_{i} is maximal in z_{i}. Consider a maximal event e_{1} ∈ z_{1} \ y. If the cell c_{1} of e_{1} is maximal in all z_{j} that fill c_{1}, then we are done. Otherwise consider the first z_{j} that fills c_{1} but for which c_{1} is not maximal. Consider a maximal event in z_{j} lying above c_{1}. Consider its cell c_{2}. Since c_{2} is above c_{1}, clearly c_{2} cannot be filled by any of the z_{i} for i < j because, either they do not fill c_{1}, or if they do, then c_{1} is maximal. Continue this process until you reach z_{n+1} at which point we will have found a cell c with the properties above.

Consider all the events e_{1}, …, e_{h}, … ∈ c.^{1} For every h ≥ 1 let I^{h} = {i ∈ I_{n+1} | e_{h} ∈ z_{i}}. Since c is maximal and it is not filled by y, then we have that for every i ∈ I^{h}, z′_{i} := z_{i} \ {e_{h}} is still a configuration and it is still above y. For every i ∈ I_{n+1} let w_{i} be z′_{i} if i belongs to some I^{h}, and otherwise let w_{i} be z_{i}. For what we have said, all w_{i} are greater than y so that ŵ_{1} ∪ … ∪ { \atop w_{n+1}} ⊆ ŷ. Also the tuple (w_{i}) is strictly below (z_{i}) in the well order defined above. We now show that

ν_{0} (ŵ_{1} ∪ … ∪ { \atop w_{n+1}}) > ν_{0}(ŷ)

which contradicts minimality. To do that we show that

ν_{0} (ŵ_{1} ∪ … ∪ { \atop w_{n+1}}) ≥ ν_{0} (ẑ_{1} ∪ … ∪ { \atop z_{n+1}}) .

That is

∑_{∅≠I⊆I_{n+1}}(−1)^{|I|−1}v (⋁_{i∈I} w_{i}) ≥ ∑_{∅≠I⊆I_{n+1}}(−1)^{|I|−1}v (⋁_{i∈I} z_{i}) .

We can start erasing summands that do not change. Let Ĩ = I_{n+1} \ ⋃_{h≥1} I^{h} For every i ∈ Ĩ, w_{i} = z_{i}, thus if I ⊆ Ĩ then ⋁_{i∈I} w_{i} = ⋁_{i∈I} z_{i}. So that

v (⋁_{i∈I} w_{i}) = v (⋁_{i∈I} z_{i}) .

1 Cells can be finite or countable. We do the proof for the countable case, the finite case being analogous and, in fact, simpler.

Removing the summands of the above shape, it is enough to prove that

∑_{{∅≠I⊆I_{n+1} \atop I\Ĩ≠∅}}(−1)^{|I|−1}v (⋁_{i∈I} w_{i}) ≥ ∑_{{∅≠I⊆I_{n+1} \atop I\Ĩ≠∅}}(−1)^{|I|−1}v (⋁_{i∈I} z_{i}) .

Also note that if for two different h, h′ ≥ 1 we have that, if I ∩ I^{h} ≠ ∅ and I ∩ I^{h′} ≠ ∅ then ⋁_{i∈I} z_{i} = ⊤, that is v (⋁_{i∈I} z_{i}) = 0, because it is the join of incompatible configurations. Therefore we can rewrite the right-hand member of the inequation above as

∑_{h≥1} ∑_{∅≠I\Ĩ⊆I^{h}}(−1)^{|I|−1}v (⋁_{i∈I} z_{i}) .

For every i ∉ Ĩwe can define z_{i}^{h} to be w_{i} ∪{e_{h}}. All such z_{i}^{h} are indeed configurations because if i ∉ Ĩ then c is accessible at w_{i}. For every I such that ∅ ≠ I \ Ĩ we have that ⋁_{i∈I} z_{i}^{h} = ⊤ if and only if ⋁_{i∈I} w_{i} = ⊤ as e_{h} is the only event in its cell appearing in any configuration, so its introduction cannot cause an incompatibility that was not already there. Now condition b) in the definition of configuration valuation says exactly that

v (⋁_{i∈I} w_{i}) = ∑_{h≥1} v (⋁_{i∈I} z_{i}^{h}) .

(Where both members may be 0 if ⋁_{i∈I} w_{i} is already ⊤.) Therefore

∑_{I\Ĩ≠∅^{∅≠I⊆I_{n+1}}} ∑_{h≥1}(−1)^{|I|−1}v (⋁_{i∈I} z_{i}^{h}) = ∑_{{∅≠I⊆I_{n+1} \atop I\Ĩ≠∅}}(−1)^{|I|−1}v (⋁_{i∈I} w_{i}) .

Now, the left hand member is absolutely convergent, because v is a nonnegative function and

∑_{I\Ĩ≠∅^{∅≠I⊆I_{n+1}}} ∑_{h≥1} v (⋁_{i∈I} z_{i}^{h}) = ∑_{{∅≠I⊆I_{n+1} \atop I\Ĩ≠∅}} v (⋁_{i∈I} w_{i}) < +∞ .

Therefore we can rearrange the terms as we like, in particular we can swap the two summations symbols. Thus

∑_{h≥1} ∑_{I\Ĩ≠∅^{∅≠I⊆I_{n+1}}}(−1)^{|I|−1}v (⋁_{i∈I} z_{i}^{h}) = ∑_{{∅≠I⊆I_{n+1} \atop I\Ĩ≠∅}}(−1)^{|I|−1}v (⋁_{i∈I} w_{i}) .

So to prove our claim it is enough to show that

∑_{h≥1} ∑_{∅≠I\Ĩ⊆I^{h}}(−1)^{|I|−1}v (⋁_{i∈I} z_{i}) ≤ ∑_{h≥1} ∑_{{∅≠I⊆I_{n+1} \atop I\Ĩ≠∅}}(−1)^{|I|−1}v (⋁_{i∈I} z_{i}^{h}) .

Note that if I\Ĩ ⊆ I^{h} then ⋁_{i∈I} z_{i} = ⋁_{i∈I} z_{i}^{h}. Therefore we can rewrite the inequation as:

∑_{h≥1} ∑_{∅≠I\Ĩ⊆I^{h}}(−1)^{|I|−1}v (⋁_{i∈I} z_{i}^{h}) ≤ ∑_{h≥1} ∑_{{∅≠I⊆I_{n+1} \atop I\Ĩ≠∅}}(−1)^{|I|−1}v (⋁_{i∈I} z_{i}^{h}) .

To prove the inequation holds, it is then enough to show that for any h ≥ 1.

∑_{∅≠I\Ĩ⊆I^{h}}(−1)^{|I|−1}v (⋁_{i∈I} z_{i}^{h}) ≤ ∑_{I\Ĩ≠∅^{∅≠I⊆I_{n+1}}}(−1)^{|I|−1}v (⋁_{i∈I} z_{i}^{h}) .

Subtracting the same quantity from both members we get equivalently

0 ≤ ∑_{{∅≠I⊆I_{n+1} \atop I\(Ĩ∪I^{h})≠∅}}(−1)^{|I|−1}v (⋁_{i∈I} z_{i}^{h}) .

Let Ĩ^{h} := ⋃_{l≠h} I^{l}. We can rewrite the sum above as

∑_{∅≠J⊆Ĩ^{h}} ∑_{H⊆Ĩ∪I^{h}}(−1)^{|H|+|J|−1}v ( ⋁_{i∈H∪J} z_{i}^{h})

= ∑_{∅≠J⊆Ĩ^{h}}(−1)^{|J|−1} ∑_{H⊆Ĩ∪I^{h}}(−1)^{|H|}v ( ⋁_{i∈H∪J} z_{i}^{h}) .

Using BSV lemma (D.2) we can rewrite this as

∑_{∅≠K⊆Ĩ^{h}} ∑_{K⊆J⊆Ĩ^{h}}(−1)^{|J|+|K|} ∑_{H⊆Ĩ∪I^{h}}(−1)^{|H|}v ( ⋁_{i∈H∪J} z_{i}^{h})

= ∑_{∅≠K⊆Ĩ^{h}} ∑_{K⊆J⊆Ĩ^{h}} ∑_{H⊆Ĩ∪I^{h}}(−1)^{|K|+|J∪H|}v ( ⋁_{i∈H∪J} z_{i}^{h})

Fix K. Consider a set I such that K ⊆ I ⊆ I_{n+1}. Since Ĩ^{h}, Ĩ ∪ I^{h} are a partition of I_{n+1}, we have that H := I ∩ (Ĩ∪ I^{h}) and J := I ∩ Ĩ^{h} are a partition of I. We use this to rewrite the term above.

= ∑_{∅≠K⊆Ĩ^{h}} ∑_{K⊆I⊆I_{n+1}}(−1)^{|I|+|K|}v (⋁_{i∈I} z_{i}^{h}) .

For every K, and defining L := I \ K, we have that

∑_{K⊆I⊆I_{n+1}}(−1)^{|I|+|K|}v (⋁_{i∈I} z_{i}^{h})

= ∑_{L⊆I_{n+1}\K}(−1)^{|L|+2|K|}v ( ⋁_{i∈K} z_{i}^{h} ∨ ⋁_{j∈L} z_{j}^{h})
= (−1)^{0+2|K|}v ( ⋁_{i∈K} z_{i}^{h}) + ∑_{∅≠L⊆I_{n+1}\K}(−1)^{|L|+2|K|}v ( ⋁_{j∈L}(z_{j}^{h} ∨ ⋁_{i∈K} z_{i}^{h}))
= v ( ⋁_{i∈K} z_{i}^{h}) + ∑_{∅≠L⊆I_{n+1}\K}(−1)^{|L|}v ( ⋁_{j∈L}(z_{j}^{h} ∨ ⋁_{i∈K} z_{i}^{h}))
= v ( ⋁_{i∈K} z_{i}^{h}) − ∑_{∅≠L⊆I_{n+1}\K}(−1)^{|L|−1}v ( ⋁_{j∈L}(z_{j}^{h} ∨ ⋁_{i∈K} z_{i}^{h})) .

If ⋁_{i∈K} z_{i}^{h} = ⊤ then the whole sum is equal to 0. Otherwise it is equal to

ν_{0} \binom{}{⋁_{i∈K} z_{i}^{h}} − ν_{0} ( ⋃_{j∈I_{n+1}\K} { \atop z_{j}^{h} ∨ ⋁_{i∈K} z_{i}^{h}}) .

Note that for every j is

{ \atop z_{j}^{h} ∨ ⋁_{i∈K} z_{i}^{h}} ⊆ { \atop ⋁_{i∈K} z_{i}^{h}}

so that

⋃_{j∈I_{n+1}\K}({ \atop z_{j}^{h} ∨ ⋁_{i∈K} z_{i}^{h}}) ⊆ { \atop ⋁_{i∈K} z_{i}^{h}} .

Moreover observe that |I_{n+1} \ K| < n + 1. By induction hypothesis

ν_{0} \binom{}{⋁_{i∈K} z_{i}^{h}} − ν_{0} ( ⋃_{j∈I_{n+1}\K} { \atop z_{j}^{h} ∨ ⋁_{i∈K} z_{i}^{h}}) ≥ 0 .

Thus we have proved that for every n-tuple of finite configurations (x_{i}) and for every finite configuration y, if x̂_{1} ∪ … ∪ x̂_{n} ⊆ ŷ, then ν_{0} (x̂_{1} ∪ … ∪ x̂_{n}) ≤ ν_{0}(ŷ).

Monotonicity now follows from the following lemma: Lemma C.6. If x_{1}, …, x_{n+1} are finite configurations

ν_{0} (x̂_{1} ∪ … ∪ x̂_{n}) ≤ ν_{0} (x̂_{1} ∪ … ∪ x̂_{n} ∪ { \atop x_{n+1}}) .

Proof.

ν_{0} (x̂_{1} ∪ … ∪ x̂_{n} ∪ { \atop x_{n+1}})

= ∑_{∅≠I⊆I_{n+1}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i})
= ∑_{∅≠I⊆I_{n}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i}) + v(x_{n+1}) − ∑_{∅≠I⊆I_{n}}(−1)^{|I|−1}v (x_{n+1} ∨ ⋁_{i∈I} x_{i})
= ∑_{∅≠I⊆I_{n}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i}) + v(x_{n+1}) − ∑_{∅≠I⊆I_{n}}(−1)^{|I|−1}v (⋁_{i∈I} x_{n+1} ∨ x_{i})
= ν_{0} (x̂_{1} ∪ … ∪ x̂_{n}) + ν_{0} \binom{}{x_{n+1}} − ν_{0} ({ \atop x_{n+1} ∨ x_{1}} ∪ … ∪ { \atop x_{n+1} ∨ x_{n}})
≥ ν_{0} (x̂_{1} ∪ … ∪ x̂_{n}) .

Therefore, by induction on m,

ν_{0} (x̂_{1} ∪ … ∪ x̂_{n}) ≤ ν_{0} (x̂_{1} ∪ … ∪ x̂_{n} ∪ ŷ_{1} ∪ … ∪ ŷ_{m}) .

Finally, to show monotonicity of ν_{0}, suppose that

x̂_{1} ∪ … ∪ x̂_{n} ⊆ ŷ_{1} ∪ … ∪ ŷ_{m} .

Then

ŷ_{1} ∪ … ∪ ŷ_{m} = x̂_{1} ∪ … ∪ x̂_{n} ∪ ŷ_{1} ∪ … ∪ ŷ_{m} .

By the above observation we have

ν_{0} (x̂_{1} ∪ … ∪ x̂_{n}) ≤ ν_{0} (x̂_{1} ∪ … ∪ x̂_{n} ∪ ŷ_{1} ∪ … ∪ ŷ_{m})

= ν_{0} (ŷ_{1} ∪ … ∪ ŷ_{m}) .
□(C.6)

To prove modularity take x̂_{1} ∪ … ∪ x̂_{n} and ŷ_{1} ∪ … ∪ ŷ_{m}, we want to prove that

ν_{0} (x̂_{1} ∪ … ∪ x̂_{n}) + ν_{0} (ŷ_{1} ∪ … ∪ x̂_{m})

= ν_{0} (x̂_{1} ∪ … ∪ x̂_{n} ∪ ŷ_{1} ∪ … ∪ x̂_{m}) + ν_{0} ((x̂_{1} ∪ … ∪ x̂_{n}) ∩ (ŷ_{1} ∪ … ∪ x̂_{m})) . By distributivity we have that

(x̂_{1} ∪ … ∪ x̂_{n}) ∩ (ŷ_{1} ∪ … ∪ x̂_{m})

= (x̂_{1} ∩ ŷ_{1}) ∪ (x̂_{1} ∩ ŷ_{2}) ∪ … ∪ (x̂_{n} ∩ ŷ_{m}) .

Using the definitions, we have to prove that

R := ∑_{∅≠I⊆I_{n}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i}) + ∑_{∅≠J⊆I_{m}}(−1)^{|I|−1}v (⋁_{i∈I} y_{j})

is equal to

L := ∑_{I⊆I_{n},J⊆I_{m}^{∅≠I⊎J}}(−1)^{|I⊎J|−1}v (⋁_{i∈I} x_{i} ∨ ⋁_{j∈J} y_{j})

+ ∑_{∅≠K⊆I_{n}×I_{m}}(−1)^{|K|−1}v ( ⋁_{(i,j)∈K}(x_{i} ∨ y_{j})) .

We can split the various I ⊎ J in three classes: when J is empty, when I is empty, and when both are not empty. So we can rewrite L as

L = ∑_{∅≠I⊆I_{n}}(−1)^{|I|−1}v (⋁_{i∈I} x_{i})

+ ∑_{∅≠J⊆I_{m}}(−1)^{|I|−1}v ( ⋁_{j∈J} y_{j})

+ ∑_{{∅≠I⊆In \atop ∅≠J⊆Im}}(−1)^{|I⊎J|−1}v (⋁_{i∈I} x_{i} ∨ ⋁_{j∈J} y_{j})

+ ∑_{∅≠K⊆I_{n}×I_{m}}(−1)^{|K|−1}v ( ⋁_{(i,j)∈K}(x_{i} ∨ y_{j})) .

The first two summands of this expression are equal to R, so we have just to prove that the last two are equal to 0.

For every ∅ ≠ I ⊆ I_{n}, ∅ ≠ J ⊆ I_{m} consider all K ⊆ I_{n} × I_{m} such that π_{1}(K) = I, π_{2}(K) = J. We argue that for all such K,

⋁_{(i,j)∈K}(x_{i} ∨ y_{j}) = ⋁_{i∈I} x_{i} ∨ ⋁_{j∈J} y_{j} .

In fact using commutativity, associativity and idempotency of the join, we can group all the x_{i} and y_{j} on the left hand member. So that

⋁_{(i,j)∈K}(x_{i} ∨ y_{j}) = ⋁_{i∈π_{1}(K)} x_{i} ∨ ⋁_{j∈π_{2}(K)} y_{j} .

We can rewrite the the last two summands of the above expression as

∑_{{∅≠I⊆In \atop ∅≠J⊆Im}}(−1)^{|I⊎J|−1}v (⋁_{i∈I} x_{i} ∨ ⋁_{j∈J} y_{j})

+ ∑_{{∅≠I⊆In \atop ∅≠J⊆Im}} ∑_{{∅≠K⊆In×Im \atop π_{1}(K)=I,π_{2}(K)=J}}(−1)^{|K|−1}v ( ⋁_{(i,j)∈K}(x_{i} ∨ y_{j}))

= ∑_{{∅≠I⊆In \atop ∅≠J⊆Im}}(−1)^{|I⊎J|−1}v (⋁_{i∈I} x_{i} ∨ ⋁_{j∈J} y_{j})

+ ∑_{{∅≠I⊆In \atop ∅≠J⊆Im}} ∑_{{∅≠K⊆In×Im \atop π_{1}(K)=I,π_{2}(K)=J}}(−1)^{|K|−1}v (⋁_{i∈I} x_{i} ∨ ⋁_{j∈J} y_{j})

= ∑_{{∅≠I⊆In \atop ∅≠J⊆Im}} v (⋁_{i∈I} x_{i} ∨ ⋁_{j∈J} y_{j}) ((−1)^{|I⊎J|−1} + ∑_{{∅≠K⊆In×Im \atop π_{1}(K)=I,π_{2}(K)=J}}(−1)^{|K|−1}) .

So it is enough to prove that for every finite sets I, J

(−1)^{|I⊎J|−1} + ∑_{{∅≠K⊆In×Im \atop π_{1}(K)=I,π_{2}(K)=J}}(−1)^{|K|−1} = 0 .

which is the statement of Lemma D.1, to be proved in Appendix C. □ Now we are ready to define ν on all Scott open sets.

Lemma C.7. For every Scott open O ⊆ L(E), we have that the set {U ∈ Bs | U ⊆ O} is directed and

O = ⋃_{{U⊆O \atop U∈Bs}} U .

Proof. Directedness is straightforward. Moreover, since L(E) is algebraic, P n is a basis for the Scott topology (and so is, a fortiori, Bs). □

Now, for every Scott open set O, define

ν(O) = sup_{{U⊆O \atop U∈Bs}} ν_{0}(U) .

We then have the following, which concludes the proof of Theorem 4.4.

Lemma C.8. The function ν is a valuation on the Scott-topology of L(E) such that for every finite configuration x, ν(↑ x) = v(x).

Continuity follows from an exchange of suprema, strictness and monotonicity are obvious. Modularity follows from the modularity of ν_{0} and continuity of the addition. Finally, because of the monotonicity of ν_{0}, we have that ν(↑ x) = ν_{0}(↑ x) = v(x). □

It remains to show that ν is non-leaking. We do this in the next section.

C.2 Inductive tests

In order to show that ν in non-leaking, we will introduce a restricted notion of test. Before we look at tests in the context on the domain of configuration. These result are valid in any event structure.

Definition C.9. Let C be a finitary set of configurations of an event structure E. We define ↑ (C) as the set ⋃_{x∈C} ↑ x.

Clearly ↑ (C) is Scott open. All the following properties are straightforward.

Proposition C.10. Let C be a finitary partial test of E, then the Scott open subsets of L(E) of the form ↑ x, for x ∈ C are pairwise disjoint. If C, C′ are two finitary sets of configurations of E and C ≤ C′ then ↑ (C) ⊇↑ (C′). If C be a finitary complete set of configurations of E, then for every maximal configuration y ∈ L(E), we have that y ∈↑ (C).

Proposition C.11. Let C, C′ be finitary tests. Then C ≤ C′ if and only if ↑ (C) ⊇↑ (C′).

Proof. of the non-trivial direction. Suppose ↑ (C) ⊇↑ (C′). If y ∈ C′ then y ∈↑ (C) which means that there exists x ∈ C such that x ≤ y. Vice versa if x ∈ C then by completeness there exists y ∈ C′ such that x, y are compatible. We have just argued that there exists x′ ∈ C such that x′ ≤ y, which implies that x, x′ are compatible. Since C is a test, we have that x = x′ and x ≤ y. □

Corollary C.12. Let ν be a continuous valuation on L(E). If C is a finitary partial test, then ν(↑ (C)) = ∑_{x∈C} ν(↑ x). If C, C′ are finitary sets of configurations and C ≤ C′ then ν(↑ (C)) ≥ ν(↑ (C′)).

As a corollary we have

Theorem C.13. Let ν be a non-leaking valuation on L(E). Define v : L_{fin}(E) → [0, 1] by v(x) = ν(↑ x). Then v is a test valuation.

Proof. Take a finitary test C. By the proposition above we have that ↑ (C) ⊇ Ω(L(E)). Therefore, since ν is non-leaking.

1 ≥ ν(↑ (C)) = ν̄(↑ (C)) ≥ ν̄(Ω(L(E))) = 1

which implies ν(↑ (C)) = 1. Since the sets of the form ↑ x, for x ∈ C are pairwise disjoint, we have ∑_{x∈C} ν(↑ x) = 1, which finally implies that ∑_{x∈C} v(x) = 1. □

We now define a special notion of test, only for confusion-free event structure.

Definition C.14. Let E be a confusion-free event structure. If x is a configuration of E, and c is a cell accessible at x we define x + c do be the set {x ∪ {e} |e ∈ c}. Let Y, Y′ be two sets of configurations of a confusion-free event structure. We write

\xymatrix{Y \ar[r]^{X,(c_{x})} & Y′}

when X ⊆ Y, for every x ∈ X, c_{x} is a cell accessible at x, and

Y′ = Y \ X ∪ ⋃_{x∈X} x + c_{x} .

We write Y → Y′ if there are X, (c_{x}) such that \xymatrix{Y \ar[r]^{X,(c_{x})} & Y′}. As usual →^{∗} denotes the reflexive and transitive closure of →.

Definition C.15. An inductive test of a confusion-free event structure is a set C of configurations such that

{∅} →^{∗} C .

The idea is that we start the computation with the empty configuration, and, at every step, we choose accessible cells to “activate” and we collect all the resulting configurations. The next proposition is a sanity check for our definitions

Proposition C.16. If C, C′ are inductive tests

C ≤ C′ ⟺ C →^{∗} C′ .

The direction ⟸) is proved by induction on the derivation C →^{∗} C′. The direction ⟹) is by induction on the derivation {∅} →^{∗} C. See [Var03].

As the choice of the name suggests we have the following result.

Proposition C.17. Every inductive test is a finitary test.

Proof. By induction on the derivations. The singleton of the empty configuration is a test. Take an inductive test C, a set X ⊆ C and for every x ∈ X a cell (c_{x}) accessible

at x. Let \xymatrix{C \ar[r]^{X,(c_{x})} & C′}. We want to show that C′ is a test.

First consider two distinct configurations x′, y′ ∈ C′. If x′, y′ ∈ C then they are incompatible by induction hypothesis. If x′ ∈ C, and y′ = y ∪ e for some y ∈ C, then x′ ≠ y, so that x′, y are incompatible. Thus x′, y′ are incompatible. If x′ = x ∪ e_{x} and y′ = y ∪ e_{y} for x, y ∈ C there are two possibilities. If x ≠ y, then they are incompatible and so are x′, y′. If x = y, then e_{x} ≠ e_{y}, but they both belong to they same cell, therefore they are in conflict, and x′, y′ are incompatible.

Now take any configuration z. By induction hypothesis there exists x ∈ C such that x, z are compatible. If x ∈ C′ we are done. If x ∉ C′ then there are two possibilities. Either z does not fill c_{x}, but then for every e ∈ c_{x}, z, x ∪ e are compatible. Or z fills c_{x} with and event ē which implies that z, x ∪ ē are compatible. □

As a corollary we have

Proposition 5.9. If E is a confusion-free event structure and if x is a finite configuration of E, then x is honest in L(E).

Proof. Given a finite configuration x, we obtain an inductive test containing x by firing all the cells of the events of x. □

Not all test are inductive as the following example shows. Consider the event structure E = ⟨E, ≤, #⟩ where E = {a_{1}, a_{2}, b_{1}, b_{2}, c_{1}, c_{2}, d}, the order is trivial and a_{1} # a_{2}, b_{1} # b_{2}, c_{1} # c_{2}. Let’s call the three cells a, b, c.

[figure: a_{1}; a_{2}; b_{1}; b_{2}; c_{1}; c_{2}; d]

Consider the following set C of configurations

{{a_{1}, b_{2}, d}, {b_{1}, c_{2}, d}, {a_{2}, c_{1}, d}, {a_{1}, b_{1}, c_{1}}, {a_{2}, b_{2}, c_{2}}} .

The reader can easily verify that C is a test. If it were an inductive test, we should be able to identify a cell that was chosen at the first step along the derivation. Because of the symmetry of the situation, we can check whether it is a. If a were the first cell chosen, every configuration in C would contain either a_{1} or a_{2}. But this is not the case^{2}.

It is now easy to show the following

Proposition C.18. If v is a configuration valuation, and if C is an inductive test, then, v[C] = 1.

Proof. By induction on the derivation Suppose \xymatrix{C \ar[r]^{X,c_{x}} & C′} and ∑_{x∈C} v(x) = 1. Consider ∑_{x′∈C′} v(x′). We can split this in

∑_{x∈C\X} v(x) + ∑_{x∈X} ∑_{e∈c_{x}} v(x ∪ {e}) .

Since v is a configuration valuation, property (b) of definition 4.3 tells us that for every x ∈ X, ∑_{e∈c_{x}} v(x ∪ {e}) = v(x). Therefore

∑_{x∈C\X} v(x) + ∑_{x∈X} ∑_{e∈c_{x}} v(x ∪ {e})

= ∑_{x∈C\X} v(x) + ∑_{x∈X} v(x) = ∑_{x∈C} v(x) = 1 .

□

We can finally prove the following theorem, which concludes the proof of Theorem 4.4

Theorem C.19. Let ν be a continuous valuation corresponding to a configuration valuation v. Then ν is non-leaking.

We show that there exists an enumeration of the cells (c_{n})_{n∈ℕ}, such that if c_{m} < c_{n}, then m < n. We build it as follows. Since the cells are countably many, they come equipped already with some enumeration. We start by picking the first cell c. We enumerate all the cells c′ < c, by layers: first the cells of depth 0, then the cells of depth 1 and so on. There are only finitely many such c′, so we stop at some point. Finally we enumerate c. For all the cells enumerated so far c_{m} < c_{n} implies m < n

2 This example bears a striking familiarity with Berry’s Gustave function

At every step, choose the next cell c (in the old enumeration) that has not been enumerated. Repeat the procedure above, enumerating the cells c′ < c that have not yet been enumerated. Finally enumerate c. The invariant c_{m} < c_{n} ⟹ m < n is preserved.

With this enumeration at hand, consider the following chain of inductive tests: C_{0} =

\{∅\}, \xymatrix{C_{n} \ar[r]^{X,c_{n}} & C_{n+1}} , where X is the set of configurations x ∈ C_{n} such that c_{n} is accessible at x. We have the following properties:

1. for every C_{n}, Ω(L(E)) ⊆↑ (C_{n});

2. ↑ (C_{n}) ⊇↑ (C_{n+1});

3. if x ∈ C_{n} and x fills c_{m} then m < n;

4. if x ∈ C_{n} then every cell c_{m} with m < n enabled at x is filled by x;

5. for every non maximal configuration z there exists n such that z ∉↑ (C_{n}).

Property (1) comes for the fact the C_{n} is a test. Property (2) comes from Proposition C.11. Property (3) is by construction. Property (4) is shown by induction on n, using the defining property of the enumeration. Take x ∈ C_{n+1} and consider a cell c_{m} with m < n + 1 enabled at x. If m < n then c_{n} ≮ c_{m} therefore c_{m} is enabled at x′ := x \ c_{n} ∈ C_{n}. By induction hypothesis c_{m} is filled by x′, and therefore is filled by x. If m = n then x has just been obtained by adding an event in c_{m} (otherwise c_{m} would not be enabled). To show (5), take a non maximal configuration z. There exists a cell c which is accessible at z. Suppose it’s c_{m}. Consider C_{m+1}. Suppose there exists x ∈ C_{m+1} such that x ≤ z. Then c_{m} is not filled by x. By property (4), c is not enabled at x. Consider a minimal event e in [c) \ x, and say c_{h} = cell(e). Since c_{h} < c = c_{m}, then h < m. By minimality of e, every event in [c_{h}) is in x. Therefore c_{h} is enabled at x. By property (4) c_{h} is filled by x. Since [c) ⊆ z we have that e ∈ z. Thus the only event in the cell of e that can be in x is e itself. Contradiction.

Therefore, combining (1) and (5)

⋂_{n∈ℕ} ↑ (C_{n}) = Ω(L(E)) .

By Theorem A.2, the valuation ν can be extended to a Borel measure ν̄. We have that ν̄(Ω(L(E))) = lim_{n→∞} ν̄(↑ (C_{n})). But ν̄(↑ (C_{n})) = ν(↑ (C_{n})) = 1 because C_{n} is an inductive test. By Theorem A.1 we have ν̄(Ω(L(E))) = 1. This implies that for every open set O ⊇ Ω(L(E)) we have

1 ≥ ν(0) = ν̄(0) ≥ ν̄(Ω(L(E))) = 1 .
□

As a corollary, using Theorem C.13 we get

Theorem C.20. If v is a configuration valuation, then v is a test valuation.

The other direction is also true

Theorem C.21. If v is a test valuation, then v is a configuration valuation.

Proof. First of all v(∅) = 1, because {∅} is a finitary test. Next we want to show that for every finite configuration x and every covering D_{c} at x, v[D_{c}] = v(x). Take a test C containing x, which exists because x is honest. Consider the test C′ = C \ {x} ∪ D_{c}.

Notice that \xymatrix{C \ar[r]^{\{x\},c} & C′}. Therefore C′ is a test. So that v[C′] = 1. But v[C′] = v[C] − v(x) + v[D_{c}]. □

We have thus proved

Theorem 5.7. Let E be a confusion-free event structure. Let v be a function L_{fin}(E) → [0, 1]. Then v is a configuration valuation if and only if it is a test valuation.

Note also that combining Theorems C.13 and C.21 we obtain

Theorem 4.5. Let ν be a non-leaking continuous valuation on L(E). The function v : L_{fin}(E) → [0, 1] defined by v(x) = ν(↑ x) is a configuration valuation.

C.3 Continuous Valuation and Runs

Theorem 5.2. Let ν be a non-leaking normalised continuous valuation on a coherent ω-algebraic domain D. Then there is a unique probability measure μ on S such that for every compact element x, μ(K(x)) = ν(↑ x). Let μ be a probability measure on S. Then the function ν defined on open sets by ν(O) = μ(O ∩ Ω(D)) is a non-leaking normalised continuous valuation.

Proof. Let μ be a probability measure on ⟨Ω(D), S⟩. The sets of the form ↑ x for x compact are a basis of the Scott topology. Since the set of compact elements is countable, every open set O is the countable union of basic open sets. Therefore every set of the form O ∩ Ω(D) is the countable union of shadows of compact elements, and it belongs to S. Thus ν is well defined. It is obviously strict, monotone and modular. By ω-algebraicity, to prove continuity it is enough to prove continuity for ω-chains ([AM00], Lemma 2.10). Take a countable increasing chain O_{k} with limit O. Since μ is a measure

μ(O ∩ Ω(D)) = sup_{k∈ℕ} μ(O_{k} ∩ Ω(D)) .

Thus

ν(O) = μ(O ∩ Ω(D)) = sup_{k∈ℕ} μ(O_{k} ∩ Ω(D)) = sup_{k∈ℕ} ν(O_{k})

and we are done. The fact that ν is non-leaking follows from the definition.

Conversely, take a non-leaking valuation ν. By the extension theorem for continuous valuations of [AES00], there is a unique measure ν̂ on the Scott-Borel sets of D which extends ν. By Corollary 3.4 and 3.5 of [Law97], recalling that a coherent domain is Lawson compact, there exists a decreasing countable chain of open sets converging to Ω(D), which is thus a G_{δ} set and therefore is measurable. Since ν is non-leaking, ν̂(Ω(D)) = 1. Define μ to be the restriction of ν̂ to Ω(D). It is indeed a probability measure. Every set of the form O ∩ Ω(D) is measurable, and

μ(O ∩ Ω(D)) = ν̂(O ∩ Ω(D))

= ν̂(O) + ν̂(Ω(D)) − ν̂(O ∪ Ω(D)) .

Since Ω(D) ⊆ O ∪ Ω(D) ⊆ D and ν̂(D) = ν̂(Ω(D)) = 1, then also ν̂(O ∪ Ω(D)) = 1, so that

μ(O ∩ Ω(D)) = ν̂(O) = ν(O)

and we are done. □ As an easy corollary of this Theorem5.2 and of Theorem C.13 we have

Theorem 5.6. Let μ be a probabilistic run of E. Define v : L_{fin}(E) → [0, 1] by v(x) = μ(K(x)). Then v is a test valuation.

The following results applies to confusion free event structures only.

Proposition 5.3. Let v be a configuration valuation on a confusion-free event structure E. Let μ_{v} be the corresponding measure as of Propositions 4.1 and Theorem 5.2. Then, v is a configuration valuation with independence iff for every two finite compatible configurations x, y

μ_{v}(K(x) ∩ K(y) | K(x ∩ y)) = μ_{v}(K(x) | K(x ∩ y)) · μ_{v}(K(y) | K(x ∩ y)).

Proof. Suppose v satisfies condition (c) of proposition 2.8. Take μ_{v}(K(x) ∩ K(y) | K(x ∩ y)). By definition (and assuming μ_{v}(K(x ∩ y)) ≠ 0) we have

μ_{v}(K(x) ∩ K(y) | K(x ∩ y))
= μ_{v}(K(x) ∩ K(y) ∩ K(x ∩ y))/μ_{v}(K(x ∩ y))
= μ_{v}(K(x) ∩ K(y))/μ_{v}(K(x ∩ y))
= μ_{v}(K(x ∪ y))/μ_{v}(K(x ∩ y))
= v(x ∪ y)/v(x ∩ y) = v(x) · v(y)/v(x ∩ y)^{2}
= (v(x)/v(x ∩ y)) · (v(y)/v(x ∩ y))
= (μ_{v}(K(x))/μ_{v}(K(x ∩ y)))
·(μ_{v}(K(y))/μ_{v}(K(x ∩ y)))
= (μ_{v}(K(x) ∩ K(x ∩ y))/μ_{v}(K(x ∩ y)))
·(μ_{v}(K(y) ∩ K(x ∩ y))/μ_{v}(K(x ∩ y)))
= μ_{v}(K(x) | K(x ∩ y)) · μ_{v}(K(y) | K(x ∩ y)) .

The converse is similar. □ In the following we prove a generalisation of Theorem 5.10. We generalise the

notions of test and finitary test to any coherent ω-algebraic domain. A partial test of a domain D is a set C of pairwise incompatible elements of D. A test is a maximal partial test. A test is finitary if all its elements are compact. Let v be a function Cp(D) → [0, 1]. Then v is called a test valuation if for all finitary test C we have v[C] = 1. A finitary partial test is honest if it is part of a finitary test. A compact element is honest if it is honest as partial test.

Theorem 5.10. Let D be a coherent ω-algebraic domain. Let v be a test valuation on D. Let H be the σ-algebra on Ω(D) generated by the shadows of honest compact elements. Then there exists a unique measure μ on H such that μ(K(x)) = v(x) for every honest compact element x.

Proof. Consider the following set T of subsets of Ω(D):

T := {K(C) | C is a honest finitary partial test} .

We claim that T is a field of sets, i.e., that it is closed under binary union and complementation. Since C is honest, it can be extended to a finitary test A. Let’s call C′ := A \ C. Clearly C′ is a honest finitary partial test. And K(C′) = \overline{K(C)}. On the one hand K(C′) ∪ K(C) = Ω(D), because of completeness of A. On the other hand K(C′) ∩ K(C) = ∅ as otherwise some element of C will be compatible with some elements of C′. For the closure under union, consider two honest finitary partial tests C_{1}, C_{2}. Consider their completions A_{1}, A_{2} and put C′_{1} := A_{1} \C_{1}, C′_{2} := A_{2} \C_{2}. Let A be an common upper bound of A_{1}, A_{2}, which exists as finitary tests form a lattice. Consider the subsets C of A defined as

C := {x ∈ A | ∃x_{1} ∈ C_{1}.x_{1} ≤ x or ∃x_{2} ∈ C_{2}.x_{2} ≤ x} .

Clearly C is a honest finitary partial test. We claim that K(C) = K(C_{1})∪K(C_{2}). Take z ∈ K(C). This means that there exists x ∈ C such that x ≤ z. Then either there exists x_{1} ∈ C_{1}, with x_{1} ≤ x ≤ z, or there exists x_{2} ∈ C_{2}, with x_{2} ≤ x ≤ z. Either case z ∈ K(C_{1}) ∪ K(C_{2}).

Conversely assume z ∈ K(C_{1}) ∪ K(C_{2}), say z ∈ K(C_{1}). There is x_{1} ∈ C_{1} such that x_{1} ≤ z. Since A is complete there must exist x ∈ A such that x ≤ z. Since A_{1} ≤ A there exists x′_{1} ∈ A_{1} such that x′_{1} ≤ x ≤ z. This implies that x′_{1}, x_{1} are compatible. Since A_{1} is a test, x′_{1} = x_{1}. Therefore x ∈ C, and z ∈ K(C).

We define a function m : T → [0, 1] by m(K(C)) = v[C]. We have to argue that m is well defined, i.e. if C_{1}, C_{2} are such that K(C_{1}) = K(C_{2}), then v[C_{1}] = v[C_{2}]. Suppose A_{1} is a test completing C_{1} and put C′_{1} = A_{1} \ C_{1}. Then C_{2} ∪ C′_{1} is a finitary test too. It is clearly complete, and if an element of C′_{1} were compatible with an element of C_{2} then it would also be compatible with some element of C_{1} contradicting that A_{1} is a test. Thus v[C_{1}] = 1 − v[C′_{1}] = v[C_{2}].

Now we argue that m is σ-additive on T . Take a sequence C_{n} of honest partial tests such that K(C_{n}) ∩ K(C_{m}) = ∅ and such that ⋃_{n} K(C_{n}) = K(C) for some C. Then we have to prove that

∑_{n} m(K(C_{n})) = m(K(C)) .

Consider C′ such that C ∪ C′ = ∅ and C ∪ C′ is a finitary test. Then, by the same argument used above, ⋃_{n} C_{n} ∪ C′ is a finitary test. Note the condition on disjointness of the K(C_{n}). Therefore

v [⋃_{n} C_{n}] = 1 − v[C′] = v[C] = m(K(C)) .

On the other hand, rearranging the terms (and recalling the disjointness again) we get

v [⋃_{n} C_{n}] = ∑_{n} v[C_{n}] = ∑_{n} m(K(C_{n})) .

Thus m is a σ-additive function defined on the field of sets T . By Caratheodory extension theorem we can extend m to a measure μ on the σ-algebra generated by T , which contains H. Thus for all honest finite elements, K(x) is measurable and μ(K(x)) = m(K(x)) = v(x). □

Theorem 5.11. If all compact elements are honest, then for every test valuation v there exists a unique continuous valuation ν, such that ν(↑ x) = v(x).

Proof. Once we have the measure μ of Theorem 5.10, we define ν(↑ x) := μ(K(x)). It is well defined as x is honest and therefore K(x) is measurable. Then ω-algebraicity of D ensures that ν is a continuous valuation. □

C.4 An Alternative Way for the Proofs

An alternative way for proving all the results consists in starting from a result in the extended version of [Voe01]. Adapting Lemma A.2 there, we obtain a direct proof of Theorem C.20, and thus we get Theorem 5.7. Then via Theorems 5.10 and 5.2 we prove Theorem 4.4, avoiding the combinatorial technicalities of its direct proof.

D Combinatorial Lemmas

We prove here two lemmas used during the proof of Theorem 4.4.

Lemma D.1. For every finite sets I, J with |I| = n, |J| = m

∑_{π_{1}(K)=I,π_{2}(K)=J^{∅≠K⊆I×J}}(−1)^{|K|} = (−1)^{n+m−1} .

Proof. Without loss of generality we can think of I = {1, …, n} and J = {1, …, m}. Also we observe that a subset K ⊆ I × J such that π_{1}(K) = I, π_{2}(K) = J is in fact a surjective and total relation between the two sets.

[figure: n; m]

Let

t_{n,m} := ∑_{π_{1}(K)=I,π_{2}(K)=J^{∅≠K⊆I×J}}(−1)^{|K|};

t_{n,m}^{o} := |{∅ ≠ K ⊆ I × J | |K| odd, π_{1}(K) = I, π_{2}(K) = J}|;

t_{n,m}^{e} := |{∅ ≠ K ⊆ I × J | |K| even, π_{1}(K) = I, π_{2}(K) = J}| .

Clearly t_{n,m} = t_{n,m}^{e} − t_{n,m}^{o}. We want to prove that t_{n,m} = (−1)^{n+m+1}. We do this by induction on n. It is easy to check that this is true for n = 1. In this case, if m is even then t_{1,m}^{e} = 1 and t_{1,m}^{o} = 0, so that t_{1,m}^{e} − t_{1,m}^{o} = (−1)^{1+m+1}. Similarly if m is odd.

Now let’s assume that for every p, t_{n,p} = (−1)^{n+p+1} and let’s try to compute t_{n+1,m}. To evaluate t_{n+1,m} we count all surjective and total relations K between I and J together with their“sign”. Consider the pairs in K of the form (n + 1, h) for h ∈ J. What do you get if you remove them? You get a total surjective relation between {1, …, n} and a subset J_{K} of {1, …, m}.

[figure: n; •; m; s]

Consider first the case where J_{K} = {1, …, m}. What is the contribution of such K’s to t_{n+1,m}? There are \binom{m}{s} ways of choosing s pairs of the form (n + 1, h). And for every such choice there are t_{n,m} (signed) relations. Adding the pairs (n+1, h) possibly modifies the sign of such relations. All in all the contribution amounts to

∑_{1≤s≤m} \binom{m}{s}(−1)^{s}t_{n,m} .

Suppose now that J_{K} is a proper subset of {1, …, m} leaving out r elements.

[figure: n; •; s; r]

Since K is surjective, all such elements h must be in a pair of the form (n + 1, h). Moreover there can be s pairs of the form (n + 1, h′) with h′ ∈ J_{K}. What is the contribution of such K’s to t_{n,m}? There are \binom{m}{r} ways of choosing the elements that are left out. For every such choice and for every s such that 0 ≤ s ≤ m−r there are \binom{m−r}{s} ways of choosing the h′ ∈ J_{K}. And for every such choice there are t_{n,m−r} (signed) relations. Adding the pairs (n + 1, h) and (n + 1, h′) possibly modifies the sign of such relations. All in all, for every r such that 1 ≤ r ≤ m − 1, the contribution amounts to

\binom{m}{r} ∑_{1≤s≤m−r} \binom{m}{s}(−1)^{s+r}t_{n,m−n} .

The (signed) sum of all these contribution will give us t_{n+1,m}. Now we use the induction hypothesis and we write (−1)^{n+p+1} for t_{n,p}. Thus:

t_{n+1,m} = ∑_{1≤s≤m} \binom{m}{s}(−1)^{s}t_{n,m}

+ ∑_{1≤r≤m−1} \binom{m}{r} ∑_{0≤s≤m−r} \binom{m − r}{s}(−1)^{s+r}t_{n,m−r}

= ∑_{1≤s≤m} \binom{m}{s}(−1)^{s+n+m+1}

+ ∑_{1≤r≤m−1} \binom{m}{r} ∑_{0≤s≤m−r} \binom{m − r}{s}(−1)^{s+n+m+1}

= (−1)^{n+m+1} ( ∑_{1≤s≤m} \binom{m}{s}(−1)^{s}

+ ∑_{1≤r≤m−1} \binom{m}{r} ∑_{0≤s≤m−r} \binom{m − r}{s}(−1)^{s}) .

By the binomial formula, for 1 ≤ r ≤ m − 1 we have

0 = (1 − 1)^{m−r} = ∑_{0≤s≤m−r} \binom{m − r}{s}(−1)^{s} .

So we are left with

t_{n+1,m} = (−1)^{n+m+1} ( ∑_{1≤s≤m} \binom{m}{s}(−1)^{s})

= (−1)^{n+m+1} ( ∑_{0≤s≤m} \binom{m}{s}(−1)^{s} − \binom{m}{0}(−1)^{0})

= (−1)^{n+m+1} (0 − 1)

= (−1)^{n+1+m+1} = (−1)^{(n+1)+m−1} . □

Lemma D.2 (BSV lemma). Let X be a finite set and let f : P (X) → ℝ. Then

∑_{∅≠J⊆X}(−1)^{|J|−1}f(J) = ∑_{∅≠K⊆X} ∑_{K⊆J⊆X}(−1)^{|J|+|K|}f(J) .

Proof. By induction on |X|. The base is obvious. Let X′ = X ∪ {∗}, with ∗ ∉ X. Consider

∑_{∅≠K⊆X′} ∑_{K⊆J⊆X′}(−1)^{|J|+|K|}f(J)

We can split the sum in two, according to whether K contains or does not contain ∗.

= ∑_{∅≠K⊆X} ∑_{K⊆J⊆X′}(−1)^{|J|+|K|}f(J) + ∑_{∗∈K⊆X′} ∑_{K⊆J⊆X′}(−1)^{|J|+|K|}f(J)

We now rewrite the second part of the expression, singling out the case where K = {∗}. In all the other cases we can write K as H ∪ {∗} for some nonempty H ⊆ X.

= ∑_{∅≠K⊆X} ∑_{K⊆J⊆X′}(−1)^{|J|+|K|}f(J)

+ ∑_{∅≠H⊆X} ∑_{H∪{∗}⊆J⊆X′}(−1)^{|J|+|H|+1}f(J) + ∑_{∗∈J⊆X′}(−1)^{|J|+1}f(J)

We now split each of the inner sums in the first line according to whether J contains or does not contain ∗. Also note that (−1)^{|J|+1} = (−1)^{|J|−1}. We have then

= ∑_{∅≠K⊆X} ( ∑_{K⊆J⊆X}(−1)^{|J|+|K|}f(J) + ∑_{K∪{∗}⊆J⊆X′}(−1)^{|J|+|K|}f(J))

+ ∑_{∅≠H⊆X} ∑_{H∪{∗}⊆J⊆X′}(−1)^{|J|+|H|+1}f(J) + ∑_{∗∈J⊆X′}(−1)^{|J|−1}f(J)

= ∑_{∅≠K⊆X} ∑_{K⊆J⊆X}(−1)^{|J|+|K|}f(J) + ∑_{∅≠K⊆X} ∑_{K∪{∗}⊆J⊆X′}(−1)^{|J|+|K|}f(J)

+ ∑_{∅≠H⊆X} ∑_{H∪{∗}⊆J⊆X′}(−1)^{|J|+|H|+1}f(J) + ∑_{∗∈J⊆X′}(−1)^{|J|−1}f(J)

Now the second and the third member of the expression above cancel out.

= ∑_{∅≠K⊆X} ∑_{K⊆J⊆X}(−1)^{|J|+|K|}f(J) + ∑_{∗∈J⊆X′}(−1)^{|J|−1}f(J)

We now use the induction hypothesis on the first member

= ∑_{∅≠J⊆X}(−1)^{|J|−1}f(J) + ∑_{∗∈J⊆X′}(−1)^{|J|−1}f(J) = ∑_{∅≠J⊆X′}(−1)^{|J|−1}f(J) . □

Recent BRICS Report Series Publications

RS-04-10 Daniele Varacca, Hagen Völzer, and Glynn Winskel. Probabilistic Event Structures and Domains. June 2004. 41 pp. Extended version of an article to appear in Gardner and Yoshida, editors, Concurrency Theory: 15th International Conference, CONCUR ’04 Proceedings, LNCS, 2004.

RS-04-9 Ivan B. Damgård, Serge Fehr, and Louis Salvail. Zero-Knowledge Proofs and String Commitments Withstanding Quantum Attacks. May 2004. 22 pp.

RS-04-8 Petr Jančar and Jiří Srba. Highly Undecidable Questions for Process Algebras. April 2004. 25 pp. To appear in Lévy, Mayr and Mitchell, editors, 3rd IFIP International Conference on Theoretical Computer Science, TCS ’04 Proceedings, 2004.

RS-04-7 Mojmír Křetínský, Vojtěch Řehák, and Jan Strejček. On the Expressive Power of Extended Process Rewrite Systems. April 2004. 18 pp.

RS-04-6 Gudmund Skovbjerg Frandsen and Igor E. Shparlinski. On Reducing a System of Equations to a Single Equation. March 2004. 11 pp. To appear in Schicho and Singer, editors, ACM SIGSAM International Symposium on Symbolic and Algebraic Computation, ISSAC ’04 Proceedings, 2004.

RS-04-5 Biernacki Dariusz and Danvy Olivier. From Interpreter to Logic Engine by Defunctionalization. March 2004. 20 pp. To appear in Bruynooghe, editor, International Symposium on Logic Based Program Development and Transformation, LOPSTR ’03 Proceedings, Revised Selected Papers, LNCS, 2003. This report supersedes the earlier BRICS report RS-03-25.

RS-04-4 Patricia Bouyer, Franck Cassez, Emmanuel Fleury, and Kim G. Larsen. Optimal Strategies in Priced Timed Game Automata. February 2004. 32 pp.

RS-04-3 Mads Sig Ager, Olivier Danvy, and Jan Midtgaard. A Functional Correspondence between Call-by-Need Evaluators and Lazy Abstract Machines. February 2004. 17 pp. This report supersedes the earlier BRICS report RS-03-24. Extended version of an article to appear in Information Processing Letters.