Subscribe
Issue No.06 - November/December (2011 vol.37)
pp: 858-871
Loïc Paulevé , IRCCyN, École Centrale de Nantes
Morgan Magnin , IRCCyN, École Centrale de Nantes
Olivier Roux , IRCCyN, École Centrale de Nantes
ABSTRACT
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.
INDEX TERMS
Temporal parameters, \pi-calculus, model-checking, Markov processes, stochastic processes.
CITATION
Loïc Paulevé, Morgan Magnin, Olivier Roux, "Tuning Temporal Features within the Stochastic π-Calculus", IEEE Transactions on Software Engineering, vol.37, no. 6, pp. 858-871, November/December 2011, doi:10.1109/TSE.2010.95
REFERENCES
 [1] R. Milner, Communication and Concurrency. Prentice-Hall, Inc., 1989. [2] M. Abadi and A.D. Gordon, "A Calculus for Cryptographic Protocols: The Spi Calculus," Information and Computation, vol. 148, pp. 36-47, 1999. [3] C. Priami, "Stochastic $\pi$ -Calculus," The Computer J., vol. 38, no. 7, pp. 578-589, 1995. [4] C. Priami, A. Regev, E. Shapiro, and W. Silverman, "Application of a Stochastic Name-Passing Calculus to Representation and Simulation of Molecular Processes," Information Processing Letters, vol. 80, no. 1, pp. 25-31, 2001. [5] C. Kuttler and J. Niehren, "Gene Regulation in the pi Calculus: Simulating Cooperativity at the Lambda Switch," Trans. Computational Systems Biology, pp. 24-55, Springer, 2006. [6] R. Blossey, L. Cardelli, and A. Phillips, "Compositionality, Stochasticity and Cooperativity in Dynamic Models of Gene Regulation," HFSP J., vol. 2, no. 1, pp. 17-28, Feb. 2008. [7] L. Cardelli, E. Caron, P. Gardner, O. Kahramanogullari, and A. Phillips, "A Process Model of Actin Polymerisation," Electronic Notes in Theoretical Computer Science, vol. 229, pp. 127-144, 2009. [8] D.T. Gillespie, "Exact Stochastic Simulation of Coupled Chemical Reactions," The J. Physical Chemistry, vol. 81, no. 25, pp. 2340-2361, 1977. [9] A. Phillips and L. Cardelli, "Efficient, Correct Simulation of Biological Processes in the Stochastic pi-Calculus," Computational Methods in Systems Biology, Springer, 2007. [10] G. Norman, C. Palamidessi, D. Parker, and P. Wu, "Model Checking Probabilistic and Stochastic Extensions of the $\pi$ -Calculus," IEEE Trans. Software Eng., vol. 35, no. 2, pp. 209-223, Mar./Apr. 2009. [11] A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker, "PRISM: A Tool for Automatic Verification of Probabilistic Systems," Proc. 12th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, 2006. [12] R. Alur and D. Dill, "The Theory of Timed Automata," Proc. REX Workshop Real-Time Theory in Practice, pp. 45-73, 1992. [13] P.M. Merlin, "A Study of the Recoverability of Computing Systems," PhD dissertation, 1974. [14] P. Francois, V. Hakim, and E.D. Siggia, "Deriving Structure from Evolution: Metazoan Segmentation," Molecular Systems Biology, vol. 3, 2007. [15] R. Milner, Communicating and Mobile Systems: The $\pi$ -Calculus. Cambridge Univ. Press, 1999. [16] C. Priami, "Stochastic $\pi$ -Calculus with General Distributions," Proc. Fourth Workshop Process Algebras and Performance Modelling, pp. 41-57, 1996. [17] A. Phillips, L. Cardelli, and G. Castagna, "A Graphical Representation for Biological Processes in the Stochastic pi-Calculus," Trans. Computational Systems Biology, pp. 123-152, Springer, 2006. [18] M. Evans, N. Hastings, and B. Peacock, Statistical Distributions, third ed. Wiley-Interscience, 2000. [19] A. Phillips, SPiM, http://research.microsoft.com/~aphillipspim , 2009. [20] A. Zaigraev and A. Podraza-Karakulska, "On Estimation of the Shape Parameter of the Gamma Distribution," Statistics & Probability Letters, vol. 78, no. 3, pp. 286-295, 2008. [21] J. Mi and A. Naranjo, "Inferences about the Scale Parameter of the Gamma Distribution Based on Data Mixed from Censoring and Grouping," Statistics & Probability Letters, vol. 62, no. 3, pp. 229-243, 2003. [22] D.J. Wilkinson, Stochastic Modelling for Systems Biology. Chapman & Hall/CRC, 2006. [23] D. Best and D. Roberts, "Algorithm AS91: The Percentage Points of the Chi-Squared Distribution," Applied Statistics, vol. 24, no. 3, pp. 385-390, 1975. [24] A.R. DiDonato and A.H. MorrisJr., "Computation of the Incomplete Gamma Function Ratios and Their Inverse," ACM Trans. Math. Software, vol. 12, no. 4, pp. 377-393, 1986. [25] R Development Core Team, R: A Language and Environment for Statistical Computing, R Foundation for Statistical Computing, http:/www.R-project.org, 2009. [26] R. Kohavi and F. Provost, "Glossary of Terms," Applications of Machine Learning and the Knowledge Discovery Process vol. 30, editorial for the special issue, 1998. [27] S. Amari and R. Misra, "Closed-Form Expressions for Distribution of Sum of Exponential Random Variables," IEEE Trans. Reliability, vol. 46, no. 4, pp. 519-522, Dec. 1997. [28] S. Nadarajah, "A Review of Results on Sums of Random Variables," Acta Applicandae Mathematicae, vol. 103, no. 2, pp. 131-140, 2008. [29] S. Favaro and S. Walker, "On the Distribution of Sums of Independent Exponential Random Variables via Wilks' Integral Representation," Acta Applicandae Mathematicae, vol. 109, no. 3, pp. 1035-1042, 2010. [30] I. Mura, D. Prandi, C. Priami, and A. Romanel, "Exploiting Non-Markovian Bio-Processes," Electronic Notes in Theoretical Computer Science, vol. 253, no. 3, pp. 83-98, 2009. [31] M.A. Gibson and J. Bruck, "Efficient Exact Stochastic Simulation of Chemical Systems with Many Species and Many Channels," The J. Physical Chemistry A, vol. 104, no. 9, pp. 1876-1889, 2000. [32] M. Kwiatkowska, G. Norman, and D. Parker, "Symmetry Reduction for Probabilistic Model Checking," Proc. 18th Int'l Conf. Computer Aided Verification, pp. 234-248, 2006. [33] J.-P. Katoen, D. Klink, M. Leucker, and V. Wolf, "Abstraction for Stochastic Systems by Erlang's Method of Stages," Proc. 19th Int'l Conf. Concurrency Theory, pp. 279-294, 2008. [34] G. López, H. Hermanns, and J.-P. Katoen, "Beyond Memoryless Distributions: Model Checking Semi-Markov Chains," Proc. Joint Int'l Workshop Process Algebra and Probabilistic Methods, Performance Modelling and Verification, pp. 57-70, 2001. [35] J. Bryans, H. Bowman, and J. Derrick, "Model Checking Stochastic Automata," ACM Trans. Computational Logic, vol. 4, no. 4, pp. 452-492, 2003. [36] A. Bobbio and A. Horváth, "Petri Nets with Discrete Phase Type Timing: A Bridge between Stochastic and Functional Analysis," Electronic Notes in Theoretical Computer Science, vol. 52, no. 3, pp. 209-226, 2002.