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

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.

Links

Last commit date

8 August 2014

Related papers

https://doi.org/10.1007/978-3-662-49674-9_21 (TACAS '16)

Last publication date

9 April 2016

Related tools

Parameter synthesis for discrete-time Markovian models: PROPhESY

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.