Abstract
We consider the issue of finding and presenting counterexamples to a claim “this spec is implemented by that imp”, that is \(\textit{spec} \sqsubseteq \textit{imp}\) (refinement), in the context of probabilistic systems: using a geometric interpretation of the probabilistic/demonic semantic domain we are able to encode both refinement success and refinement failure as linear satisfaction problems, which can then be analysed automatically by an SMT solver. This allows the automatic discovery of certificates for counterexamples in independently and efficiently checkable form. In many cases the counterexamples can subsequently be converted into “source level” hints for the verifier.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Back, R.-J.R., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, Heidelberg (1998)
Clarke, E., Lu, Y., Grumberg, O., Jha, S., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM 50(5), 752–794 (2003)
Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 45–59. Springer, Heidelberg (2000)
Deng, Y., van Glabeek, R., Morgan, C.C., Zhang, C.: Scalar Outcomes Suffice for Finitary Probabilistic Testing. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 363–378. Springer, Heidelberg (2007)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)
Gonzalia, C., McIver, A.K.: Automating Refinement Checking in Probabilistic System Design. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol. 4789, pp. 212–231. Springer, Heidelberg (2007)
Han, T., Katoen, J.-P.: Counterexamples in probabilistic model checking. In: Krishnamurthi, S., Odersky, M. (eds.) CC 2007. LNCS, vol. 4420, pp. 72–86. Springer, Heidelberg (2007)
He, J., Seidel, K., McIver, A.: Probabilistic models for the guarded command language. Science of Computer Programming 28, 171–192 (1997)
Hurd, J., McIver, A.K., Morgan, C.C.: Probabilistic guarded commands mechanised in HOL. In: Cerone, A., de Pierro, A. (eds.) Proc 4th QAPL. ENTCS, vol. 112, Elsevier, Amsterdam (2005)
Kozen, D.: A probabilistic PDL. Jnl. Comp. Sys. Sci. 30(2), 162–178 (1985)
McIver, A.K., Morgan, C.C.: Abstraction, Refinement and Proof for Probabilistic Systems. In: Tech. Mono. Comp. Sci., Springer, New York (2005)
McIver, A.K., Morgan, C.C., Gonzalia, C.: Proofs and refutations for probabilistic systems (2007), http://www.ics.mq.edu.au/~anabel/FM08.pdf
Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice-Hall, Englewood Cliffs (1994)
Morgan, C.C., McIver, A.K., Seidel, K.: Probabilistic predicate transformers. ACM Trans. Prog. Lang. Sys. 18(3), 325–353 (1996)
von Neumann, J., Morgenstern, O.: Theory of Games and Economic Behavior, 2nd edn. Princeton University Press, Princeton (1947)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
McIver, A.K., Morgan, C.C., Gonzalia, C. (2008). Proofs and Refutations for Probabilistic Refinement. In: Cuellar, J., Maibaum, T., Sere, K. (eds) FM 2008: Formal Methods. FM 2008. Lecture Notes in Computer Science, vol 5014. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68237-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-68237-0_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68235-6
Online ISBN: 978-3-540-68237-0
eBook Packages: Computer ScienceComputer Science (R0)