Abstraction, Refinement and Proof for Probabilistic Systems / Edition 1

by Annabelle McIver, Charles Carroll Morgan

Overview

Probabilistic guarded commands and their refinement logic.- to pGCL: Its logic and its model.- Probabilistic loops: Invariants and variants.- Case studies in termination: Choice coordination, the dining philosophers, and the random walk.- Probabilistic data refinement: The steam boiler.- Semantic structures.- Theory for the demonic model.- The geometry of probabilistic programs.- Proved rules for probabilistic loops.- Infinite state spaces, angelic choice and the transformer hierarchy.- Advanced topics: Quantitative modal logic and game interpretations.- Quantitative temporal logic: An introduction.- The quantitative algebra of qTL.- The quantitative modal ?-calculus, and gambling games.

Product Details

ISBN-13:	9781441923127
Publisher:	Springer New York
Publication date:	11/19/2010
Series:	Monographs in Computer Science
Edition description:	Softcover reprint of hardcover 1st ed. 2005
Pages:	388
Product dimensions:	6.10(w) x 9.25(h) x 0.36(d)

Table of Contents

Probabilistic guarded commands and their refinement logic.- to pGCL: Its logic and its model.- Probabilistic loops: Invariants and variants.- Case studies in termination: Choice coordination, the dining philosophers, and the random walk.- Probabilistic data refinement: The steam boiler.- Semantic structures.- Theory for the demonic model.- The geometry of probabilistic programs.- Proved rules for probabilistic loops.- Infinite state spaces, angelic choice and the transformer hierarchy.- Advanced topics: Quantitative modal logic and game interpretations.- Quantitative temporal logic: An introduction.- The quantitative algebra of qTL.- The quantitative modal—-calculus, and gambling games.