×

Formalisms for specifying Markovian population models. (English) Zbl 1260.68284

Bournez, Olivier (ed.) et al., Reachability problems. 3rd international workshop, RP 2009, Palaiseau, France, September 23–25, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-04419-9/pbk). Lecture Notes in Computer Science 5797, 3-23 (2009).
Summary: We compare several languages for specifying Markovian population models such as queuing networks and chemical reaction networks. These languages – matrix descriptions, stochastic Petri nets, stoichiometric equations, stochastic process algebras, and guarded command models – all describe continuous-time Markov chains, but they differ according to important properties, such as compositionality, expressiveness and succinctness, executability, ease of use, and the support they provide for checking the well-formedness of a model and for analyzing a model.
For the entire collection see [Zbl 1175.68005].

MSC:

68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
60J27 Continuous-time Markov processes on discrete state spaces
65C40 Numerical analysis or methods applied to Markov chains
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

SMART_; Bio-PEPA; MRMC

References:

[1] Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods in System Design 15(1), 7–48 (1999) · doi:10.1023/A:1008739929481
[2] Anderson, W.: Continuous-time Markov chains: An applications-oriented approach. Springer, Heidelberg (1991) · Zbl 0731.60067 · doi:10.1007/978-1-4612-3038-0
[3] Baarir, S., Beccuti, M., Cerotti, D., De Pierro, M., Donatelli, S., Franceschinis, G.: The GreatSPN tool: recent enhancements. SIGMETRICS Perform. Eval. Rev. 36(4), 4–9 (2009) · doi:10.1145/1530873.1530876
[4] Bernardo, M., Gorrieri, R.: Extended Markovian process algebra. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 315–330. Springer, Heidelberg (1996) · doi:10.1007/3-540-61604-7_63
[5] Buchholz, P.: Exact and ordinary lumpability in finite markov chains. Journal of applied probability 31(1), 59–75 (1994) · Zbl 0796.60073 · doi:10.1017/S0021900200107338
[6] Buchholz, P., Dayar, T.: Block SOR preconditioned projection methods for Kronecker structured Markovian representations. SIAM Journal on Scientific Computing 26(4), 1289–1313 (2005) · Zbl 1076.60062 · doi:10.1137/S1064827503425882
[7] Buchholz, P., Sanders, W.H.: Approximate computation of transient results for large Markov chains. In: Proc. of QEST 2004, pp. 126–135. IEEE Computer Society Press, Los Alamitos (2004)
[8] Ciardo, G., Jones III, R.L., Miner, A.S., Siminiceanu, R.I.: Logic and stochastic modeling with SMART. Perform. Eval. 63(6), 578–608 (2006) · doi:10.1016/j.peva.2005.06.001
[9] Ciocchetta, F., Hillston, J.: Bio-PEPA: a framework for modelling and analysis of biological systems. Theoretical Computer Science (to appear, 2009) · Zbl 1173.68041 · doi:10.1016/j.tcs.2009.02.037
[10] Clarke, E., Fujita, M., McGeer, P., Yang, J., Zhao, X.: Multi-terminal binary decision diagrams: An ecient data structure for matrix representation. In: Proc. IWLS 1993 (1993)
[11] Deavours, D.D., Sanders, W.H.: ”On-the-fly” solution techniques for stochastic Petri nets and extensions. In: IEEE TSE, pp. 132–141 (1997) · doi:10.1109/PNPM.1997.595544
[12] Didier, F., Henzinger, T., Mateescu, M., Wolf, V.: Approximation of event probabilities in noisy cellular processes. In: Proc. of CMSB. LNCS, Springer, Heidelberg (to appear, 2009) · Zbl 1211.92016
[13] Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975) · Zbl 0308.68017 · doi:10.1145/360933.360975
[14] Fernandes, P., Plateau, B., Stewart, W.J.: Numerical evaluation of stochastic automata networks. In: Proc. of MASCOTS 1995 (1995) · doi:10.1109/MASCOT.1995.378690
[15] Fisher, J., Henzinger, T.A.: Executable cell biology. Nature Biotechnology 25, 1239–1249 (2007) · doi:10.1038/nbt1356
[16] Gardner, T., Cantor, C., Collins, J.: Construction of a genetic toggle switch in Escherichia coli. Nature 403, 339–342 (2000) · doi:10.1038/35002131
[17] Gillespie, D.T.: Markov Processes. Academic Press, London (1992)
[18] Götz, N., Herzog, U., Rettelbach, M.: TIPP – a language for timed processes and performance evaluation. Technical Report Technical Report 4/92, IMMD VII, University of Erlangen-Nurnberg (1992)
[19] Gross, D., Miller, D.: The randomization technique as a modeling tool and solution procedure for transient Markov processes. Operations Research 32(2), 926–944 (1984) · Zbl 0536.60078 · doi:10.1287/opre.32.2.343
[20] Haas, P.J.: Stochastic Petri Nets: Modelling, Stability, Simulation. Springer, Heidelberg (2002) · Zbl 1052.90001 · doi:10.1007/b97265
[21] Henzinger, T., Mateescu, M., Wolf, V.: Sliding window abstraction for infinite Markov chains. In: Proc. CAV. LNCS, Springer, Heidelberg (to appear, 2009) · Zbl 1242.60079
[22] Hermanns, H.: An operator for symmetry representation and exploitation in stochastic process algebras. In: Proc. of PAPM 1997, pp. 55–70 (1997)
[23] Hillston, J.: The nature of synchronisation. In: Proc. of PAPM 1994, pp. 51–70 (1994)
[24] Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996) · Zbl 1080.68003 · doi:10.1017/CBO9780511569951
[25] Horton, G., Kulkarni, V.G., Nicol, D.M., Trivedi, K.S.: Fluid stochastic Petri nets: Theory, applications, and solution techniques. European Journal of Operational Research 105(1), 184–201 (1998) · Zbl 0957.90011 · doi:10.1016/S0377-2217(97)00028-3
[26] Hucka, M., Finney, A., Sauro, H.M., Bolouri, H., Doyle, J.C., Kitano, H.: The systems biology markup language (SBML): a medium for representation and exchange of biochemical network models. BIOINFORMATICS 19(4), 524–531 (2003) · doi:10.1093/bioinformatics/btg015
[27] Katoen, J.-P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: Proc. of QEST 2005, pp. 243–244. IEEE Computer Society Press, Los Alamitos (2005)
[28] Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic model checking for performance and reliability analysis. ACM SIGMETRICS Performance Evaluation Review 36(4), 40–45 (2009) · doi:10.1145/1530873.1530882
[29] Law, A., Kelton, W.: Simulation Modeling and Analysis. McGraw-Hill, New York (2000) · Zbl 0489.65007
[30] Marsan, M.A., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with generalized stochastic petri nets. Sigm. Perform. Eval. Rev. 26(2), 2 (1998) · doi:10.1145/288197.581193
[31] McAdams, H.H., Arkin, A.: It’s a noisy business! Trends in Genetics 15(2), 65–69 (1999) · doi:10.1016/S0168-9525(98)01659-X
[32] Paulsson, J.: Summing up the noise in gene networks. Nature 427(6973), 415–418 (2004) · doi:10.1038/nature02257
[33] Plateau, B.: On the stochastic structure of parallelism and synchronization models for distributed algorithms. In: Proc. of the Sigmetrics Conference on Measurement and Modeling of Computer Systems, pp. 147–154 (1985) · doi:10.1145/317795.317819
[34] Priami, C.: Stochastic pi-calculus. The Computer Journal 38(7), 578–589 (1995) · doi:10.1093/comjnl/38.7.578
[35] Rao, C., Wolf, D., Arkin, A.: Control, exploitation and tolerance of intracellular noise. Nature 420(6912), 231–237 (2002) · doi:10.1038/nature01258
[36] Reuter, G.E.H.: Competition processes. In: Proc. 4th Berkeley Symp. Math. Statist. Prob., vol. 2, pp. 421–430. Univ. of California Press, Berkeley (1961) · Zbl 0114.09001
[37] Rutten, J., Kwiatkowska, M., Norman, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. CRM Monograph Series, vol. 23. American Mathematical Society, Providence (2004)
[38] Sanders, W.H., Ers, Y., Meyer, J.: Reduced base model construction methods for stochastic activity networks. In: Proc. of PNPM 1989, vol. 11, pp. 74–84 (1989)
[39] Srivastava, R., You, L., Summers, J., Yin, J.: Stochastic vs. deterministic modeling of intracellular viral kinetics. Journal of Theoretical Biology 218, 309–321 (2002) · doi:10.1006/jtbi.2002.3078
[40] Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1995)
[41] Stewart, W.J., Atif, K., Plateau, B.: The numerical solution of stochastic automata networks. European Journal of Operational Research 86(3), 503–525 (1995) · Zbl 0914.90112 · doi:10.1016/0377-2217(94)00075-N
[42] Swain, P.S., Elowitz, M.B., Siggia, E.D.: Intrinsic and extrinsic contributions to stochasticity in gene expression. Proc. Natl. Acad. of Sci. 99(20), 12795–12800 (2002) · doi:10.1073/pnas.162041399
[43] Tian, T., Burrage, K.: Stochastic models for regulatory networks of the genetic toggle switch. Proc. Natl. Acad. Sci. 103(22), 8372–8377 (2006) · doi:10.1073/pnas.0507818103
[44] Turner, T.E., Schnell, S., Burrage, K.: Stochastic approaches for modelling in vivo reactions. Computational Biology and Chemistry 28, 165–178 (2004) · Zbl 1087.92035 · doi:10.1016/j.compbiolchem.2004.05.001
[45] Wilkinson, D.J.: Stochastic Modelling for Systems Biology. Chapman & Hall, Boca Raton (2006) · Zbl 1099.92004
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.