# TACAS'16 Paper - Tool Description and Benchmarks

Paper: "PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems"
by Milan Češka, Petr Pilař, Nicola Paoletti, Luboš Brim, and Marta Kwiatkowska

PRISM-PSY is a novel tool that performs precise GPU-accelerated parameter synthesis for continuous-time Markov chains (CTMCs) and time-bounded temporal logic specifications. The tool, publicly available at github extends the widely used probabilistic model-checker PRISM. All the experiments have been carried out using the branch develop-ocl-paper.

## Usage

Currently, the functionality is accessible only via the command-line interface. The switches for invoking parameter exploration and parameter synthesis procedures are listed below:

• `-pse <time> <space> <acc>` performs forward parametric transient analysis with parameter space `<space>` and accuracy `<acc>` for time point `<time>`. The parameter space describes the parameters and their ranges as a list of elements of the following form: `<parameter>=<lower-bound>:<upper-bound>`. Note that parameters must be declared as uninitialised constants in the PRISM model file. The accuracy value is a real number determining the greatest acceptable difference between the maximised and minimised probability of the same state; if the results of transient analysis are too inaccurate in this sense, the parameter space gets decomposed into subregions and the transient computation is repeated, with the parameters' ranges being successively reduced to the individual subregions. For example:
```	prism ../bench/models/sir.sm -pse 2.5 k1=0.3:0.5,k2=0.8:1.0 5e-3
```
• `-psesynth-thr <space> <tol>` solves the threshold synthesis problem with parameter space `<space>` and volume tolerance `<tol>`. This switch requires a property containing a probability/reward threshold `~r`.
• `-psecheck <space> <acc>` performs parametric model checking (i.e. approximate the satisfaction function) with parameter space `<space>` and accuracy `<acc>`. This switch as well as all switches for min/max synthesis require a quantitative property specification, i.e. with unknown probability/reward threshold (`~r` is replaced by `?`).
• `-psesynth-min-naive <space> <tol>` solves the min synthesis problem using the naive approach (no sampling) with parameter space `<space>` and probability tolerance `<tol>`.
• `-psesynth-min-sampling <space> <tol>` solves the min synthesis problem using the sampling-based approach with parameter space `<space>` and probability tolerance `<tol>`.
• `-psesynth-max-naive <space> <tol>` solves the max synthesis problem using the naive approach (no sampling) with parameter space `<space>` and probability tolerance `<tol>`.
• `-psesynth-max-sampling <space> <tol>` solves the max synthesis problem using the sampling-based approach with parameter space `<space>` and probability tolerance `<tol>`.

Outputs vary depending on the settings of the synthesis experiment. However, in most cases, the results contain a structured listing of the final parameter regions meeting the user-specified accuracy criteria. For instance, for the third experiment in the Google FS model, we obtain:

```	True regions (31):
* c_fail=0.2265625:0.2575,c_hw_repair_rate=1.015625:1.0625 [lower prob bound = 0.5208975938617837, upper prob bound = 0.6607299064918649]
* c_fail=0.4121875:0.443125,c_hw_repair_rate=1.4375:1.484375 [lower prob bound = 0.5581055125135674, upper prob bound = 0.6550648387086644]
....

False regions (54):
* c_fail=0.87625:0.938125,c_hw_repair_rate=0.875:0.96875 [lower prob bound = 0.09624826389447758, upper prob bound = 0.2995971131368263]
* c_fail=0.13375:0.195625,c_hw_repair_rate=1.53125:1.625 [lower prob bound = 0.2653483558746305, upper prob bound = 0.44262270471338117]
...

Undecided regions (51):
* c_fail=0.35031249999999997:0.38125,c_hw_repair_rate=0.96875:1.015625 [lower prob bound = 0.3629496979782683, upper prob bound = 0.5090851688699273]
* c_fail=0.4740625:0.505,c_hw_repair_rate=1.484375:1.53125 [lower prob bound = 0.46962807535355544, upper prob bound = 0.5680179153119927]
...
```
In addition, parametric transient analysis yields an output where each region is associated with vectors of minimised & maximised values:

```	Printing minimised & maximised transient probabilities:

== Region k1=0.3:0.4 ==

=== Minimised state values ===

3:(1,1)=8.997879675312062E-5
6:(2,0)=0.9998740020491458
9:(3,0)=5.998467961952004E-6

=== Maximised state values ===

3:(1,1)=1.1997172900416084E-4
6:(2,0)=0.9999039949813968
9:(3,0)=5.998467961952004E-6

== Region k1=0.4:0.5 ==

=== Minimised state values ===

3:(1,1)=1.1997172900416084E-4
6:(2,0)=0.9998440091168947
9:(3,0)=5.998467961952004E-6

=== Maximised state values ===

3:(1,1)=1.4996466125520103E-4
6:(2,0)=0.9998740020491458
9:(3,0)=5.998467961952004E-6
```

The output indicates that the result for parameter region `k1=0.3:0.5` was not accurate enough and thus the region was decomposed into two subregions `k1=0.3:0.4` and `k1=0.4:0.5` both of which in turn satisfied the accuracy criteria. Results for the parametric model checking and parameter synthesis are related to the single given initial state. The results for the other states can be obtained using `print filter`.

The optimizations and data-parallelisation presented in the paper can be turned on using environment variables as follows:

