# 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.