{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T19:06:38Z","timestamp":1762542398092},"publisher-location":"Cham","reference-count":50,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319164793"},{"type":"electronic","value":"9783319164809"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-16480-9_52","type":"book-chapter","created":{"date-parts":[[2015,3,16]],"date-time":"2015-03-16T15:09:53Z","timestamp":1426518593000},"page":"542-554","source":"Crossref","is-referenced-by-count":10,"title":["Computing Biological Model Parameters by Parallel Statistical Model Checking"],"prefix":"10.1007","author":[{"given":"Toni","family":"Mancini","sequence":"first","affiliation":[]},{"given":"Enrico","family":"Tronci","sequence":"additional","affiliation":[]},{"given":"Ivano","family":"Salvo","sequence":"additional","affiliation":[]},{"given":"Federico","family":"Mari","sequence":"additional","affiliation":[]},{"given":"Annalisa","family":"Massini","sequence":"additional","affiliation":[]},{"given":"Igor","family":"Melatti","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"52_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-39176-7_4","volume-title":"Model Checking Software","author":"V. Alimguzhin","year":"2013","unstructured":"Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E.: A map-reduce parallel approach to automatic synthesis of control software. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol.\u00a07976, pp. 43\u201360. Springer, Heidelberg (2013)"},{"key":"52_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-642-39176-7_5","volume-title":"Model Checking Software","author":"V. Alimguzhin","year":"2013","unstructured":"Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E.: On-the-fly control software synthesis. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol.\u00a07976, pp. 61\u201380. Springer, Heidelberg (2013)"},{"key":"52_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-642-22944-2_28","volume-title":"Algebra and Coalgebra in Computer Science","author":"M. AlTurki","year":"2011","unstructured":"AlTurki, M., Meseguer, J.: pVeStA: A parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., C\u00eerstea, C. (eds.) CALCO 2011. LNCS, vol.\u00a06859, pp. 386\u2013392. Springer, Heidelberg (2011)"},{"doi-asserted-by":"crossref","unstructured":"Ballarini, P., Forlin, M., Mazza, T., Prandi, D.: Efficient parallel statistical model Checking of Biochemical Networks. In: Proc. of PDMC, EPCTS 2014, pp. 47\u201361 (2009)","key":"52_CR4","DOI":"10.4204\/EPTCS.14.4"},{"issue":"3","key":"52_CR5","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1093\/bib\/bbp020","volume":"10","author":"P. Ballarini","year":"2009","unstructured":"Ballarini, P., Guido, R., Mazza, T., Prandi, D.: Taming the complexity of biological pathways through parallel computing. Briefings in Bioinformatics\u00a010(3), 278\u2013288 (2009)","journal-title":"Briefings in Bioinformatics"},{"key":"52_CR6","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1186\/1752-0509-2-26","volume":"2","author":"E. Balsa-Canto","year":"2008","unstructured":"Balsa-Canto, E., Peifer, M., Banga, J.R., Timmer, J., Fleck, C.: Hybrid optimization method with general switching strategy for parameter estimation. BMC Systems Biology\u00a02, 26 (2008)","journal-title":"BMC Systems Biology"},{"issue":"3","key":"52_CR7","first-page":"35","volume":"194","author":"J. Barnat","year":"2008","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I., Dra\u017ean, S., \u0160afr\u00e1nek, D.: Parallel model checking large-scale genetic regulatory networks with DiVinE. ENTCS\u00a0194(3), 35\u201350 (2008)","journal-title":"ENTCS"},{"doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., \u0160afr\u00e1nek, D., Vejn\u00e1r, M.: Parameter scanning by parallel model checking with applications in systems biology. In: Proc. of HiBi\/PDMC, pp. 95\u2013104. IEEE (2010)","key":"52_CR8","DOI":"10.1109\/PDMC-HiBi.2010.21"},{"doi-asserted-by":"crossref","unstructured":"Chis, O.-T., Banga, J.R., Balsa-Canto, E.: Structural identifiability of systems biology models: A critical comparison of methods. PLoS ONE, 6(11) (2011)","key":"52_CR9","DOI":"10.1371\/journal.pone.0027755"},{"issue":"1","key":"52_CR10","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s00236-002-0099-y","volume":"39","author":"G. Penna Della","year":"2003","unstructured":"Della Penna, G., Intrigila, B., Tronci, E., Venturini Zilli, M.: Synchronized regular expressions. Acta Inf.\u00a039(1), 31\u201370 (2003)","journal-title":"Acta Inf."},{"unstructured":"Dierkes, T., R\u00f6blitz, S., Wade, M., Deuflhard, P.: Parameter identification in large kinetic networks with BioPARKIN. CoRR, abs (2013)","key":"52_CR11"},{"key":"52_CR12","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-540-88562-7_20","volume-title":"Computational Methods in Systems Biology","author":"R. Donaldson","year":"2008","unstructured":"Donaldson, R., Gilbert, D.: A model checking approach to the parameter estimation of biochemical pathways. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol.\u00a05307, pp. 269\u2013287. Springer, Heidelberg (2008)"},{"doi-asserted-by":"crossref","unstructured":"Ehrig, R., Nowak, U., Oeverdieck, L., Deuflhard, P.: Advanced extrapolation methods for large scale differential algebraic problems. In: High Performance Scient. and Eng. Comp. LNCSE (1999)","key":"52_CR13","DOI":"10.1007\/978-3-642-60155-2_20"},{"doi-asserted-by":"crossref","unstructured":"Gong, H., Zuliani, P., Komuravelli, A., Faeder, J.R., Clarke, E.M.: Analysis and verification of the hmgb1 signaling pathway. BMC Bioinform.\u00a011(S-7), S10 (2010)","key":"52_CR14","DOI":"10.1186\/1471-2105-11-S7-S10"},{"key":"52_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-642-28067-2_7","volume-title":"Algebraic and Numeric Biology","author":"H. Gong","year":"2012","unstructured":"Gong, H., Zuliani, P., Komuravelli, A., Faeder, J.R., Clarke, E.M.: Computational modeling and verification of signaling pathways in cancer. In: Horimoto, K., Nakatsui, M., Popov, N. (eds.) ANB 2010. LNCS, vol.\u00a06479, pp. 117\u2013135. Springer, Heidelberg (2012)"},{"doi-asserted-by":"crossref","unstructured":"Gong, H., Zuliani, P., Wang, Q., Clarke, E.M.: Formal analysis for logical models of pancreatic cancer. In: Proc. of 50th CDC, pp. 4855\u20134860. IEEE (2011)","key":"52_CR16","DOI":"10.1109\/CDC.2011.6161052"},{"unstructured":"Grosu, R., Smolka, S.A.: Quantitative model checking. In: Preliminary Proc. of ISoLA, pp. 165\u2013174 (2004)","key":"52_CR17"},{"key":"52_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-540-31980-1_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Grosu","year":"2005","unstructured":"Grosu, R., Smolka, S.A.: Monte carlo model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 271\u2013286. Springer, Heidelberg (2005)"},{"issue":"3","key":"52_CR19","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/j.tcs.2007.11.013","volume":"391","author":"J. Heath","year":"2008","unstructured":"Heath, J., Kwiatkowska, M.Z., Norman, G., Parker, D., Tymchyshyn, O.: Probabilistic model checking of complex biological pathways. Theor. Comput. Sci.\u00a0391(3), 239\u2013257 (2008)","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"Hussain, F., Dutta, R.G., Jha, S.K., Langmead, C.J., Jha, S.: Parameter discovery for stochastic biological models against temporal behavioral specifications using an sprt based metric for simulated annealing. In: Proc. of 2nd ICCABS, pp. 1\u20136. IEEE (2012)","key":"52_CR20","DOI":"10.1109\/ICCABS.2012.6182640"},{"doi-asserted-by":"crossref","unstructured":"Ingalls, B., Iglesias, P.: Control Theory and Systems Biology. MIT Press (2009)","key":"52_CR21","DOI":"10.7551\/mitpress\/9780262013345.001.0001"},{"key":"52_CR22","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1089\/10665270252833208","volume":"9","author":"H. Jong De","year":"2002","unstructured":"De Jong, H.: Modeling and simulation of genetic regulatory systems: A literature review. Journal of Computational Biology\u00a09, 67\u2013103 (2002)","journal-title":"Journal of Computational Biology"},{"issue":"4","key":"52_CR23","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/1364644.1364651","volume":"35","author":"M. Kwiatkowska","year":"2008","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Using probabilistic model checking in systems biology. ACM SIGMETRICS Perf. Eval. Rev.\u00a035(4), 14\u201321 (2008)","journal-title":"ACM SIGMETRICS Perf. Eval. Rev."},{"unstructured":"Langmead, C.J.: Generalized queries and bayesian statistical model checking in dynamic bayesian networks: Application to personalized medicine. In: Proc. of CSB, pp. 201\u2013212 (2009)","key":"52_CR24"},{"key":"52_CR25","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1090\/qam\/10666","volume":"2","author":"K. Levenberg","year":"1944","unstructured":"Levenberg, K.: A method for the solution of certain non-linear problems in least squares. The Quarterly of Applied Math\u00a02, 164\u2013168 (1944)","journal-title":"The Quarterly of Applied Math"},{"issue":"1","key":"52_CR26","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1186\/1752-0509-7-91","volume":"7","author":"P. Li","year":"2013","unstructured":"Li, P., Vu, Q.D.: Identification of parameter correlations for parameter estimation in dynamic biological models. BMC Systems Biology\u00a07(1), 91 (2013)","journal-title":"BMC Systems Biology"},{"key":"52_CR27","volume-title":"System Identification (2Nd Ed.): Theory for the User","author":"L. Ljung","year":"1999","unstructured":"Ljung, L.: System Identification (2Nd Ed.): Theory for the User. Prentice Hall PTR, Upper Saddle River (1999)"},{"unstructured":"Stahl, S., Brusco, M.: Branch-and-Bound Applications in Combinatorial Data Analysis. Statistics and Computing. Springer (2005)","key":"52_CR28"},{"key":"52_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-642-39799-8_21","volume-title":"Computer Aided Verification","author":"T. Mancini","year":"2013","unstructured":"Mancini, T., Mari, F., Massini, A., Melatti, I., Merli, F., Tronci, E.: System level formal verification via model checking driven simulation. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 296\u2013312. Springer, Heidelberg (2013)"},{"doi-asserted-by":"crossref","unstructured":"Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E.: Anytime system level verification via random exhaustive hardware in the loop simulation. In: Proc. of DSD, pp. 236\u2013245 (2014)","key":"52_CR30","DOI":"10.1109\/DSD.2014.91"},{"doi-asserted-by":"crossref","unstructured":"Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E.: System level formal verification via distributed multi-core hardware in the loop simulation. In: Proc. of PDP (2014)","key":"52_CR31","DOI":"10.1109\/PDP.2014.32"},{"doi-asserted-by":"crossref","unstructured":"Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E.: SyLVaaS: System level formal verification as a service. In: Proc. of PDP. IEEE (2015)","key":"52_CR32","DOI":"10.1109\/PDP.2015.119"},{"key":"52_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-642-14295-6_20","volume-title":"Computer Aided Verification","author":"F. Mari","year":"2010","unstructured":"Mari, F., Melatti, I., Salvo, I., Tronci, E.: Synthesis of quantized feedback control software for discrete time linear hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 180\u2013195. Springer, Heidelberg (2010)"},{"issue":"1","key":"52_CR34","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2559934","volume":"23","author":"F. Mari","year":"2014","unstructured":"Mari, F., Melatti, I., Salvo, I., Tronci, E.: Model based synthesis of control software from system level formal specifications. ACM TOSEM\u00a023(1), 1\u201342 (2014)","journal-title":"ACM TOSEM"},{"doi-asserted-by":"crossref","unstructured":"Miskov-Zivanov, N., Zuliani, P., Clarke, E.M., Faeder, J.R.: Studies of biological networks with statistical model checking: Application to immune system cells. In: Proc. of BCB, pp. 728\u2013729. ACM (2007)","key":"52_CR35","DOI":"10.1145\/2506583.2512390"},{"doi-asserted-by":"crossref","unstructured":"Phillips, J.C., Sun, Y., Jain, N., Bohm, E.J., Kal\u00e9, L.V.: Mapping to irregular torus topologies and other techniques for petascale biomolecular simulation. In: Proc. of SC14, pp. 81\u201391. IEEE (2014)","key":"52_CR36","DOI":"10.1109\/SC.2014.12"},{"issue":"15","key":"52_CR37","doi-asserted-by":"publisher","first-page":"1923","DOI":"10.1093\/bioinformatics\/btp358","volume":"25","author":"A. Raue","year":"2009","unstructured":"Raue, A., Kreutz, C., Maiwald, T., Bachmann, J., Schilling, M., Klingm\u00fcller, U., Timmer, J.: Structural and practical identifiability analysis of partially observed dynamical models by exploiting the profile likelihood. Bioinformatics\u00a025(15), 1923\u20131929 (2009)","journal-title":"Bioinformatics"},{"key":"52_CR38","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-540-88562-7_19","volume-title":"Computational Methods in Systems Biology","author":"A. Rizk","year":"2008","unstructured":"Rizk, A., Batt, G., Fages, F., Soliman, S.: On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol.\u00a05307, pp. 251\u2013268. Springer, Heidelberg (2008)"},{"key":"52_CR39","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1016\/j.jtbi.2012.11.020","volume":"321","author":"S. R\u00f6blitz","year":"2013","unstructured":"R\u00f6blitz, S., St\u00f6tzel, C., Deuflhard, P., Jones, H.M., Azulay, D.-O., van der Graaf, P., Martin, S.W.: A mathematical model of the human menstrual cycle for the administration of GnRH analogues. Journ. of Theor. Biology\u00a0321, 8\u201327 (2013)","journal-title":"Journ. of Theor. Biology"},{"unstructured":"Sebastio, S., Vandin, A.: Multivesta: statistical model checking for discrete event simulators. In: Proc. of ValueTools, pp. 310\u2013315 (2013)","key":"52_CR40"},{"key":"52_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/11513988_26","volume-title":"Computer Aided Verification","author":"K. Sen","year":"2005","unstructured":"Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 266\u2013280. Springer, Heidelberg (2005)"},{"unstructured":"Snir, M., Otto, S., Huss-Lederman, S., Walker, D., Dongarra, J.: MPI-The Complete Reference, Vol. 1: The MPI Core, 2nd edn. MIT Press (1998)","key":"52_CR42"},{"key":"52_CR43","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0577-7","volume-title":"Mathematical Control Theory: Deterministic Finite Dimensional Systems. (2nd Edition)","author":"E.D. Sontag","year":"1998","unstructured":"Sontag, E.D.: Mathematical Control Theory: Deterministic Finite Dimensional Systems (2nd Edition). Springer, New York (1998)"},{"issue":"3","key":"52_CR44","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1109\/TCBB.2011.110","volume":"9","author":"A. Streck","year":"2012","unstructured":"Streck, A., Krejci, A., Brim, L., Barnat, J., Safranek, D., Vejnar, M., Vejpustek, T.: On parameter synthesis by parallel model checking. IEEE\/ACM Trans. on Comput. Biology and Bioinf.\u00a09(3), 693\u2013705 (2012)","journal-title":"IEEE\/ACM Trans. on Comput. Biology and Bioinf."},{"issue":"1","key":"52_CR45","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1109\/TCBB.2011.67","volume":"9","author":"J. Sun","year":"2012","unstructured":"Sun, J., Garibaldi, J.M., Hodgman, C.: Parameter estimation using metaheuristics in systems biology: A comprehensive review. IEEE\/ACM Trans. Comput. Biology Bioinform.\u00a09(1), 185\u2013202 (2012)","journal-title":"IEEE\/ACM Trans. Comput. Biology Bioinform."},{"doi-asserted-by":"crossref","unstructured":"Tronci, E., Mancini, T., Mari, F., Melatti, I., Salvo, I., Prodanovic, M., Gruber, J.K., Hayes, B., Elmegaard, L.: Demand-aware price policy synthesis and verification services for smart grids. In: SmartGridComm, pp. 236\u2013245. IEEE (2014)","key":"52_CR46","DOI":"10.1109\/SmartGridComm.2014.7007745"},{"doi-asserted-by":"crossref","unstructured":"Tronci, E., Mancini, T., Salvo, I., Sinisi, S., Mari, F., Melatti, I., Massini, A., Dav\u00ec, F., Dierkes, T., Ehrig, R., R\u00f6blitz, S., Leeners, B., Kr\u00fcger, T.H.C., Egli, M., Ille, F.: Patient-specific models from inter-patient biological models and clinical records. In: Proc. of FMCAD, pp. 207\u2013214 (2014)","key":"52_CR47","DOI":"10.1109\/FMCAD.2014.6987615"},{"doi-asserted-by":"crossref","unstructured":"Vaseghi, S.V.: Advanced Digital Signal Processing and Noise Reductio. John Wiley & Sons (2006)","key":"52_CR48","DOI":"10.1002\/0470094966"},{"doi-asserted-by":"crossref","unstructured":"Wilkinson, D.J.: Stochastic Modelling for Systems Biology. Chapman & Hall (2006)","key":"52_CR49","DOI":"10.1201\/9781420010664"},{"issue":"2","key":"52_CR50","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/s10703-013-0195-3","volume":"43","author":"P. Zuliani","year":"2013","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to Stateflow\/Simulink verification. Formal Methods in System Design\u00a043(2), 338\u2013367 (2013)","journal-title":"Formal Methods in System Design"}],"container-title":["Lecture Notes in Computer Science","Bioinformatics and Biomedical Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-16480-9_52","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,3]],"date-time":"2022-05-03T00:54:57Z","timestamp":1651539297000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-16480-9_52"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319164793","9783319164809"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-16480-9_52","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}