PV2 PRISM-PSYsynthesises model parameters such that a property meets a given threshold

GPU-accelerated parameter synthesis for stochastic systems

Application domain/field

Type of tool

Parameter synthesizer


In model checking, one often assumes that model parameters are known. However, if these parameters are not known, then you can use parameter synthesis. In parameter synthesis for CTMCs, one takes a time-bounded CSL formula and a model whose transition rates are functions of the parameters. Then you try to find parameter values such that the satisfaction probability of the CSL formula meets a given threshold, is maximised, or is minimised. This tool uses GPUs to accelerate the synthesis procedure. PRISM-PSY uses the front-end of PRISM.


Related papers

PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems (TACAS '16)

Last publication date

9 April 2016

Related tools

Parameter synthesis for discrete-time Markovian models: PROPhESY

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.