Labelled Markov processes

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. 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 Labelled Markov processes are probabilistic versions of labelled transition systems with continuous state spaces. The 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. Labelled Markov processes are probabilistic versions of labelled transition systems with continuous state spaces. The 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