The AMSR2PRISM translator

The software allows biological systems modelling when the exact rates of biological events are not known, but are supposed to lie in some intervals. On these (abstract) models it is possible to perform probabilistic model checking obtaining lower and upper bounds for the probabilities of reaching states satisfying given properties. These bounds are under- and over-approximations, respectively, of the probabilities one would obtain by verifying the models with exact kinetic rates belonging to the intervals (the model checking is realized using PRISM).

For more information on the approach followed by the tool have a look at the paper “Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates”.

Download (binary)

Download (sources)