FORMATS'15 - Supporting Material

Paper: "Automated Verification of Partially Observable Probabilistic Real-Time Systems"
Gethin Norman, David Parker and Xueyi Zou

Models and Properties

Included below are the models and properties for the examples and case studies included in the paper. The models are partially observable probabilistic timed automata (POPTAs). For this, we developed a prototype extension of the probabilistic model checker PRISM, which has since been improved and integrated into the main codebase (see below for details). Small fixes have been applied to some of the models, mainly to comply with syntactic checks added to the implementation. If you specifically need the original versions, check this archive.

The models can also be treated as (fully observable) PTAs with the standard version of PRISM, by changing the keyword popta to pta and removing the observables block.

The Tool

The prototype extension of PRISM developed for this paper has since been integrated into the main codebase, and we recommend that you use that if you are interested this implementation of POMDP model checking. If you specifically need the original version of the code used for the paper, you can find it here.

In the main release of PRISM, the examples above can be found in prism-examples/pomdps and prism-examples/poptas. In the zip file of the original code, they are in prism/examples-distr. In both cases, scripts are provided to show how to run them. Here is an example, where -gridresolution is used to change the grid resolution (M in the paper):

prism pump.prism pump.props -prop 2 -const h0=2,h1=16,N=8 -gridresolution 2

We also provide logs showing the execution of the tool on the case studies in the paper: logs.tar.gz.