Labelled Markov processes are probabilistic versions of labelled transition systems with continuous state spaces. This book covers basic probability and measure theory on continuous state spaces and then develops the theory of LMPs. The main topics covered are bisimulation, the logical characterization of bisimulation, metrics and approximation theory. An unusual feature of the book is the connection made with categorical and domain theoretic concepts.
Author(s): Prakash Panangaden
Publisher: Imperial College Press
Year: 2009
Language: English
Pages: 212
Contents......Page 10
Preface......Page 8
1.1 Preliminary Remarks......Page 14
1.2 Elementary Discrete Probability Theory......Page 16
1.3 The Need for Measure Theory......Page 19
1.4 The Laws of Large Numbers......Page 21
1.5 Borel-Cantelli Lemmas......Page 24
2.1 Measurable Spaces......Page 26
2.3 Metric Spaces and Properties of Measurable Functions......Page 32
2.4 Measurable Spaces of Sequences......Page 35
2.5 Measures......Page 36
2.6 Lebesgue Measure......Page 42
2.7 Nonmeasurable Sets......Page 48
2.8 Exercises......Page 49
3. Integration......Page 52
3.1 The Definition of Integration......Page 53
3.2 Properties of the Integral......Page 56
3.3 Riemann Integrals......Page 59
3.4 Multiple Integrals......Page 62
3.5 Exercises......Page 66
4. The Radon-Nikodym Theorem......Page 68
4.1 Set Functions......Page 69
4.2 Decomposition Theorems......Page 70
4.3 Absolute Continuity......Page 72
4.4 Exercises......Page 75
5.1 The Category SRel......Page 76
5.2 Probability Monads......Page 78
5.3 The Structure of SRel......Page 81
5.3.1 Partially additive structure......Page 82
5.4 Kozen Semantics and Duality......Page 86
5.4.1 While loops in a probabilistic framework......Page 87
5.5 Exercises......Page 89
6.1 Probability Spaces......Page 90
6.2 Random Variables......Page 91
6.3 Conditional Probability......Page 93
6.4 Regular Conditional Probability......Page 97
6.5 Stochastic Processes and Markov Processes......Page 100
7. Bisimulation for Labelled Markov Processes......Page 102
7.1 Ordinary Bisimulation......Page 104
7.2 Probabilistic Bisimulation for Discrete Systems......Page 105
7.3 Two Examples of Continuous-State Processes......Page 106
7.4 The De.nition of Labelled Markov Processes......Page 107
7.5 Basic Facts About Analytic Spaces......Page 109
7.6 Bisimulation for Labelled Markov Processes......Page 111
7.7 A Logical Characterisation of Bisimulation......Page 114
8. Metrics for Labelled Markov Processes......Page 120
8.1 From Bisimulation to aMetric......Page 121
8.2 A Real-Valued Logic on Labelled Markov Processes......Page 123
8.3 Metrics on Processes......Page 129
8.4 Metric Reasoning for Process Algebras......Page 131
8.5 Perturbation......Page 135
8.6 The AsymptoticMetric......Page 137
8.8 The Pseudometric as a Maximum Fixed Point......Page 139
9. Approximating Labelled Markov Processes......Page 146
9.1.1 Finite-state approximation: .rst attempt......Page 147
9.2 DealingWith Loops......Page 152
9.3 Adapting the Approximation to Formulas......Page 158
10. Approximating the Approximation......Page 160
11.1 Background on Domain Theory......Page 166
11.1.1 Basic de.nitions and results......Page 167
11.1.2 Valuations and the probabilistic powerdomain......Page 168
11.1.3 The Lawson topology......Page 169
11.2 The Domain Proc......Page 172
11.3 L as the Logic of Proc......Page 174
11.4.1 From Proc to labelled Markov processes......Page 176
11.4.2 Embedding labelled Markov processes into Proc......Page 177
12. Real-Time and Continuous Stochastic Logic......Page 180
12.1 Background......Page 181
12.2 Spaces of Paths in a CTMP......Page 182
12.3 The Logic CSL......Page 185
12.4 A General Technique for Relating Bisimulation and Logic......Page 188
12.5 Bisimilarity and CSL......Page 190
13.1 Mathematical Foundations......Page 194
13.3 Nondeterminism......Page 197
13.5 Weak Bisimulation......Page 199
13.6 Approximation......Page 200
13.7 Model Checking......Page 201
Bibliography......Page 202
Index......Page 210
