Stone Duality for Markov Processes
Transcript Of Stone Duality for Markov Processes
Stone Duality for Markov Processes
Dexter Kozen1
Kim G. Larsen2 Radu Mardare2 Prakash Panangaden3
1Computer Science Department, Cornell University, Ithaca, New York, USA 2Department of Computer Science, University of Aalborg, Aalborg, Denmark
3School of Computer Science, McGill University, Montreal, Canada
March 14, 2013
Abstract
We define Aumann algebras, an algebraic analog of probabilistic modal logic. An Aumann algebra consists of a Boolean algebra with operators modeling probabilistic transitions. We prove that countable Aumann algebras and countably-generated continuous-space Markov processes are dual in the sense of Stone. Our results subsume existing results on completeness of probabilistic modal logics for Markov processes.
1 Introduction
The Stone representation theorem [1] is a recognized landmarks of mathematics. The theorem states that every (abstract) Boolean algebra is isomorphic to a Boolean algebra of sets. In fact, Stone proved much more: that Boolean algebras are dual to a certain category of topological spaces known as Stone spaces. See Johnstone [2] for a detailed and eloquent introduction to this theorem and its ramifications, as well as an account of several other related dualities, like Gelfand duality, that appear in mathematics.
Formally, Stone duality states that the category of Boolean algebras and Boolean algebra homomorphisms and the category of Stone spaces and continuous maps are contravariantly equivalent. Jonsson and Tarski [3] extended this to modal logic and showed a duality between Boolean algebras
1
with additional operators and certain topological spaces with additional operators.
Stone duality embodies completeness theorems, but goes far beyond them. Proofs of completeness typically work by constructing an instance of a model from maximal consistent sets of formulas. Stone duality works in the same way, but gives a correspondence not just for syntactically generated algebras, but for any suitable algebra. This includes both smaller algebras, which could be finite and generate finite structures, or larger algebras, which could be uncountable, thus not syntactically generated. Furthermore, homomorphisms of algebras give rise to maps between the corresponding structures in the opposite direction. Thus mathematical arguments can be transferred in both directions.
Stone-type dualities are now recognized as being ubiquitous in computer science. Plotkin [4] and Smyth [5] emphasized that the duality between state-transformer semantics and predicate-transformer semantics is an instance of a Stone-type duality. Kozen [6] discovered such a duality for probabilistic transition systems. Abramsky [7] identified dualities in domain and concurrency theory. Recently several authors (e.g. [8, 9]) have emphasized the duality between logics and transition systems from a coalgebraic perspective. Mislove et al. [10] found a duality between labeled Markov processes and C*-algebras based on the closely related classical Gelfand duality.
For Markov processes, the natural logic is a simple modal logic in which bounds on probabilities enter into the modalities. This logic can be stripped down to a very spartan core—just the modalities and finite conjunction— and still characterize bisimulation for labeled Markov processes [11, 12]. It is therefore tempting to understand this logic algebraically in the same way that Boolean algebras capture propositional reasoning and the Jonsson– Tarski results give duality for algebras arising from modal logics.
In this paper, we develop a Stone-type duality for continuous-space probabilistic transitions systems and a certain kind of algebra that we have named Aumann algebras. These are Boolean algebras with operators that behave like probabilistic modalities. Recent papers [13–15] have established completeness theorems and finite model theorems for similar logics. Thus it seemed ripe to attempt to capture these logics algebraically and explore duality theory. This is what we do in this paper.
A comparison with related work appears in §7. We note here that we go beyond existing completeness results [13–15] in a number of ways. Follow-
2
ing the pioneering work of Goldblatt [14], the strong completeness theorems use a powerful infinitary axiom scheme called the countably additivity rule in [14]. This rule has an uncountable set of instances. Moreover, for strong completeness, one needs to postulate Lindenbaum’s lemma, which for the aforementioned logics has not been proven. In this paper we use the Rasiowa–Sikorski lemma [16] to finesse Goldblatt’s axiom and prove Lindenbaum’s lemma.
Our key results are:
• a description of a new class of algebras that capture in algebraic form the probabilistic modal logics used for continuous-state Markov processes;
• a version of duality for countable algebras and a certain class of countablygenerated Markov processes; and
• a complete axiomatization that does not involve infinitary axiom schemes with uncountably many instances and avoids postulating Lindenbaum’s lemma as a meta-axioms.
The duality is represented in the diagram below. Here SMP stands for Stone Markov processes and AA for countable Aumann algebras. The formal definitions are given in §§3–4.
A
SMP
AAop
M
A general Markov process gives rise to a countable Aumann algebra but a countable Aumann algebra gives rise to a Stone Markov process. However, starting from a Markov process M, constructing the corresponding Aumann algebra A, then constructing the corresponding Stone Markov process corresponding A, one obtains a Markov process bisimilar to M.
1.1 A Summary for Experts
The duality theorem proved in this paper has some novel features that distinguish it from many others that have appeared in the literature.
3
First and foremost, we have minimized the use of infinitary axioms [17] by using the Rasiowa–Sikorski lemma (whose proof uses the Baire category theorem) in the following way. In going from the algebra to the dual Markov process, we look at ultrafilters that do not respect the infinitary axioms of Aumann algebras. We call these bad ultrafilters. We show that these form a meager set (in the sense of the Baire category theorem) and can be removed without affecting the transition probabilities that we are trying to define. Countability is essential here. In order to show that we do not affect the algebra of clopen sets by doing this, we introduce a distinguished base of clopen sets in the definition of Markov process, which has to satisfy some conditions. We show that this forms an Aumann algebra. We are able to go from a Markov process to an Aumann algebra by using this distinguished base. Morphisms of Markov processes are required to preserve distinguished base elements backwards; that is, if f : M → N and A ∈ AN , then f −1(A) ∈ AM. Thus we get Boolean algebra homomorphisms in the dual for free.
Removing bad points has the effect of destroying compactness of the resulting topological space. We introduce a new concept called saturation that takes the place of compactness. The idea is that a saturated model has all the good ultrafilters. The Stone dual of an Aumann algebra is saturated, because it is constructed that way. However, it is possible to have a Markov process that is unsaturated but still represents the same algebra. For example, we removed bad points and could, in principle, remove a few more; as long as the remaining points are still dense, we have not changed the algebra. One can saturate a model by a process akin to compactification. We explicitly describe how to do this below.
2 Background
Let Q0 = Q ∩ [0, 1] and R+ = R ∩ [0, ∞).
2.1 Measurable Spaces and Measures
In this section we introduce a few concepts and results from measure theory that we will find useful. All of these results are well known. For proofs and related results, we refer the reader to [18] or [19].
Let M be an arbitrary nonempty set.
4
• A field (of sets) over M is a Boolean algebra of subsets of M under the usual set-theoretic Boolean operations.
• A σ-algebra over M is a field of sets over M closed under countable union. The tuple (M, Σ) is called a measurable space and the elements of Σ measurable sets.
Given two measurable spaces (M, Σ) and (N, Ω), a function f : M → N is measurable if f −1(T) ∈ Σ for all T ∈ Ω. We use M → N to denote the family of measurable functions from (M, Σ) to (N, Ω).
If Ω ⊆ 2M, the σ-algebra generated by Ω, denoted Ωσ, is the smallest σ-algebra containing Ω.
A nonnegative real-valued set function µ is finitely additive if µ(A ∪ B) = µ(A) + µ(B) whenever A ∩ B = ∅. We say that µ is countably subadditive if µ( i Ai) ≤ ∑i µ(Ai) for a countable family of measurable sets, and we say that µ is countably additive if µ(∪i Ai) = ∑i µ(Ai) for a countable pairwisedisjoint family of measurable sets.
Finite additivity implies monotonicity and countable additivity implies continuity properties as stated in the theorems below.
Theorem 1. Let F ⊆ 2M be a field of sets. If µ : F → R+ is finitely additive,
then
(i) µ(∅) = 0; (ii) µ is monotone: if A ⊆ B then µ(A) ≤ µ(B); and (iii) if A ⊆ B then µ(B \ A) = µ(B) − µ(A).
The next theorem provides five equivalent properties that a finitely additive function over a field of sets can have.
Theorem 2. Let F ⊆ 2M be a field of sets. Let µ : F → R+ be finitely additive.
The following are equivalent:
(i) µ is countably subadditive: for any countable collection Ai such that
F,
µ( Ai) ≤ ∑ µ(Ai);
i
i
i Ai ∈
5
(ii) µ is countably additive: for any countable collection Ai such that i Ai ∈ F and the Ai are pairwise disjoint,
µ( Ai) = ∑ µ(Ai);
i
i
(iii) µ is ω-continuous from below: for any countable chain A0 ⊆ A1 ⊆ · · · such that i Ai ∈ F ,
µ( Ai) = sup µ(Ai);
i
i
(iv) µ is ω-continuous from above: for any countable chain A0 ⊇ A1 ⊇ · · · such that i Ai ∈ F ,
µ( Ai) = inf µ(Ai);
i
i
(v) µ is ω-continuous from above at ∅: for any countable chain A0 ⊇ A1 ⊇ · · · such that i Ai = ∅, µ( Ai) = 0.
i
A measure on a measurable space M = (M, Σ) is a countably additive
set function µ : Σ → R+. Observe that all measures satisfy the five equiva-
lent properties stated in Theorem 2.
The next theorem is a key tool in our constructions.
Theorem 3 (Theorem 11.3 of [18]). Let F ⊆ 2M be a field of sets. Let µ : F →
R+ be finitely additive and countably subadditive. Then µ extends uniquely to a
measure on F σ.
Proof sketch. This argument is known as the Carathe´odory construction. For B ∈ 2M, define
µ*(B) = inf sup µ( F),
B⊆ C F⊆C C countable F finite
where the infimum ranges over countable F -covers C of B. The map µ* is called an outer measure of µ. One can show that µ* satisfies the following properties:
6
• µ* and µ agree on F ;
• µ is monotone;
• µ is countably subadditive.
Now define a set B to be measurable with respect to µ* if for all A ∈ 2M,
µ*(A) = µ*(A ∩ B) + µ*(A \ B).
One now shows that the set of measurable sets is a σ-algebra, therefore contains F σ, and all properties of measures are satisfied.
A measure is a probability measure if in addition µ(M) = 1. We use ∆(M, Σ) to denote the class of probability measures on (M, Σ). We can view ∆(M, Σ) as a measurable space by considering the σ-algebra generated by the sets {µ ∈ ∆(M, Σ) | µ(S) ≥ r} for S ∈ Σ and r ∈ [0, 1]. This is the least σ-algebra on ∆(M, Σ) such that all maps µ → µ(S) : ∆(M, Σ) → [0, 1] for S ∈ Σ are measurable, where the real interval [0, 1] is endowed with the σ-algebra generated by all rational intervals.
2.2 Analytic Spaces
It turns out that one obtains a much richer theory when one combines measure theory and topology; in fact a standard restriction is to consider so called Polish spaces. We will work with a broader class called analytic spaces. We define these and related concepts here.
Every topological space has a natural σ-algebra associated with it, namely the one generated by the open sets. This is called the Borel algebra of the space, and the measurable sets are called Borel sets.
Recall that a topological space is said to be separable if it contains a countable dense subset and second countable if its topology has a countable base. Second countability implies separability, but not vice versa in general; however, the two concepts coincide for metric spaces.
A Polish space is the topological space underlying a complete separable metric space.
An analytic space is a continuous image of a Polish space. More precisely, if X and Y are Polish spaces and f : X → Y is continuous, then the image f (X) is an analytic space.
7
Remarkably, one does not get a broader class by allowing f to be merely measurable instead of continuous and by taking the image of a Borel subset of X instead of X. That is, the measurable image of any Borel subset of a Polish space is analytic.
Analytic spaces enjoy remarkable properties that were crucial in proving the logical characterization of bisimulation [12, 20]. We note that the completeness theorems proved in [13, 21, 22] were established for Markov processes defined on analytic spaces.
2.3 The Baire Category Theorem
The Baire category theorem is a topological result with important applications in logic. It can be used to prove the Rasiowa–Sikorski lemma [16] that is central for our paper.
A subset D of a topological space X is dense if its closure D is all of X. Equivalently, a dense set is one intersecting every nonempty open set. A set N ⊆ X is nowhere dense if every nonempty open set contains a nonempty open subset disjoint from N. A set is said to be of the first category or meager if it is a countable union of nowhere dense sets. The term “meager” is meant to suggest that these sets are small in a topological sense. A basic fact that we use is that the boundary of an open set is nowhere dense.
A Baire space is one in which the intersection of countably many dense open sets is dense. It follows from these definitions that the complement of a first category set is dense in any Baire space. Baire originally proved that the real line is a Baire space. More generally, every Polish space is Baire and every locally compact Hausdorff space is Baire. For us, the relevant version is the following special case: every compact Hausdorff space is Baire.
Definition 4. Let B be a Boolean algebra and let T ⊆ B such that T has a greatest lower bound T in B. An ultrafilter (maximal filter) U is said to respect T if T ⊆ U implies that T ∈ U.
If T is a family of subsets of B, we say that an ultrafilter U respects T if it respects every member of T .
Theorem 5 (Rasiowa–Sikorski lemma [16]). For any Boolean algebra B and any countable family T of subsets of B, each member of which has a meet in B, and for any nonzero x ∈ B, there exists an ultrafilter in B that contains x and respects T .
8
This lemma was later proved by Tarski in a purely algebraic way. See [14] for a discussion of the role of the Baire category theorem in the proof.
2.4 The Stone Representation Theorem
Starting from a Boolean algebra B, one can construct a topological space called a Stone space as follows. The points of the space are the ultrafilters of B, which are in one-to-one correspondence with the Boolean algebra homo-
morphisms B → 2, where 2 is the two-element Boolean algebra. For each
x ∈ B, let x be the set of ultrafilters containing x. The sets x form a base for the topology. The resulting space is compact, Hausdorff, and totally disconnected. The basic open sets x are both closed and open (clopen); spaces with a base of clopen sets are called zero-dimensional. For compact Hausdorff spaces, the notions of zero-dimensionality and total disconnectedness coincide.
A Stone space is defined to be a zero-dimensional compact Hausdorff space. The family of clopen sets of a Stone space form a Boolean algebra. One can go back and forth from Boolean algebras to Stone spaces; in both cases one obtains an object isomorphic to the starting object. Jonsson and Tarski [3] extended this to Boolean algebras with additional operators, essentially algebraic versions of modal operators, and corresponding topological spaces equipped with suitable closure operators.
The correspondence lifts to a contravariant equivalence between the category of Boolean algebras and Boolean algebra homomorphisms and the category of Stone spaces and continuous maps. Many other dualities in mathematics are recognized as being of this type [2].
C
SS
BAop
U
3 Markov Processes and Markovian Logic
3.1 Markov Processes
Markov processes (MPs) are models of probabilistic systems with a continuous state space and probabilistic transitions [12, 20, 23]. In earlier papers,
9
they were called labeled Markov processes to emphasize the fact that there were multiple possible actions, but here we will suppress the labels, as they do not contribute any relevant structure for our results.
Definition 6 (Markov process). Given an analytic space (M, Σ), a Markov process is a measurable mapping θ ∈ M → ∆(M, Σ) .
In what follows we identify a Markov process with the tuple M = (M, Σ, θ); M is the support set, denoted by supp(M), and θ is the transition function. For m ∈ M, θ(m) : Σ → [0, 1] is a probability measure on the state space (M, Σ). For N ∈ Σ, the value θ(m)(N) ∈ [0, 1] represents the probability of a transition from m to a state in N.
The condition that θ is a measurable function M → ∆(M, Σ) is equivalent to the condition that for fixed N ∈ Σ, the function m → θ(m)(N) is a measurable function M → [0, 1] (see e.g. Proposition 2.9 of [23]).
3.2 Markovian Logic
Markovian logic (ML) is a multi-modal logic for semantics based on MPs [13, 15, 21, 24–28]. In addition to the Boolean operators, this logic is equipped
with probabilistic modal operators Lr for r ∈ Q0 that bound the probabilities
of transitions. Intuitively, the formula Lr ϕ is satisfied by m ∈ M whenever the probability of a transition from m to a state satisfying ϕ is at least r.
Definition 7 (Syntax). The formulas of L are defined, for a set P of atomic propositions, by the grammar
ϕ ::= p | ⊥ | ϕ → ϕ | Lr ϕ
where p can be any element of P and r any element of Q0.
The Boolean operators ∨, ∧, ¬, and
usual. For r1, . . . , rn ∈ Q0 and ϕ ∈ L, let
are defined from → and ⊥ as
Lr1···rn ϕ = Lr1 · · · Lrn ϕ.
The Markovian semantics for L is defined for a given MP M = (M, Σ, θ) and m ∈ M, on top of an interpretation function i : M → 2P , as follows.
• M, m, i p if p ∈ i(m),
10
Dexter Kozen1
Kim G. Larsen2 Radu Mardare2 Prakash Panangaden3
1Computer Science Department, Cornell University, Ithaca, New York, USA 2Department of Computer Science, University of Aalborg, Aalborg, Denmark
3School of Computer Science, McGill University, Montreal, Canada
March 14, 2013
Abstract
We define Aumann algebras, an algebraic analog of probabilistic modal logic. An Aumann algebra consists of a Boolean algebra with operators modeling probabilistic transitions. We prove that countable Aumann algebras and countably-generated continuous-space Markov processes are dual in the sense of Stone. Our results subsume existing results on completeness of probabilistic modal logics for Markov processes.
1 Introduction
The Stone representation theorem [1] is a recognized landmarks of mathematics. The theorem states that every (abstract) Boolean algebra is isomorphic to a Boolean algebra of sets. In fact, Stone proved much more: that Boolean algebras are dual to a certain category of topological spaces known as Stone spaces. See Johnstone [2] for a detailed and eloquent introduction to this theorem and its ramifications, as well as an account of several other related dualities, like Gelfand duality, that appear in mathematics.
Formally, Stone duality states that the category of Boolean algebras and Boolean algebra homomorphisms and the category of Stone spaces and continuous maps are contravariantly equivalent. Jonsson and Tarski [3] extended this to modal logic and showed a duality between Boolean algebras
1
with additional operators and certain topological spaces with additional operators.
Stone duality embodies completeness theorems, but goes far beyond them. Proofs of completeness typically work by constructing an instance of a model from maximal consistent sets of formulas. Stone duality works in the same way, but gives a correspondence not just for syntactically generated algebras, but for any suitable algebra. This includes both smaller algebras, which could be finite and generate finite structures, or larger algebras, which could be uncountable, thus not syntactically generated. Furthermore, homomorphisms of algebras give rise to maps between the corresponding structures in the opposite direction. Thus mathematical arguments can be transferred in both directions.
Stone-type dualities are now recognized as being ubiquitous in computer science. Plotkin [4] and Smyth [5] emphasized that the duality between state-transformer semantics and predicate-transformer semantics is an instance of a Stone-type duality. Kozen [6] discovered such a duality for probabilistic transition systems. Abramsky [7] identified dualities in domain and concurrency theory. Recently several authors (e.g. [8, 9]) have emphasized the duality between logics and transition systems from a coalgebraic perspective. Mislove et al. [10] found a duality between labeled Markov processes and C*-algebras based on the closely related classical Gelfand duality.
For Markov processes, the natural logic is a simple modal logic in which bounds on probabilities enter into the modalities. This logic can be stripped down to a very spartan core—just the modalities and finite conjunction— and still characterize bisimulation for labeled Markov processes [11, 12]. It is therefore tempting to understand this logic algebraically in the same way that Boolean algebras capture propositional reasoning and the Jonsson– Tarski results give duality for algebras arising from modal logics.
In this paper, we develop a Stone-type duality for continuous-space probabilistic transitions systems and a certain kind of algebra that we have named Aumann algebras. These are Boolean algebras with operators that behave like probabilistic modalities. Recent papers [13–15] have established completeness theorems and finite model theorems for similar logics. Thus it seemed ripe to attempt to capture these logics algebraically and explore duality theory. This is what we do in this paper.
A comparison with related work appears in §7. We note here that we go beyond existing completeness results [13–15] in a number of ways. Follow-
2
ing the pioneering work of Goldblatt [14], the strong completeness theorems use a powerful infinitary axiom scheme called the countably additivity rule in [14]. This rule has an uncountable set of instances. Moreover, for strong completeness, one needs to postulate Lindenbaum’s lemma, which for the aforementioned logics has not been proven. In this paper we use the Rasiowa–Sikorski lemma [16] to finesse Goldblatt’s axiom and prove Lindenbaum’s lemma.
Our key results are:
• a description of a new class of algebras that capture in algebraic form the probabilistic modal logics used for continuous-state Markov processes;
• a version of duality for countable algebras and a certain class of countablygenerated Markov processes; and
• a complete axiomatization that does not involve infinitary axiom schemes with uncountably many instances and avoids postulating Lindenbaum’s lemma as a meta-axioms.
The duality is represented in the diagram below. Here SMP stands for Stone Markov processes and AA for countable Aumann algebras. The formal definitions are given in §§3–4.
A
SMP
AAop
M
A general Markov process gives rise to a countable Aumann algebra but a countable Aumann algebra gives rise to a Stone Markov process. However, starting from a Markov process M, constructing the corresponding Aumann algebra A, then constructing the corresponding Stone Markov process corresponding A, one obtains a Markov process bisimilar to M.
1.1 A Summary for Experts
The duality theorem proved in this paper has some novel features that distinguish it from many others that have appeared in the literature.
3
First and foremost, we have minimized the use of infinitary axioms [17] by using the Rasiowa–Sikorski lemma (whose proof uses the Baire category theorem) in the following way. In going from the algebra to the dual Markov process, we look at ultrafilters that do not respect the infinitary axioms of Aumann algebras. We call these bad ultrafilters. We show that these form a meager set (in the sense of the Baire category theorem) and can be removed without affecting the transition probabilities that we are trying to define. Countability is essential here. In order to show that we do not affect the algebra of clopen sets by doing this, we introduce a distinguished base of clopen sets in the definition of Markov process, which has to satisfy some conditions. We show that this forms an Aumann algebra. We are able to go from a Markov process to an Aumann algebra by using this distinguished base. Morphisms of Markov processes are required to preserve distinguished base elements backwards; that is, if f : M → N and A ∈ AN , then f −1(A) ∈ AM. Thus we get Boolean algebra homomorphisms in the dual for free.
Removing bad points has the effect of destroying compactness of the resulting topological space. We introduce a new concept called saturation that takes the place of compactness. The idea is that a saturated model has all the good ultrafilters. The Stone dual of an Aumann algebra is saturated, because it is constructed that way. However, it is possible to have a Markov process that is unsaturated but still represents the same algebra. For example, we removed bad points and could, in principle, remove a few more; as long as the remaining points are still dense, we have not changed the algebra. One can saturate a model by a process akin to compactification. We explicitly describe how to do this below.
2 Background
Let Q0 = Q ∩ [0, 1] and R+ = R ∩ [0, ∞).
2.1 Measurable Spaces and Measures
In this section we introduce a few concepts and results from measure theory that we will find useful. All of these results are well known. For proofs and related results, we refer the reader to [18] or [19].
Let M be an arbitrary nonempty set.
4
• A field (of sets) over M is a Boolean algebra of subsets of M under the usual set-theoretic Boolean operations.
• A σ-algebra over M is a field of sets over M closed under countable union. The tuple (M, Σ) is called a measurable space and the elements of Σ measurable sets.
Given two measurable spaces (M, Σ) and (N, Ω), a function f : M → N is measurable if f −1(T) ∈ Σ for all T ∈ Ω. We use M → N to denote the family of measurable functions from (M, Σ) to (N, Ω).
If Ω ⊆ 2M, the σ-algebra generated by Ω, denoted Ωσ, is the smallest σ-algebra containing Ω.
A nonnegative real-valued set function µ is finitely additive if µ(A ∪ B) = µ(A) + µ(B) whenever A ∩ B = ∅. We say that µ is countably subadditive if µ( i Ai) ≤ ∑i µ(Ai) for a countable family of measurable sets, and we say that µ is countably additive if µ(∪i Ai) = ∑i µ(Ai) for a countable pairwisedisjoint family of measurable sets.
Finite additivity implies monotonicity and countable additivity implies continuity properties as stated in the theorems below.
Theorem 1. Let F ⊆ 2M be a field of sets. If µ : F → R+ is finitely additive,
then
(i) µ(∅) = 0; (ii) µ is monotone: if A ⊆ B then µ(A) ≤ µ(B); and (iii) if A ⊆ B then µ(B \ A) = µ(B) − µ(A).
The next theorem provides five equivalent properties that a finitely additive function over a field of sets can have.
Theorem 2. Let F ⊆ 2M be a field of sets. Let µ : F → R+ be finitely additive.
The following are equivalent:
(i) µ is countably subadditive: for any countable collection Ai such that
F,
µ( Ai) ≤ ∑ µ(Ai);
i
i
i Ai ∈
5
(ii) µ is countably additive: for any countable collection Ai such that i Ai ∈ F and the Ai are pairwise disjoint,
µ( Ai) = ∑ µ(Ai);
i
i
(iii) µ is ω-continuous from below: for any countable chain A0 ⊆ A1 ⊆ · · · such that i Ai ∈ F ,
µ( Ai) = sup µ(Ai);
i
i
(iv) µ is ω-continuous from above: for any countable chain A0 ⊇ A1 ⊇ · · · such that i Ai ∈ F ,
µ( Ai) = inf µ(Ai);
i
i
(v) µ is ω-continuous from above at ∅: for any countable chain A0 ⊇ A1 ⊇ · · · such that i Ai = ∅, µ( Ai) = 0.
i
A measure on a measurable space M = (M, Σ) is a countably additive
set function µ : Σ → R+. Observe that all measures satisfy the five equiva-
lent properties stated in Theorem 2.
The next theorem is a key tool in our constructions.
Theorem 3 (Theorem 11.3 of [18]). Let F ⊆ 2M be a field of sets. Let µ : F →
R+ be finitely additive and countably subadditive. Then µ extends uniquely to a
measure on F σ.
Proof sketch. This argument is known as the Carathe´odory construction. For B ∈ 2M, define
µ*(B) = inf sup µ( F),
B⊆ C F⊆C C countable F finite
where the infimum ranges over countable F -covers C of B. The map µ* is called an outer measure of µ. One can show that µ* satisfies the following properties:
6
• µ* and µ agree on F ;
• µ is monotone;
• µ is countably subadditive.
Now define a set B to be measurable with respect to µ* if for all A ∈ 2M,
µ*(A) = µ*(A ∩ B) + µ*(A \ B).
One now shows that the set of measurable sets is a σ-algebra, therefore contains F σ, and all properties of measures are satisfied.
A measure is a probability measure if in addition µ(M) = 1. We use ∆(M, Σ) to denote the class of probability measures on (M, Σ). We can view ∆(M, Σ) as a measurable space by considering the σ-algebra generated by the sets {µ ∈ ∆(M, Σ) | µ(S) ≥ r} for S ∈ Σ and r ∈ [0, 1]. This is the least σ-algebra on ∆(M, Σ) such that all maps µ → µ(S) : ∆(M, Σ) → [0, 1] for S ∈ Σ are measurable, where the real interval [0, 1] is endowed with the σ-algebra generated by all rational intervals.
2.2 Analytic Spaces
It turns out that one obtains a much richer theory when one combines measure theory and topology; in fact a standard restriction is to consider so called Polish spaces. We will work with a broader class called analytic spaces. We define these and related concepts here.
Every topological space has a natural σ-algebra associated with it, namely the one generated by the open sets. This is called the Borel algebra of the space, and the measurable sets are called Borel sets.
Recall that a topological space is said to be separable if it contains a countable dense subset and second countable if its topology has a countable base. Second countability implies separability, but not vice versa in general; however, the two concepts coincide for metric spaces.
A Polish space is the topological space underlying a complete separable metric space.
An analytic space is a continuous image of a Polish space. More precisely, if X and Y are Polish spaces and f : X → Y is continuous, then the image f (X) is an analytic space.
7
Remarkably, one does not get a broader class by allowing f to be merely measurable instead of continuous and by taking the image of a Borel subset of X instead of X. That is, the measurable image of any Borel subset of a Polish space is analytic.
Analytic spaces enjoy remarkable properties that were crucial in proving the logical characterization of bisimulation [12, 20]. We note that the completeness theorems proved in [13, 21, 22] were established for Markov processes defined on analytic spaces.
2.3 The Baire Category Theorem
The Baire category theorem is a topological result with important applications in logic. It can be used to prove the Rasiowa–Sikorski lemma [16] that is central for our paper.
A subset D of a topological space X is dense if its closure D is all of X. Equivalently, a dense set is one intersecting every nonempty open set. A set N ⊆ X is nowhere dense if every nonempty open set contains a nonempty open subset disjoint from N. A set is said to be of the first category or meager if it is a countable union of nowhere dense sets. The term “meager” is meant to suggest that these sets are small in a topological sense. A basic fact that we use is that the boundary of an open set is nowhere dense.
A Baire space is one in which the intersection of countably many dense open sets is dense. It follows from these definitions that the complement of a first category set is dense in any Baire space. Baire originally proved that the real line is a Baire space. More generally, every Polish space is Baire and every locally compact Hausdorff space is Baire. For us, the relevant version is the following special case: every compact Hausdorff space is Baire.
Definition 4. Let B be a Boolean algebra and let T ⊆ B such that T has a greatest lower bound T in B. An ultrafilter (maximal filter) U is said to respect T if T ⊆ U implies that T ∈ U.
If T is a family of subsets of B, we say that an ultrafilter U respects T if it respects every member of T .
Theorem 5 (Rasiowa–Sikorski lemma [16]). For any Boolean algebra B and any countable family T of subsets of B, each member of which has a meet in B, and for any nonzero x ∈ B, there exists an ultrafilter in B that contains x and respects T .
8
This lemma was later proved by Tarski in a purely algebraic way. See [14] for a discussion of the role of the Baire category theorem in the proof.
2.4 The Stone Representation Theorem
Starting from a Boolean algebra B, one can construct a topological space called a Stone space as follows. The points of the space are the ultrafilters of B, which are in one-to-one correspondence with the Boolean algebra homo-
morphisms B → 2, where 2 is the two-element Boolean algebra. For each
x ∈ B, let x be the set of ultrafilters containing x. The sets x form a base for the topology. The resulting space is compact, Hausdorff, and totally disconnected. The basic open sets x are both closed and open (clopen); spaces with a base of clopen sets are called zero-dimensional. For compact Hausdorff spaces, the notions of zero-dimensionality and total disconnectedness coincide.
A Stone space is defined to be a zero-dimensional compact Hausdorff space. The family of clopen sets of a Stone space form a Boolean algebra. One can go back and forth from Boolean algebras to Stone spaces; in both cases one obtains an object isomorphic to the starting object. Jonsson and Tarski [3] extended this to Boolean algebras with additional operators, essentially algebraic versions of modal operators, and corresponding topological spaces equipped with suitable closure operators.
The correspondence lifts to a contravariant equivalence between the category of Boolean algebras and Boolean algebra homomorphisms and the category of Stone spaces and continuous maps. Many other dualities in mathematics are recognized as being of this type [2].
C
SS
BAop
U
3 Markov Processes and Markovian Logic
3.1 Markov Processes
Markov processes (MPs) are models of probabilistic systems with a continuous state space and probabilistic transitions [12, 20, 23]. In earlier papers,
9
they were called labeled Markov processes to emphasize the fact that there were multiple possible actions, but here we will suppress the labels, as they do not contribute any relevant structure for our results.
Definition 6 (Markov process). Given an analytic space (M, Σ), a Markov process is a measurable mapping θ ∈ M → ∆(M, Σ) .
In what follows we identify a Markov process with the tuple M = (M, Σ, θ); M is the support set, denoted by supp(M), and θ is the transition function. For m ∈ M, θ(m) : Σ → [0, 1] is a probability measure on the state space (M, Σ). For N ∈ Σ, the value θ(m)(N) ∈ [0, 1] represents the probability of a transition from m to a state in N.
The condition that θ is a measurable function M → ∆(M, Σ) is equivalent to the condition that for fixed N ∈ Σ, the function m → θ(m)(N) is a measurable function M → [0, 1] (see e.g. Proposition 2.9 of [23]).
3.2 Markovian Logic
Markovian logic (ML) is a multi-modal logic for semantics based on MPs [13, 15, 21, 24–28]. In addition to the Boolean operators, this logic is equipped
with probabilistic modal operators Lr for r ∈ Q0 that bound the probabilities
of transitions. Intuitively, the formula Lr ϕ is satisfied by m ∈ M whenever the probability of a transition from m to a state satisfying ϕ is at least r.
Definition 7 (Syntax). The formulas of L are defined, for a set P of atomic propositions, by the grammar
ϕ ::= p | ⊥ | ϕ → ϕ | Lr ϕ
where p can be any element of P and r any element of Q0.
The Boolean operators ∨, ∧, ¬, and
usual. For r1, . . . , rn ∈ Q0 and ϕ ∈ L, let
are defined from → and ⊥ as
Lr1···rn ϕ = Lr1 · · · Lrn ϕ.
The Markovian semantics for L is defined for a given MP M = (M, Σ, θ) and m ∈ M, on top of an interpretation function i : M → 2P , as follows.
• M, m, i p if p ∈ i(m),
10