Research Catalog

Title

Abstraction, refinement and proof for probabilistic systems / Annabelle McIver, Carroll Morgan.

Author

McIver, Annabelle.

Publication

New York : Springer, [2005], ©2005.

Items in the Library & Off-site

Holdings

Details

Additional Authors

Morgan, Carroll, 1952-

Description

xix, 383 pages : illustrations; 24 cm.

Summary

"Abstraction, Refinement and Proof for Probabilistic Systems presents a rigorous approach to modeling and reasoning about computer systems that incorporate probability. Its foundations lie in traditional Boolean sequential-program logic - but its extension to numeric rather than merely true-or-false judgments takes it much further, into areas such as randomized algorithms, fault tolerance and, in distributed systems, almost-certain symmetry breaking."--BOOK JACKET.

Series Statement

Monographs in computer science

Uniform Title

Monographs in computer science.

Subjects

• Systems engineering
• Probabilities
• Probabilités
• Engineering mathematics
• Mathématiques de l'ingénieur
• Ingénierie des systèmes

Bibliography (note)

• Includes bibliographical references (p. [345]-355) and indexes.

Contents

Pt. I. Probabilistic guarded commands -- 1. Introduction to pGCL -- 2. Probabilistic loops : invariants and variants -- 3. Case studies in termination -- 4. Probabilistic data refinement : the steam boiler -- Pt. II. Semantic structures -- 5. Theory for the demonic model -- 6. The geometry of probabilistic programs -- 7. Proved rules for probabilistic loops -- 8. The transformer hierarchy -- Pt. III. Advanced topics -- 9. Quantitative temporal logic : an introduction -- 10. The quantitative algebra of qTL -- 11. The quantitative modal [mu]-calculus qM[mu], and games -- Pt. IV. Appendices, bibliography and indexes.

ISBN

0387401156 (alk. paper)

LCCN

2004057839

OCLC

• ocm56615822
• SCSB-5166043

Owning Institutions

Columbia University Libraries