Model exploration and analysis for quantitative safety refinement in probabilistic B

The role played by counterexamples in standard system analysis is well known; but less common is a notion of counterexample in probabilistic systems refinement. In this paper we extend previous work using counterexamples to inductive invariant properties of probabilistic systems, demonstrating how t...

Full description

Bibliographic Details
Main Authors: Annabelle McIver, Ukachukwu Ndukwu
Format: Article
Language:English
Published: Open Publishing Association 2011-06-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1106.4096v1