Abstraction, Refinement and Proof for Probabilistic Systems

Part I. Probabilistic guarded commands and their refinement logic

1. Introduction to pGCL: Its logic and its model

2. Probabilistic loops: Invariants and variants

3. Case studies in termination: Choice coordination, the dining philosophers, and the random walk

4. Probabilistic data refinement: The steam boiler

Part II. Semantic structures

5. Theory for the demonic model

6. The geometry of probabilistic programs

7. Proved rules for probabilistic loops

8. Infinite state spaces, angelic choice and the transformer hierarchy

Part III. Advanced topics: Quantitative modal logic and game interpretations

9. Quantitative temporal logic: An introduction

10. The quantitative algebra of qTL

11. The quantitative modal µ-calculus, and gambling games

DRM-restrictions

Printing: not available
Clipboard copying: not available

Keywords: COMPUTERS / Computer Science COM014000