Abstraction, Refinement and Proof for Probabilistic Systems

The book is a focused survey on probabilistic program semantics, conceived to tell a coherent story with a uniform notation. It is grouped into three themes: Part I is for 'users' of the techniques who will be developing actual programs; Part II gives mathematical foundations intended for those studying exactly how it was done and how to build semantic structures/models in their own work; and Part III describes a very 'hot' research direction, temporal logic and model checking. Topics and features: - introduces readers to very up-to-date research in the mathematics of rigorous development of randomized (probabilistic) algorithms - illustrates by example the typical steps necessary in computer science to build a mathematical model of any programming paradigm - presents results of a large and integrated body of research in the area of 'quantitative' program logics An advanced research survey monograph, integrating three major topic areas: random/probabilistic algorithms, assertion-based program reasoning, and refinement programming models. Essential foundation topic for modern sequential programming methodology.