Tuning Temporal Features within the Stochastic [pi]-Calculus

• Published in: IEEE transactions on software engineering 2011-11, Vol.37 (6), p.858
• Main Authors: Pauleve, Loic, Magnin, Morgan, Roux, Olivier
• Format: Article
• Language: English
• Subjects: Algorithms; Calculus; Case studies; Communication; Digital Object Identifier; Markov analysis; Random variables
• ISSN: 0098-5589; 1939-3520
• DOI: 10.1109/TSE.2010.95

The stochastic \pi-calculus is a formalism that has been used for modeling complex dynamical systems where the stochasticity and the delay of transitions are important features, such as in the case of biochemical reactions. Commonly, durations of transitions within stochastic \pi-calculus models follow an exponential law. The underlying dynamics of such models are expressed in terms of continuous-time Markov chains, which can then be efficiently simulated and model-checked. However, the exponential law comes with a huge variance, making it difficult to model systems with accurate temporal constraints. In this paper, a technique for tuning temporal features within the stochastic \pi-calculus is presented. This method relies on the introduction of a stochasticity absorption factor by replacing the exponential distribution with the Erlang distribution, which is a sum of exponential random variables. This paper presents a construction of the stochasticity absorption factor in the classical stochastic \pi-calculus with exponential rates. Tools for manipulating the stochasticity absorption factor and its link with timed intervals for firing transitions are also presented. Finally, the model-checking of such designed models is tackled by supporting the stochasticity absorption factor in a translation from the stochastic \pi-calculus to the probabilistic model checker PRISM.