@inproceedings{88c4385515224e8faf18f0076ce5225d,
title = "Automating refinement checking in probabilistic system design",
abstract = "Refinement plays a crucial role in {"}top-down{"} styles of verification, such as the refinement calculus, but for probabilistic systems proof of refinement is a particularly challenging task due to the combination of probability and nondeterminism which typically arises in partially-specified systems. Whilst the theory of probabilistic refinement is well-known [18] there are few tools to help with establishing refinements between programs. In this paper we describe a tool which provides partial support during refinement proofs. The tool essentially builds small models of programs using an algebraic rewriting system to extract the overall probabilistic behaviour. We use that behaviour to recast refinement-checking as a linear satisfiability problem, which can then be exported to a linear arithmetic solver. One of the major benefits of this approach is the ability to generate counterexamples, alerting the prover to a problem in a proposed refinement. We demonstrate the technique on a small case study based on Schneider et al.'s Tank Monitoring [26].",
keywords = "Algebraic rewriting system for probability, Linear satisfiability, Probabilistic systems, Probabilistic verification, Refinement",
author = "C. Gonzalia and A. McIver",
year = "2007",
doi = "10.1007/978-3-540-76650-6_13",
language = "English",
isbn = "9783540766483",
volume = "4789 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer, Springer Nature",
pages = "212--231",
editor = "Michael Butler and Hinchey, {Michael G.} and Larrondo-Petrie, {Maria M.}",
booktitle = "Formal Methods and Software Engineering - 9th International Conference on Formal Engineenng Methods, ICFEM 2007, Proceedings",
address = "United States",
note = "9th International Conference on Formal Engineering Methods, ICFEM 2007 ; Conference date: 14-11-2007 Through 15-11-2007",
}