A Probabilistic Model for Molecular Systems

We introduce a model for molecular reactions based on probabilistic rewriting rules. We give a probabilistic algorithm for rule applications as a semantics for the model, and we show how a probabilistic transition system can be derived from it. We use the algorithm in the development of an interpreter for the model, which we use to simulate the evolution of molecular systems. In particular, we show the results of the simulation of a real example of enzymatic activity. Moreover, we apply the probabilistic model checker PRISM to the transition system derived by the model of this example, and we show the results of model checking of some illustrative properties.