"Verification and Control of Partially Observable Probabilistic Systems" - Supporting Material

Paper: "Verification and Control of Partially Observable Probabilistic 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 Markov decision processes (POMDPs) and partially observable probabilistic timed automata (POPTAs). For the paper, 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) MDPs and PTAs with the standard version of PRISM, by changing the keyword pomdp to mdp or popta to pta and removing the observables block.

• Simple examples
  
  
  • POMDP models: maze.prism and maze2.prism
  • POPTA models: example1.prism and example2.prism
  • Property files: maze.props, example1.props and example2.props
  
  
• Wireless Network Scheduling (POMDP)
  
  
  • Model without priorities: network2.prism and network3.prism
  • Model without priorities and no idling: network2_noidle.prism and network3_noidle.prism
  • Model with priorities: network2_priorities.prism and network3_priorities.prism
  • Model with priorities and no idling: network2_priorities_noidle.prism and network3_priorities_noidle.prism
  • Property files: network.props and network_priorities.props
  • Parameters:
    • T number of slots per time period
    • K number of time periods
  
  
• Task-graph scheduling problem (POPTA)
  
  
  • Basic POPTA model: scheduler.prism
  • Model with random delays: scheduler_prob.prism
  • Property file: scheduler.props
  • Parameter: sleep (probability processor p1 goes into sleep state after finishing a task)
  
  
• The NRL (Naval Research Laboratory) pump (POPTA)
  
  
  • Model: pump.prism
  • Property file: pump.props
  • Parameters:
    • h0 time delay between acks when high tries to communicate 0
    • h1 time delay between acks when high tries to communicate 1
    • N number of messages that low sends
  
  
• Markowitch & Roggeman's non-repudiation protocol (POPTA)
  
  
  • Simple POMDP model: repudiation_pomdp.prism
  • Basic POPTA model: repudiation.prism
  • Complex POPTA model: repudiation_complex.prism
  • Property file: repudiation.props
  • Parameters: K (the originator randomly selects an integer over the range 1,...,K)
  
  
• The Dining Cryptographers Protocol (POMDP)
  
  
  • Models: crypt3.prism, crypt4.prism, crypt5.prism and crypt6.prism
  • Property file: crypt.props
  
  
• Robot in a grid (POMDP)
  
  
  • Models: 3x3grid.prism (POMDP), 4x4grid.prism
  • Models for step bounded property: 3x3grid_bounded.prism, 4x4grid_bounded.prism
  • Property file: grid.props
  • Parameters: K number of steps (in bounded property)

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.