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

GPU-accelerated parameter synthesis for stochastic systems

Application domain/field

• Continuous-time Markov chains (CTMCs)
• Parameter synthesis
• Continuous stochastic logic (CSL)
• Model checking
• Stochastic model checking

Type of tool

Parameter synthesizer

Internals

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.