@ARTICLE{Mancini2015542,
author={Mancini, T. and Tronci, E. and Salvo, I. and Mari, F. and Massini, A. and Melatti, I.},
title={Computing biological model parameters by parallel statistical model checking},
journal={Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
year={2015},
volume={9044},
pages={542-554},
note={cited By 1; Conference of 3rd International Work-Conference on Bioinformatics and Biomedical Engineering, IWBBIO 2015 ; Conference Date: 15 April 2015 Through 17 April 2015;  Conference Code:115599},
url={https://www.scopus.com/inward/record.uri?eid=2-s2.0-84925275587&partnerID=40&md5=2cb3ff224d168ef55928e7927d8e800b},
affiliation={Computer Science Department, Sapienza University of Rome, Italy},
abstract={Biological models typically depend on many parameters. Assigning suitable values to such parameters enables model individualisation. In our clinical setting, this means finding a model for a given patient. Parameter values cannot be assigned arbitrarily, since inter-dependency constraints among them are not modelled and ignoring such constraints leads to biologically meaningless model behaviours. Classical parameter identification or estimation techniques are typically not applicable due to scarcity of clinical measurements and the huge size of parameter space. Recently, we have proposed a statistical algorithm that finds (almost) all biologically meaningful parameter values. Unfortunately, such algorithm is computationally extremely intensive, taking up to months of sequential computation. In this paper we propose a parallel algorithm designed as to be effectively executed on an arbitrary large cluster of multi-core heterogenous machines. © Springer International Publishing Switzerland 2015.},
keywords={Bioinformatics;  Biomedical engineering;  Clustering algorithms;  Model checking, Biological modeling;  Clinical measurements;  Estimation techniques;  Inter-dependencies;  Modeling behaviour;  Sequential computations;  Statistical algorithm;  Statistical model checking, Parameter estimation},
references={Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E., A map-reduce parallel approach to automatic synthesis of control software (2013) SPIN 2013. LNCS, 7976, pp. 43-60. , In: Bartocci, E., Ramakrishnan, C.R. (eds.), Springer, Heidelberg; Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E., On-the-fly control software synthesis (2013) SPIN 2013. LNCS, 7976, pp. 61-80. , In: Bartocci, E., Ramakrishnan, C.R. (eds.), Springer, Heidelberg; Alturki, M., Meseguer, J., PVeStA: A parallel statistical model checking and quantitative analysis tool (2011) CALCO 2011. LNCS, 6859, pp. 386-392. , In: Corradini, A., Klin, B., Cˆırstea, C. (eds.), Springer, Heidelberg; Ballarini, P., Forlin, M., Mazza, T., Prandi, D., Efficient parallel statistical model Checking of Biochemical Networks (2009) Proc. Of PDMC, EPCTS 2014, pp. 47-61; Ballarini, P., Guido, R., Mazza, T., Prandi, D., Taming the complexity of biological pathways through parallel computing (2009) Briefings in Bioinformatics, 10 (3), pp. 278-288; Balsa-Canto, E., Peifer, M., Banga, J.R., Timmer, J., Fleck, C., Hybrid optimization method with general switching strategy for parameter estimation (2008) BMC Systems Biology, 2, p. 26; Barnat, J., Brim, L., Cernà, I., Drazan, S., Safrànek, D., Parallel model checking large-scale genetic regulatory networks with DiVinE (2008) ENTCS, 194 (3), pp. 35-50; Barnat, J., Brim, L., Šafrànek, D., Vejnàr, M., Parameter scanning by parallel model checking with applications in systems biology (2010) Proc. Of Hibi/Pdmc, pp. 95-104. , IEEE; Chis, O.-T., Banga, J.R., Balsa-Canto, E., Structural identifiability of systems biology models: A critical comparison of methods (2011) Plos ONE, 6 (11); Della Penna, G., Intrigila, B., Tronci, E., Venturini Zilli, M., Synchronized regular expressions (2003) Acta Inf, 39 (1), pp. 31-70; Dierkes, T., Röblitz, S., Wade, M., Deuflhard, P., Parameter identification in large kinetic networks with BioPARKIN (2013) Corr, , abs; Donaldson, R., Gilbert, D., A model checking approach to the parameter estimation of biochemical pathways (2008) CMSB 2008. LNCS (LNBI), 5307, pp. 269-287. , In: Heiner, M., Uhrmacher, A.M. (eds.), Springer, Heidelberg; Ehrig, R., Nowak, U., Oeverdieck, L., Deuflhard, P., Advanced extrapolation methods for large scale differential algebraic problems (1999) High Performance Scient. And Eng. Comp. LNCSE; Gong, H., Zuliani, P., Komuravelli, A., Faeder, J.R., Clarke, E.M., Analysis and verification of the hmgb1 signaling pathway (2010) BMC Bioinform, 11 (7), p. S10; Gong, H., Zuliani, P., Komuravelli, A., Faeder, J.R., Clarke, E.M., Computational modeling and verification of signaling pathways in cancer (2012) ANB 2010. LNCS, 6479, pp. 117-135. , In: Horimoto, K., Nakatsui, M., Popov, N. (eds.), Springer, Heidelberg; Gong, H., Zuliani, P., Wang, Q., Clarke, E.M., Formal analysis for logical models of pancreatic cancer (2011) Proc. Of 50Th CDC, pp. 4855-4860. , IEEE; Grosu, R., Smolka, S.A., Quantitative model checking (2004) Preliminary Proc. Of Isola, pp. 165-174; Grosu, R., Smolka, S.A., Monte carlo model checking (2005) TACAS 2005. LNCS, 3440, pp. 271-286. , In: Halbwachs, N., Zuck, L.D. (eds.), Springer, Heidelberg; Heath, J., Kwiatkowska, M.Z., Norman, G., Parker, D., Tymchyshyn, O., Probabilistic model checking of complex biological pathways (2008) Theor. Comput. Sci, 391 (3), pp. 239-257; 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 (2012) Proc. Of 2Nd ICCABS, pp. 1-6. , IEEE; Ingalls, B., Iglesias, P., (2009) Control Theory and Systems Biology, , MIT Press; De Jong, H., Modeling and simulation of genetic regulatory systems: A literature review (2002) Journal of Computational Biology, 9, pp. 67-103; Kwiatkowska, M., Norman, G., Parker, D., Using probabilistic model checking in systems biology (2008) ACM SIGMETRICS Perf. Eval. Rev, 35 (4), pp. 14-21; Langmead, C.J., Generalized queries and bayesian statistical model checking in dynamic bayesian networks: Application to personalized medicine (2009) Proc. Of CSB, pp. 201-212; Levenberg, K., A method for the solution of certain non-linear problems in least squares (1944) The Quarterly of Applied Math, 2, pp. 164-168; Li, P., Vu, Q.D., Identification of parameter correlations for parameter estimation in dynamic biological models (2013) BMC Systems Biology, 7 (1), p. 91; Ljung, L., (1999) System Identification (2Nd Ed.): Theory for the User, , Prentice Hall PTR, Upper Saddle River; Stahl, S., Brusco, M., Branch-and-Bound Applications in Combinatorial Data Analysis (2005) Statistics and Computing, , Springer; Mancini, T., Mari, F., Massini, A., Melatti, I., Merli, F., Tronci, E., System level formal verification via model checking driven simulation (2013) CAV 2013. LNCS, 8044, pp. 296-312. , In: Sharygina, N., Veith, H. (eds.), Springer, Heidelberg; Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., Anytime system level verification via random exhaustive hardware in the loop simulation (2014) Proc. Of DSD, pp. 236-245; Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., System level formal verification via distributed multi-core hardware in the loop simulation (2014) Proc. Of PDP; Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., SyLVaaS: System level formal verification as a service (2015) Proc. Of PDP. IEEE; Mari, F., Melatti, I., Salvo, I., Tronci, E., Synthesis of quantized feedback control software for discrete time linear hybrid systems (2010) CAV 2010. LNCS, 6174, pp. 180-195. , In: Touili, T., Cook, B., Jackson, P. (eds.), Springer, Heidelberg; Mari, F., Melatti, I., Salvo, I., Tronci, E., Model based synthesis of control software from system level formal specifications (2014) ACM TOSEM, 23 (1), pp. 1-42; Miskov-Zivanov, N., Zuliani, P., Clarke, E.M., Faeder, J.R., Studies of biological networks with statistical model checking: Application to immune system cells (2007) Proc. Of BCB, pp. 728-729. , ACM; Phillips, J.C., Sun, Y., Jain, N., Bohm, E.J., Kal, L., Mapping to irregular torus topologies and other techniques for petascale biomolecular simulation (2014) Proc. Of SC14, pp. 81-91. , IEEE; Raue, A., Kreutz, C., Maiwald, T., Bachmann, J., Schilling, M., Klingmüller, U., Timmer, J., Structural and practical identifiability analysis of partially observed dynamical models by exploiting the profile likelihood (2009) Bioinformatics, 25 (15), pp. 1923-1929; Rizk, A., Batt, G., Fages, F., Soliman, S., On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology (2008) CMSB 2008. LNCS (LNBI), 5307, pp. 251-268. , In: Heiner, M., Uhrmacher, A.M. (eds.), Springer, Heidelberg; Röblitz, S., Stötzel, 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 (2013) Journ. Of Theor. Biology, 321, pp. 8-27; Sebastio, S., Vandin, A., Multivesta: Statistical model checking for discrete event simulators (2013) Proc. Of Valuetools, pp. 310-315; Sen, K., Viswanathan, M., Agha, G., On statistical model checking of stochastic systems (2005) CAV 2005. LNCS, 3576, pp. 266-280. , In: Etessami, K., Rajamani, S.K. (eds.), Springer, Heidelberg; Snir, M., Otto, S., Huss-Lederman, S., Walker, D., Dongarra, J., (1998) Mpi-The Complete Reference, 1. , The MPI Core, 2nd edn. MIT Press; Sontag, E.D., (1998) Mathematical Control Theory: Deterministic Finite Dimensional Systems, , 2nd Edition). Springer, New York; Streck, A., Krejci, A., Brim, L., Barnat, J., Safranek, D., Vejnar, M., Vejpustek, T., On parameter synthesis by parallel model checking (2012) IEEE/ACM Trans. On Comput. Biology and Bioinf, 9 (3), pp. 693-705; Sun, J., Garibaldi, J.M., Hodgman, C., Parameter estimation using metaheuristics in systems biology: A comprehensive review (2012) IEEE/ACM Trans. Comput. Biology Bioinform, 9 (1), pp. 185-202; Tronci, E., Mancini, T., Mari, F., Melatti, I., Salvo, I., Prodanovic, M., Gruber, J.K., Elmegaard, L., Demand-aware price policy synthesis and verification services for smart grids (2014) Smartgridcomm, pp. 236-245. , IEEE; Tronci, E., Mancini, T., Salvo, I., Sinisi, S., Mari, F., Melatti, I., Massini, A., Ille, F., Patient-specific models from inter-patient biological models and clinical records (2014) Proc. Of FMCAD, pp. 207-214; Vaseghi, S.V., (2006) Advanced Digital Signal Processing and Noise Reductio, , John Wiley & Sons; Wilkinson, D.J., (2006) Stochastic Modelling for Systems Biology, , Chapman & Hall; Zuliani, P., Platzer, A., Clarke, E.M., Bayesian statistical model checking with application to Stateflow/Simulink verification (2013) Formal Methods in System Design, 43 (2), pp. 338-367},
editor={Ortuno F., Rojas I},
sponsors={Algorithms for Molecular Biology; BioData Mining; BioMed Central; CITIC-UGR; E-Health Business Development BULL; Faculty of Sciences, Universidad de Granada; GigaScience; Harmonic Pharma; IEEE Computational Intelligence Society; Journal of Biomedical Semantics; Source Code for Biology and Medicine},
publisher={Springer Verlag},
issn={03029743},
isbn={9783319164793},
language={English},
abbrev_source_title={Lect. Notes Comput. Sci.},
document_type={Conference Paper},
source={Scopus},
}

{"_id":"dSexBkor3wk6ge9wZ","bibbaseid":"mancini-tronci-salvo-mari-massini-melatti-computingbiologicalmodelparametersbyparallelstatisticalmodelchecking-2015","downloads":0,"creationDate":"2016-10-14T09:18:19.792Z","title":"Computing biological model parameters by parallel statistical model checking","author_short":["Mancini, T.","Tronci, E.","Salvo, I.","Mari, F.","Massini, A.","Melatti, I."],"year":2015,"bibtype":"article","biburl":"http://mari.di.uniroma1.it/fmPubs.bib","bibdata":{"bibtype":"article","type":"article","author":[{"propositions":[],"lastnames":["Mancini"],"firstnames":["T."],"suffixes":[]},{"propositions":[],"lastnames":["Tronci"],"firstnames":["E."],"suffixes":[]},{"propositions":[],"lastnames":["Salvo"],"firstnames":["I."],"suffixes":[]},{"propositions":[],"lastnames":["Mari"],"firstnames":["F."],"suffixes":[]},{"propositions":[],"lastnames":["Massini"],"firstnames":["A."],"suffixes":[]},{"propositions":[],"lastnames":["Melatti"],"firstnames":["I."],"suffixes":[]}],"title":"Computing biological model parameters by parallel statistical model checking","journal":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","year":"2015","volume":"9044","pages":"542-554","note":"cited By 1; Conference of 3rd International Work-Conference on Bioinformatics and Biomedical Engineering, IWBBIO 2015 ; Conference Date: 15 April 2015 Through 17 April 2015; Conference Code:115599","url":"https://www.scopus.com/inward/record.uri?eid=2-s2.0-84925275587&partnerID=40&md5=2cb3ff224d168ef55928e7927d8e800b","affiliation":"Computer Science Department, Sapienza University of Rome, Italy","abstract":"Biological models typically depend on many parameters. Assigning suitable values to such parameters enables model individualisation. In our clinical setting, this means finding a model for a given patient. Parameter values cannot be assigned arbitrarily, since inter-dependency constraints among them are not modelled and ignoring such constraints leads to biologically meaningless model behaviours. Classical parameter identification or estimation techniques are typically not applicable due to scarcity of clinical measurements and the huge size of parameter space. Recently, we have proposed a statistical algorithm that finds (almost) all biologically meaningful parameter values. Unfortunately, such algorithm is computationally extremely intensive, taking up to months of sequential computation. In this paper we propose a parallel algorithm designed as to be effectively executed on an arbitrary large cluster of multi-core heterogenous machines. © Springer International Publishing Switzerland 2015.","keywords":"Bioinformatics; Biomedical engineering; Clustering algorithms; Model checking, Biological modeling; Clinical measurements; Estimation techniques; Inter-dependencies; Modeling behaviour; Sequential computations; Statistical algorithm; Statistical model checking, Parameter estimation","references":"Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E., A map-reduce parallel approach to automatic synthesis of control software (2013) SPIN 2013. LNCS, 7976, pp. 43-60. , In: Bartocci, E., Ramakrishnan, C.R. (eds.), Springer, Heidelberg; Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E., On-the-fly control software synthesis (2013) SPIN 2013. LNCS, 7976, pp. 61-80. , In: Bartocci, E., Ramakrishnan, C.R. (eds.), Springer, Heidelberg; Alturki, M., Meseguer, J., PVeStA: A parallel statistical model checking and quantitative analysis tool (2011) CALCO 2011. LNCS, 6859, pp. 386-392. , In: Corradini, A., Klin, B., Cˆırstea, C. (eds.), Springer, Heidelberg; Ballarini, P., Forlin, M., Mazza, T., Prandi, D., Efficient parallel statistical model Checking of Biochemical Networks (2009) Proc. Of PDMC, EPCTS 2014, pp. 47-61; Ballarini, P., Guido, R., Mazza, T., Prandi, D., Taming the complexity of biological pathways through parallel computing (2009) Briefings in Bioinformatics, 10 (3), pp. 278-288; Balsa-Canto, E., Peifer, M., Banga, J.R., Timmer, J., Fleck, C., Hybrid optimization method with general switching strategy for parameter estimation (2008) BMC Systems Biology, 2, p. 26; Barnat, J., Brim, L., Cernà, I., Drazan, S., Safrànek, D., Parallel model checking large-scale genetic regulatory networks with DiVinE (2008) ENTCS, 194 (3), pp. 35-50; Barnat, J., Brim, L., Šafrànek, D., Vejnàr, M., Parameter scanning by parallel model checking with applications in systems biology (2010) Proc. Of Hibi/Pdmc, pp. 95-104. , IEEE; Chis, O.-T., Banga, J.R., Balsa-Canto, E., Structural identifiability of systems biology models: A critical comparison of methods (2011) Plos ONE, 6 (11); Della Penna, G., Intrigila, B., Tronci, E., Venturini Zilli, M., Synchronized regular expressions (2003) Acta Inf, 39 (1), pp. 31-70; Dierkes, T., Röblitz, S., Wade, M., Deuflhard, P., Parameter identification in large kinetic networks with BioPARKIN (2013) Corr, , abs; Donaldson, R., Gilbert, D., A model checking approach to the parameter estimation of biochemical pathways (2008) CMSB 2008. LNCS (LNBI), 5307, pp. 269-287. , In: Heiner, M., Uhrmacher, A.M. (eds.), Springer, Heidelberg; Ehrig, R., Nowak, U., Oeverdieck, L., Deuflhard, P., Advanced extrapolation methods for large scale differential algebraic problems (1999) High Performance Scient. And Eng. Comp. LNCSE; Gong, H., Zuliani, P., Komuravelli, A., Faeder, J.R., Clarke, E.M., Analysis and verification of the hmgb1 signaling pathway (2010) BMC Bioinform, 11 (7), p. S10; Gong, H., Zuliani, P., Komuravelli, A., Faeder, J.R., Clarke, E.M., Computational modeling and verification of signaling pathways in cancer (2012) ANB 2010. LNCS, 6479, pp. 117-135. , In: Horimoto, K., Nakatsui, M., Popov, N. (eds.), Springer, Heidelberg; Gong, H., Zuliani, P., Wang, Q., Clarke, E.M., Formal analysis for logical models of pancreatic cancer (2011) Proc. Of 50Th CDC, pp. 4855-4860. , IEEE; Grosu, R., Smolka, S.A., Quantitative model checking (2004) Preliminary Proc. Of Isola, pp. 165-174; Grosu, R., Smolka, S.A., Monte carlo model checking (2005) TACAS 2005. LNCS, 3440, pp. 271-286. , In: Halbwachs, N., Zuck, L.D. (eds.), Springer, Heidelberg; Heath, J., Kwiatkowska, M.Z., Norman, G., Parker, D., Tymchyshyn, O., Probabilistic model checking of complex biological pathways (2008) Theor. Comput. Sci, 391 (3), pp. 239-257; 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 (2012) Proc. Of 2Nd ICCABS, pp. 1-6. , IEEE; Ingalls, B., Iglesias, P., (2009) Control Theory and Systems Biology, , MIT Press; De Jong, H., Modeling and simulation of genetic regulatory systems: A literature review (2002) Journal of Computational Biology, 9, pp. 67-103; Kwiatkowska, M., Norman, G., Parker, D., Using probabilistic model checking in systems biology (2008) ACM SIGMETRICS Perf. Eval. Rev, 35 (4), pp. 14-21; Langmead, C.J., Generalized queries and bayesian statistical model checking in dynamic bayesian networks: Application to personalized medicine (2009) Proc. Of CSB, pp. 201-212; Levenberg, K., A method for the solution of certain non-linear problems in least squares (1944) The Quarterly of Applied Math, 2, pp. 164-168; Li, P., Vu, Q.D., Identification of parameter correlations for parameter estimation in dynamic biological models (2013) BMC Systems Biology, 7 (1), p. 91; Ljung, L., (1999) System Identification (2Nd Ed.): Theory for the User, , Prentice Hall PTR, Upper Saddle River; Stahl, S., Brusco, M., Branch-and-Bound Applications in Combinatorial Data Analysis (2005) Statistics and Computing, , Springer; Mancini, T., Mari, F., Massini, A., Melatti, I., Merli, F., Tronci, E., System level formal verification via model checking driven simulation (2013) CAV 2013. LNCS, 8044, pp. 296-312. , In: Sharygina, N., Veith, H. (eds.), Springer, Heidelberg; Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., Anytime system level verification via random exhaustive hardware in the loop simulation (2014) Proc. Of DSD, pp. 236-245; Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., System level formal verification via distributed multi-core hardware in the loop simulation (2014) Proc. Of PDP; Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., SyLVaaS: System level formal verification as a service (2015) Proc. Of PDP. IEEE; Mari, F., Melatti, I., Salvo, I., Tronci, E., Synthesis of quantized feedback control software for discrete time linear hybrid systems (2010) CAV 2010. LNCS, 6174, pp. 180-195. , In: Touili, T., Cook, B., Jackson, P. (eds.), Springer, Heidelberg; Mari, F., Melatti, I., Salvo, I., Tronci, E., Model based synthesis of control software from system level formal specifications (2014) ACM TOSEM, 23 (1), pp. 1-42; Miskov-Zivanov, N., Zuliani, P., Clarke, E.M., Faeder, J.R., Studies of biological networks with statistical model checking: Application to immune system cells (2007) Proc. Of BCB, pp. 728-729. , ACM; Phillips, J.C., Sun, Y., Jain, N., Bohm, E.J., Kal, L., Mapping to irregular torus topologies and other techniques for petascale biomolecular simulation (2014) Proc. Of SC14, pp. 81-91. , IEEE; Raue, A., Kreutz, C., Maiwald, T., Bachmann, J., Schilling, M., Klingmüller, U., Timmer, J., Structural and practical identifiability analysis of partially observed dynamical models by exploiting the profile likelihood (2009) Bioinformatics, 25 (15), pp. 1923-1929; Rizk, A., Batt, G., Fages, F., Soliman, S., On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology (2008) CMSB 2008. LNCS (LNBI), 5307, pp. 251-268. , In: Heiner, M., Uhrmacher, A.M. (eds.), Springer, Heidelberg; Röblitz, S., Stötzel, 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 (2013) Journ. Of Theor. Biology, 321, pp. 8-27; Sebastio, S., Vandin, A., Multivesta: Statistical model checking for discrete event simulators (2013) Proc. Of Valuetools, pp. 310-315; Sen, K., Viswanathan, M., Agha, G., On statistical model checking of stochastic systems (2005) CAV 2005. LNCS, 3576, pp. 266-280. , In: Etessami, K., Rajamani, S.K. (eds.), Springer, Heidelberg; Snir, M., Otto, S., Huss-Lederman, S., Walker, D., Dongarra, J., (1998) Mpi-The Complete Reference, 1. , The MPI Core, 2nd edn. MIT Press; Sontag, E.D., (1998) Mathematical Control Theory: Deterministic Finite Dimensional Systems, , 2nd Edition). Springer, New York; Streck, A., Krejci, A., Brim, L., Barnat, J., Safranek, D., Vejnar, M., Vejpustek, T., On parameter synthesis by parallel model checking (2012) IEEE/ACM Trans. On Comput. Biology and Bioinf, 9 (3), pp. 693-705; Sun, J., Garibaldi, J.M., Hodgman, C., Parameter estimation using metaheuristics in systems biology: A comprehensive review (2012) IEEE/ACM Trans. Comput. Biology Bioinform, 9 (1), pp. 185-202; Tronci, E., Mancini, T., Mari, F., Melatti, I., Salvo, I., Prodanovic, M., Gruber, J.K., Elmegaard, L., Demand-aware price policy synthesis and verification services for smart grids (2014) Smartgridcomm, pp. 236-245. , IEEE; Tronci, E., Mancini, T., Salvo, I., Sinisi, S., Mari, F., Melatti, I., Massini, A., Ille, F., Patient-specific models from inter-patient biological models and clinical records (2014) Proc. Of FMCAD, pp. 207-214; Vaseghi, S.V., (2006) Advanced Digital Signal Processing and Noise Reductio, , John Wiley & Sons; Wilkinson, D.J., (2006) Stochastic Modelling for Systems Biology, , Chapman & Hall; Zuliani, P., Platzer, A., Clarke, E.M., Bayesian statistical model checking with application to Stateflow/Simulink verification (2013) Formal Methods in System Design, 43 (2), pp. 338-367","editor":[{"propositions":[],"lastnames":["Ortuno","F."],"firstnames":["Rojas","I"],"suffixes":[]}],"sponsors":"Algorithms for Molecular Biology; BioData Mining; BioMed Central; CITIC-UGR; E-Health Business Development BULL; Faculty of Sciences, Universidad de Granada; GigaScience; Harmonic Pharma; IEEE Computational Intelligence Society; Journal of Biomedical Semantics; Source Code for Biology and Medicine","publisher":"Springer Verlag","issn":"03029743","isbn":"9783319164793","language":"English","abbrev_source_title":"Lect. Notes Comput. Sci.","document_type":"Conference Paper","source":"Scopus","bibtex":"@ARTICLE{Mancini2015542,\nauthor={Mancini, T. and Tronci, E. and Salvo, I. and Mari, F. and Massini, A. and Melatti, I.},\ntitle={Computing biological model parameters by parallel statistical model checking},\njournal={Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},\nyear={2015},\nvolume={9044},\npages={542-554},\nnote={cited By 1; Conference of 3rd International Work-Conference on Bioinformatics and Biomedical Engineering, IWBBIO 2015 ; Conference Date: 15 April 2015 Through 17 April 2015; Conference Code:115599},\nurl={https://www.scopus.com/inward/record.uri?eid=2-s2.0-84925275587&partnerID=40&md5=2cb3ff224d168ef55928e7927d8e800b},\naffiliation={Computer Science Department, Sapienza University of Rome, Italy},\nabstract={Biological models typically depend on many parameters. Assigning suitable values to such parameters enables model individualisation. In our clinical setting, this means finding a model for a given patient. Parameter values cannot be assigned arbitrarily, since inter-dependency constraints among them are not modelled and ignoring such constraints leads to biologically meaningless model behaviours. Classical parameter identification or estimation techniques are typically not applicable due to scarcity of clinical measurements and the huge size of parameter space. Recently, we have proposed a statistical algorithm that finds (almost) all biologically meaningful parameter values. Unfortunately, such algorithm is computationally extremely intensive, taking up to months of sequential computation. In this paper we propose a parallel algorithm designed as to be effectively executed on an arbitrary large cluster of multi-core heterogenous machines. © Springer International Publishing Switzerland 2015.},\nkeywords={Bioinformatics; Biomedical engineering; Clustering algorithms; Model checking, Biological modeling; Clinical measurements; Estimation techniques; Inter-dependencies; Modeling behaviour; Sequential computations; Statistical algorithm; Statistical model checking, Parameter estimation},\nreferences={Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E., A map-reduce parallel approach to automatic synthesis of control software (2013) SPIN 2013. LNCS, 7976, pp. 43-60. , In: Bartocci, E., Ramakrishnan, C.R. (eds.), Springer, Heidelberg; Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E., On-the-fly control software synthesis (2013) SPIN 2013. LNCS, 7976, pp. 61-80. , In: Bartocci, E., Ramakrishnan, C.R. (eds.), Springer, Heidelberg; Alturki, M., Meseguer, J., PVeStA: A parallel statistical model checking and quantitative analysis tool (2011) CALCO 2011. LNCS, 6859, pp. 386-392. , In: Corradini, A., Klin, B., Cˆırstea, C. (eds.), Springer, Heidelberg; Ballarini, P., Forlin, M., Mazza, T., Prandi, D., Efficient parallel statistical model Checking of Biochemical Networks (2009) Proc. Of PDMC, EPCTS 2014, pp. 47-61; Ballarini, P., Guido, R., Mazza, T., Prandi, D., Taming the complexity of biological pathways through parallel computing (2009) Briefings in Bioinformatics, 10 (3), pp. 278-288; Balsa-Canto, E., Peifer, M., Banga, J.R., Timmer, J., Fleck, C., Hybrid optimization method with general switching strategy for parameter estimation (2008) BMC Systems Biology, 2, p. 26; Barnat, J., Brim, L., Cernà, I., Drazan, S., Safrànek, D., Parallel model checking large-scale genetic regulatory networks with DiVinE (2008) ENTCS, 194 (3), pp. 35-50; Barnat, J., Brim, L., Šafrànek, D., Vejnàr, M., Parameter scanning by parallel model checking with applications in systems biology (2010) Proc. Of Hibi/Pdmc, pp. 95-104. , IEEE; Chis, O.-T., Banga, J.R., Balsa-Canto, E., Structural identifiability of systems biology models: A critical comparison of methods (2011) Plos ONE, 6 (11); Della Penna, G., Intrigila, B., Tronci, E., Venturini Zilli, M., Synchronized regular expressions (2003) Acta Inf, 39 (1), pp. 31-70; Dierkes, T., Röblitz, S., Wade, M., Deuflhard, P., Parameter identification in large kinetic networks with BioPARKIN (2013) Corr, , abs; Donaldson, R., Gilbert, D., A model checking approach to the parameter estimation of biochemical pathways (2008) CMSB 2008. LNCS (LNBI), 5307, pp. 269-287. , In: Heiner, M., Uhrmacher, A.M. (eds.), Springer, Heidelberg; Ehrig, R., Nowak, U., Oeverdieck, L., Deuflhard, P., Advanced extrapolation methods for large scale differential algebraic problems (1999) High Performance Scient. And Eng. Comp. LNCSE; Gong, H., Zuliani, P., Komuravelli, A., Faeder, J.R., Clarke, E.M., Analysis and verification of the hmgb1 signaling pathway (2010) BMC Bioinform, 11 (7), p. S10; Gong, H., Zuliani, P., Komuravelli, A., Faeder, J.R., Clarke, E.M., Computational modeling and verification of signaling pathways in cancer (2012) ANB 2010. LNCS, 6479, pp. 117-135. , In: Horimoto, K., Nakatsui, M., Popov, N. (eds.), Springer, Heidelberg; Gong, H., Zuliani, P., Wang, Q., Clarke, E.M., Formal analysis for logical models of pancreatic cancer (2011) Proc. Of 50Th CDC, pp. 4855-4860. , IEEE; Grosu, R., Smolka, S.A., Quantitative model checking (2004) Preliminary Proc. Of Isola, pp. 165-174; Grosu, R., Smolka, S.A., Monte carlo model checking (2005) TACAS 2005. LNCS, 3440, pp. 271-286. , In: Halbwachs, N., Zuck, L.D. (eds.), Springer, Heidelberg; Heath, J., Kwiatkowska, M.Z., Norman, G., Parker, D., Tymchyshyn, O., Probabilistic model checking of complex biological pathways (2008) Theor. Comput. Sci, 391 (3), pp. 239-257; 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 (2012) Proc. Of 2Nd ICCABS, pp. 1-6. , IEEE; Ingalls, B., Iglesias, P., (2009) Control Theory and Systems Biology, , MIT Press; De Jong, H., Modeling and simulation of genetic regulatory systems: A literature review (2002) Journal of Computational Biology, 9, pp. 67-103; Kwiatkowska, M., Norman, G., Parker, D., Using probabilistic model checking in systems biology (2008) ACM SIGMETRICS Perf. Eval. Rev, 35 (4), pp. 14-21; Langmead, C.J., Generalized queries and bayesian statistical model checking in dynamic bayesian networks: Application to personalized medicine (2009) Proc. Of CSB, pp. 201-212; Levenberg, K., A method for the solution of certain non-linear problems in least squares (1944) The Quarterly of Applied Math, 2, pp. 164-168; Li, P., Vu, Q.D., Identification of parameter correlations for parameter estimation in dynamic biological models (2013) BMC Systems Biology, 7 (1), p. 91; Ljung, L., (1999) System Identification (2Nd Ed.): Theory for the User, , Prentice Hall PTR, Upper Saddle River; Stahl, S., Brusco, M., Branch-and-Bound Applications in Combinatorial Data Analysis (2005) Statistics and Computing, , Springer; Mancini, T., Mari, F., Massini, A., Melatti, I., Merli, F., Tronci, E., System level formal verification via model checking driven simulation (2013) CAV 2013. LNCS, 8044, pp. 296-312. , In: Sharygina, N., Veith, H. (eds.), Springer, Heidelberg; Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., Anytime system level verification via random exhaustive hardware in the loop simulation (2014) Proc. Of DSD, pp. 236-245; Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., System level formal verification via distributed multi-core hardware in the loop simulation (2014) Proc. Of PDP; Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., SyLVaaS: System level formal verification as a service (2015) Proc. Of PDP. IEEE; Mari, F., Melatti, I., Salvo, I., Tronci, E., Synthesis of quantized feedback control software for discrete time linear hybrid systems (2010) CAV 2010. LNCS, 6174, pp. 180-195. , In: Touili, T., Cook, B., Jackson, P. (eds.), Springer, Heidelberg; Mari, F., Melatti, I., Salvo, I., Tronci, E., Model based synthesis of control software from system level formal specifications (2014) ACM TOSEM, 23 (1), pp. 1-42; Miskov-Zivanov, N., Zuliani, P., Clarke, E.M., Faeder, J.R., Studies of biological networks with statistical model checking: Application to immune system cells (2007) Proc. Of BCB, pp. 728-729. , ACM; Phillips, J.C., Sun, Y., Jain, N., Bohm, E.J., Kal, L., Mapping to irregular torus topologies and other techniques for petascale biomolecular simulation (2014) Proc. Of SC14, pp. 81-91. , IEEE; Raue, A., Kreutz, C., Maiwald, T., Bachmann, J., Schilling, M., Klingmüller, U., Timmer, J., Structural and practical identifiability analysis of partially observed dynamical models by exploiting the profile likelihood (2009) Bioinformatics, 25 (15), pp. 1923-1929; Rizk, A., Batt, G., Fages, F., Soliman, S., On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology (2008) CMSB 2008. LNCS (LNBI), 5307, pp. 251-268. , In: Heiner, M., Uhrmacher, A.M. (eds.), Springer, Heidelberg; Röblitz, S., Stötzel, 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 (2013) Journ. Of Theor. Biology, 321, pp. 8-27; Sebastio, S., Vandin, A., Multivesta: Statistical model checking for discrete event simulators (2013) Proc. Of Valuetools, pp. 310-315; Sen, K., Viswanathan, M., Agha, G., On statistical model checking of stochastic systems (2005) CAV 2005. LNCS, 3576, pp. 266-280. , In: Etessami, K., Rajamani, S.K. (eds.), Springer, Heidelberg; Snir, M., Otto, S., Huss-Lederman, S., Walker, D., Dongarra, J., (1998) Mpi-The Complete Reference, 1. , The MPI Core, 2nd edn. MIT Press; Sontag, E.D., (1998) Mathematical Control Theory: Deterministic Finite Dimensional Systems, , 2nd Edition). Springer, New York; Streck, A., Krejci, A., Brim, L., Barnat, J., Safranek, D., Vejnar, M., Vejpustek, T., On parameter synthesis by parallel model checking (2012) IEEE/ACM Trans. On Comput. Biology and Bioinf, 9 (3), pp. 693-705; Sun, J., Garibaldi, J.M., Hodgman, C., Parameter estimation using metaheuristics in systems biology: A comprehensive review (2012) IEEE/ACM Trans. Comput. Biology Bioinform, 9 (1), pp. 185-202; Tronci, E., Mancini, T., Mari, F., Melatti, I., Salvo, I., Prodanovic, M., Gruber, J.K., Elmegaard, L., Demand-aware price policy synthesis and verification services for smart grids (2014) Smartgridcomm, pp. 236-245. , IEEE; Tronci, E., Mancini, T., Salvo, I., Sinisi, S., Mari, F., Melatti, I., Massini, A., Ille, F., Patient-specific models from inter-patient biological models and clinical records (2014) Proc. Of FMCAD, pp. 207-214; Vaseghi, S.V., (2006) Advanced Digital Signal Processing and Noise Reductio, , John Wiley & Sons; Wilkinson, D.J., (2006) Stochastic Modelling for Systems Biology, , Chapman & Hall; Zuliani, P., Platzer, A., Clarke, E.M., Bayesian statistical model checking with application to Stateflow/Simulink verification (2013) Formal Methods in System Design, 43 (2), pp. 338-367},\neditor={Ortuno F., Rojas I},\nsponsors={Algorithms for Molecular Biology; BioData Mining; BioMed Central; CITIC-UGR; E-Health Business Development BULL; Faculty of Sciences, Universidad de Granada; GigaScience; Harmonic Pharma; IEEE Computational Intelligence Society; Journal of Biomedical Semantics; Source Code for Biology and Medicine},\npublisher={Springer Verlag},\nissn={03029743},\nisbn={9783319164793},\nlanguage={English},\nabbrev_source_title={Lect. Notes Comput. Sci.},\ndocument_type={Conference Paper},\nsource={Scopus},\n}\n\n","author_short":["Mancini, T.","Tronci, E.","Salvo, I.","Mari, F.","Massini, A.","Melatti, I."],"editor_short":["Ortuno F., R. I"],"key":"Mancini2015542","id":"Mancini2015542","bibbaseid":"mancini-tronci-salvo-mari-massini-melatti-computingbiologicalmodelparametersbyparallelstatisticalmodelchecking-2015","role":"author","urls":{"Paper":"https://www.scopus.com/inward/record.uri?eid=2-s2.0-84925275587&partnerID=40&md5=2cb3ff224d168ef55928e7927d8e800b"},"keyword":["Bioinformatics; Biomedical engineering; Clustering algorithms; Model checking","Biological modeling; Clinical measurements; Estimation techniques; Inter-dependencies; Modeling behaviour; Sequential computations; Statistical algorithm; Statistical model checking","Parameter estimation"],"downloads":0},"search_terms":["computing","biological","model","parameters","parallel","statistical","model","checking","mancini","tronci","salvo","mari","massini","melatti"],"keywords":["bioinformatics; biomedical engineering; clustering algorithms; model checking","biological modeling; clinical measurements; estimation techniques; inter-dependencies; modeling behaviour; sequential computations; statistical algorithm; statistical model checking","parameter estimation"],"authorIDs":["5800a2dbaf110b6716000017"],"dataSources":["L3NrffcQCrJ5r6svQ"]}