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 Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

The role played by counterexamples in standard system analysis is well known;but less common is a notion of counterexample in probabilistic systemsrefinement. In this paper we extend previous work using counterexamples toinductive invariant properties of probabilistic systems, demonstrating how theycan be used to extend the technique of bounded model checking-style analysisfor the refinement of quantitative safety specifications in the probabilistic Blanguage. In particular, we show how the method can be adapted to cope withrefinements incorporating probabilistic loops. Finally, we demonstrate thetechnique on pB models summarising a one-step refinement of a randomisedalgorithm for finding the minimum cut of undirected graphs, and that for thedependability analysis of a controller design.

Model exploration and analysis for quantitative safety refinement in probabilistic B