• `PSE_ADAPTIVE_FOX_GLYNN=0|1 (default 0)` -- Turns on the adaptive Fox-Glynn technique.
• `PSE_OCL=0|1 (default 0)` -- Turns on the GPU acceleration.
• `PSE_FMT=CSR|ELL (default CSR)` -- Turns on the CSR/ELL based implementation. Works only in combination with PSE_OCL=1.
• `PSE_PARA=n` -- Turns on parallelisation on the subregion level for multi-core CPUs. Works only in combination with PSE_OCL=0.
• `PSE_MANY=n` -- Turns on parallelisation on the subregion level for GPUs. Works only in combination with PSE_OCL=1.

## Benchmarks

• 1st experiment: ` prism google.sm -psesynth-thr c_hw_repair_rate=0.5:2 0.01 -csl 'P>=0.5 [ F<=60 (service_level_3) ]' `
• 2nd experiment: `prism google.sm -psesynth-max-sample c_hw_repair_rate=0.5:2 0.01 -csl 'P=? [ !(service_level_3) U[40,60] (service_level_3) ]' `
• 3rd experiment: ` prism google.sm -psesynth-thr c_fail=0.01:1,c_hw_repair_rate=0.5:2 0.1 -csl ' P>=0.5 [ !(service_level_3) U[40,60] (service_level_3) ] ' `
• Epidemic Model Models: sir.sm, sir-big.sm
• 1st experiment: ` prism sir.sm -psesynth-max-sample ki=5e-05:0.003,kr=0.005:0.2 0.01 -csl 'P=? [ (popI>0) U[100,120] (popI=0) ]' `
• 2nd experiment:` prism sir-big.sm -psesynth-max-sample ki=5e-05:0.003,kr=0.005:0.2 0.01 -csl 'P=? [ (popI>0) U[100,200] (popI=0) ]' `
• Signalling in Prokaryotic Cells Models: sig.sm, sig-big.sm
• 1st experiment: ` prism sig.sm -psesynth-thr degrR=0.005:0.02,prodR=0.1:0.9 0.09 -csl 'R{"noise"}>=8.0 [C<=10]' `
• 2nd experiment:``` prism sig-big.sm -psesynth-thr degrR=0.005:0.02,prodR=0.1:0.9 0.09 -csl 'R{"noise"}>=8.0 [C<=10]' ```
• Approximate Majority Models: am.sm
• 1st experiment: ` prism am.sm -psesynth-thr k1=1:100,k2=1:100,k3=1:100 0.1 -csl 'P>=0.95 [ F[100,100] (popA=14)&(popB=0) ]' `
• Workstation Cluster Models: cluster.sm
• 1st experiment: ` prism cluster.sm -psesynth-thr ws_check=5:20,ws_fail=0.001:0.02,ws_repair=0.5:5 0.1 -csl 'R{"time_not_min"}<=0.1[ C<=100 ]' `

To execute benchmarks for a particular case study, a perl script is available at bench.pl. Usage:

```perl bench.pl <input> <n> <folder>
```

where `<input>` is an input script (e.g. SIR.in.pl for the epidemic model), `<n>` is the number of executions for each setting and `<folder>` is an output folder. If the script is run with the option `--dry` it only generates a set of commands related to the benchmark (without executing it) in the following form:

```env PRISM_JAVAMAXMEM=8g PSE_ADAPTIVE_FOX_GLYNN=1 PSE_FMT=ELL PSE_MANY=16 PSE_OCL=1 stdbuf -o0 -e0 ../bin/prism sir.sm -psesynth-max-sample ki=5e-05:0.003,kr=0.005:0.2 0.01 -csl 'P=? [ (popI>0) U[100,120] (popI=0) ]'
```

## Limitations

### Rate functions

The current implementation of the tool supports only linear parametric rate functions where parameters can occur only as factors multiplying the rate constants. Specifically, the PRISM guarded command for a parametric transition has the following form:

```	[synchronization] (guard) -> k * const : (update);
```

where `k` is a parameter and `const` is a (possibly state-dependent) constant. Such parametric rate functions are sufficient to describe a wide range of systems, from biological (e.g. mass action kinetics) to computer systems (e.g. queueing protocols).

### Properties

To specify properties, we employ the time-bounded fragment of Continuous Stochastic Logic (CSL) extended with time-bounded rewards. Currently, the tool support only unnested formulae given by the following syntax:

```	state formula Φ = P~r[φ] | R~r[C<=t]
```
```	path formula φ =  Ψ U[t1,t2] Ψ, where Ψ = `a` | !Ψ | Ψ & Ψ, and
```

`a` is an atomic proposition, `~r` is an probability or reward threshold, `t` is a time bound, and `[t1,t2]` is a bounded time interval. The tool also supports the derived operators future (`F`) and globally (`G`). Note that, the synthesis algorithms will be adapted in future to support the full fragment of time-bounded CSL including nested formulae.

### Model size

The current version of the tool employs the front-end and the explicit model construction of the PRISM tool. Namely, PRISM-PSY builds on top of the PRISM explicit engine which does not scale well for large models as it uses a large amount of memory during model construction. Although we have reduced the memory consumption of the explicit engine, the construction of a model with 1M states still requires more than 8G, which is the available memory of the workstation we used for the experimental evaluation. Note that the environment variable `PRISM_JAVAMAXMEM=8g` has to be set in order to reserve enough memory for the tool. Also note that this memory issue is not related to the algorithms nor their data-parallel implementation presented in this paper. We plan to implement our own parser and model construction in order to solve this memory constraint.