English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

In this paper we revisit the well-known technique of predicate abstraction tocharacterise performance attributes of system models incorporating probability.We recast the theory using expectation transformers, and identify transformerproperties which correspond to abstractions that yield nevertheless exact boundon the performance of infinite state probabilistic systems. In addition, weextend the developed technique to the special case of "data independent"programs incorporating probability. Finally, we demonstrate the subtleness ofthe extended technique by using the PRISM model checking tool to analyse aninfinite state protocol, obtaining exact bounds on its performance.

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