www.prismmodelchecker.org
[GR12] Sergio Giro and Markus Rabe. Verification of Partial-Information Probabilistic Systems using Counterexample-Guided Refinements. In Proc. 10th International Symposium on Automated Technology for Verification and Analysis (ATVA'12), volume 7561 of LNCS, pages 333-348, Springer. October 2012. [pdf] [bib] [Describes new techniques for model checking MDPs under partial-information schedulers, implemented in an extension of PRISM.]
Downloads:  pdf pdf (562 KB)  bib bib
Notes: The original publication is available at www.springerlink.com.
Abstract. The verification of partial-information probabilistic systems has been shown to be undecidable in general. In this paper, we present a technique based on inspection of counterexamples that can be helpful to analyse systems in particular cases. The starting point is the observation that the system under complete information provides safe bounds for the extremal probabilities of the system under partial information. Using classical (total information) model checkers, we can determine optimal schedulers that represent safe bounds but which may be spurious, in the sense that they use more information than is available under the partial information assumptions. The main contribution of this paper is a refinement technique that, given such a scheduler, transforms the model to exclude the scheduler and with it a whole class of schedulers that use the same unavailable information when making a decision. With this technique, we can use classical total information probabilistic model checkers to analyse a probabilistic partial information model with increasing precision. We show that, for the case of infimum reachability probabilities, the total information probabilities in the refined systems converge to the partial information probabilities in the original model.

Publications