Contents -- Preface -- 1. Introduction -- 1.1 Preliminary Remarks -- 1.2 Elementary Discrete Probability Theory -- 1.3 The Need for Measure Theory -- 1.4 The Laws of Large Numbers -- 1.5 Borel-Cantelli Lemmas -- 2. Measure Theory -- 2.1 Measurable Spaces -- 2.2 Measurable Functions -- 2.3 Metric Spaces and Properties of Measurable Functions -- 2.4 Measurable Spaces of Sequences -- 2.5 Measures -- 2.6 Lebesgue Measure -- 2.7 Nonmeasurable Sets -- 2.8 Exercises -- 3. Integration -- 3.1 The Definition of Integration -- 3.2 Properties of the Integral -- 3.3 Riemann Integrals -- 3.4 Multiple Integrals -- 3.5 Exercises -- 4. The Radon-Nikodym Theorem -- 4.1 Set Functions -- 4.2 Decomposition Theorems -- 4.3 Absolute Continuity -- 4.4 Exercises -- 5. A Category of Stochastic Relations -- 5.1 The Category SRel -- 5.2 Probability Monads -- 5.3 The Structure of SRel -- 5.3.1 Partially additive structure -- 5.4 Kozen Semantics and Duality -- 5.4.1 While loops in a probabilistic framework -- 5.5 Exercises -- 6. Probability Theory on Continuous Spaces -- 6.1 Probability Spaces -- 6.2 Random Variables -- 6.3 Conditional Probability -- 6.4 Regular Conditional Probability -- 6.5 Stochastic Processes and Markov Processes -- 7. Bisimulation for Labelled Markov Processes -- 7.1 Ordinary Bisimulation -- 7.2 Probabilistic Bisimulation for Discrete Systems -- 7.3 Two Examples of Continuous-State Processes -- 7.4 The De.nition of Labelled Markov Processes -- 7.5 Basic Facts About Analytic Spaces -- 7.6 Bisimulation for Labelled Markov Processes -- 7.7 A Logical Characterisation of Bisimulation -- 8. Metrics for Labelled Markov Processes -- 8.1 From Bisimulation to aMetric -- 8.2 A Real-Valued Logic on Labelled Markov Processes -- 8.3 Metrics on Processes -- 8.4 Metric Reasoning for Process Algebras -- 8.5 Perturbation -- 8.6 The AsymptoticMetric.

8.7 Behavioural Properties of the Metric -- 8.8 The Pseudometric as a Maximum Fixed Point -- 9. Approximating Labelled Markov Processes -- 9.1 An Explicit Approximation Construction -- 9.1.1 Finite-state approximation: .rst attempt -- 9.2 DealingWith Loops -- 9.3 Adapting the Approximation to Formulas -- 10. Approximating the Approximation -- 11. A Domain of Labelled Markov Processes -- 11.1 Background on Domain Theory -- 11.1.1 Basic de.nitions and results -- 11.1.2 Valuations and the probabilistic powerdomain -- 11.1.3 The Lawson topology -- 11.2 The Domain Proc -- 11.3 L as the Logic of Proc -- 11.4 Relating Proc and LMP -- 11.4.1 From Proc to labelled Markov processes -- 11.4.2 Embedding labelled Markov processes into Proc -- 12. Real-Time and Continuous Stochastic Logic -- 12.1 Background -- 12.2 Spaces of Paths in a CTMP -- 12.3 The Logic CSL -- 12.4 A General Technique for Relating Bisimulation and Logic -- 12.5 Bisimilarity and CSL -- 13. Related Work -- 13.1 Mathematical Foundations -- 13.2 Metrics -- 13.3 Nondeterminism -- 13.4 Testing -- 13.5 Weak Bisimulation -- 13.6 Approximation -- 13.7 Model Checking -- Bibliography -- Index.