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:

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:

Benchmarks

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.