An expectation transformer approach to predicate abstraction and data independence for probabilistic programs

Ukachukwu Ndukwu, Annabelle Kate McIver

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

6 Citations (Scopus)

Abstract

In this paper we revisit the well-known technique of predicate abstraction to characterise performance attributes of system models incorporating probability. We recast the theory using expectation transformers, and identify transformer properties which correspond to abstractions that yield nevertheless exact bound on the performance of infinite state probabilistic systems. In addition, we extend the developed technique to the special case of "data independent programs incorporating probability. Finally, we demonstrate the subtleness of the extended technique by using the PRISM model checking tool to analyse an infinite state protocol, obtaining exact bounds on its performance.
Original languageEnglish
Title of host publicationProceedings of the 8th Workshop on Quantitative Aspects of Programming Languages
EditorsAlessandra Di Pierro, Gethin Norman
PublisherElectronic Proceedings in Theoretical Computer Science (EPTCS)
Pages129-143
Number of pages15
DOIs
Publication statusPublished - 2010
EventWorkshop on Quantitative Aspects of Programming Languages - Cyprus
Duration: 27 Mar 201028 Mar 2010

Workshop

WorkshopWorkshop on Quantitative Aspects of Programming Languages
CityCyprus
Period27/03/1028/03/10

Fingerprint Dive into the research topics of 'An expectation transformer approach to predicate abstraction and data independence for probabilistic programs'. Together they form a unique fingerprint.

Cite this