Abstraction, Refinement and Proof for Probabilistic Systems

تکنیک‌های احتمالاتی به طور فزاینده‌ای در برنامه‌ها و سیستم‌های رایانه‌ای به کار می‌روند، زیرا می‌توانند کارایی را در الگوریتم‌های متوالی افزایش دهند، برنامه‌های کاربردی توزیع غیرعملکردی را فعال کنند و به طور کلی امکان کمی کردن ریسک و ایمنی را فراهم کنند. این امر باعث می‌شود مدل‌های عملیاتی نحوه کار آنها و منطق استدلال درباره آنها بسیار مهم باشد.

انتزاع، اصلاح و اثبات برای سیستم‌های احتمالی یک رویکرد دقیق برای مدل‌سازی و استدلال در مورد سیستم‌های رایانه‌ای که احتمال را در خود دارند ارائه می‌کند. پایه‌های آن در منطق برنامه‌های ترتیبی بولی سنتی نهفته است - اما بسط آن به قضاوت‌های عددی و نه صرفاً درست یا غلط، آن را بسیار فراتر می‌برد، به حوزه‌هایی مانند الگوریتم‌های تصادفی، تحمل خطا، و در سیستم‌های توزیع‌شده، تقارن تقریباً معین. شکستن ارائه با سبک آشنای توسعه برنامه \"ادعای\" آغاز می شود و با افزایش تخصص ادامه می یابد: بخش اول به منطق برنامه احتمالی، از جمله بسیاری از مثال ها و مطالعات موردی می پردازد. بخش دوم معانی دقیق را مشخص می کند. و قسمت سوم رویکردی را به مطالب پیشرفته در مورد محاسبات زمانی و بازی های دو نفره اعمال می کند.

موضوعات و ویژگی ها:

* یک معناشناسی کلی برای هر دو ارائه می کند. احتمال و عدم قطعیت اهریمنی، از جمله انتزاع و پالایش داده

* خوانندگان را با آخرین تحقیقات ریاضی در رسمی سازی دقیق الگوریتم های تصادفی (احتمالی) آشنا می کند * مراحل لازم برای ساخت را با مثال نشان می دهد. مدل مفهومی برنامه‌ریزی احتمالی \"پارادایم\"

* نتایج یک تمرین تحقیقاتی بزرگ و یکپارچه (10 سال و ادامه) را در حوزه پیشرو منطق برنامه \"کمی\" در نظر می‌گیرد. P>

* شامل خلاصه های مفید پایان فصل، یک نمایه جامع، و یک ضمیمه است که رویکردهای جایگزین را بررسی می کند

این تک نگاری قابل دسترس و متمرکز ، که توسط مقامات بین المللی در مورد برنامه ریزی احتمالی نوشته شده است، یک مبحث اساسی برای برنامه نویسی مدرن و توسعه سیستم ها ایجاد می کند. محققان، دانشمندان کامپیوتر، و دانش‌آموختگان و فارغ‌التحصیلان پیشرفته‌ای که برنامه‌نویسی یا سیستم‌های احتمالی را مطالعه می‌کنند، این کار را یک متن منبع معتبر و ضروری می‌دانند.

Probabilistic techniques are increasingly being employed in computer programs and systems because they can increase efficiency in sequential algorithms, enable otherwise nonfunctional distribution applications, and allow quantification of risk and safety in general. This makes operational models of how they work, and logics for reasoning about them, extremely important.

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. The presentation begins with the familiar "assertional" style of program development and continues with increasing specialization: Part I treats probabilistic program logic, including many examples and case studies; Part II sets out the detailed semantics; and Part III applies the approach to advanced material on temporal calculi and two-player games.

Topics and features:

* Presents a general semantics for both probability and demonic nondeterminism, including abstraction and data refinement

* Introduces readers to the latest mathematical research in rigorous formalization of randomized (probabilistic) algorithms * Illustrates by example the steps necessary for building a conceptual model of probabilistic programming "paradigm"

* Considers results of a large and integrated research exercise (10 years and continuing) in the leading-edge area of "quantitative" program logics

* Includes helpful chapter-ending summaries, a comprehensive index, and an appendix that explores alternative approaches

This accessible, focused monograph, written by international authorities on probabilistic programming, develops an essential foundation topic for modern programming and systems development. Researchers, computer scientists, and advanced undergraduates and graduates studying programming or probabilistic systems will find the work an authoritative and essential resource text.