{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,22]],"date-time":"2025-04-22T04:01:09Z","timestamp":1745294469484,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642355233"},{"type":"electronic","value":"9783642355240"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35524-0_3","type":"book-chapter","created":{"date-parts":[[2012,11,20]],"date-time":"2012-11-20T01:03:10Z","timestamp":1353373390000},"page":"53-76","source":"Crossref","is-referenced-by-count":7,"title":["Multiple Verification in Complex Biological Systems: The Bone Remodelling Case Study"],"prefix":"10.1007","author":[{"given":"Ezio","family":"Bartocci","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pietro","family":"Li\u00f2","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emanuela","family":"Merelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicola","family":"Paoletti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Akman, O.E., Guerriero, M.L., Loewe, L., Troein, C.: Complementary approaches to understanding the plant circadian clock. In: FBTC. EPTCS, vol.\u00a019, pp. 1\u201319 (2010)","DOI":"10.4204\/EPTCS.19.1"},{"issue":"1","key":"3_CR2","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A. Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM Transactions on Computational Logic\u00a01(1), 162\u2013170 (2000)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"1-3","key":"3_CR3","first-page":"13","volume":"67","author":"R. Barbuti","year":"2005","unstructured":"Barbuti, R., Cataudella, S., Maggiolo-Schettini, A., Milazzo, P., Troina, A.: A probabilistic model for molecular systems. Fundamenta Informaticae\u00a067(1-3), 13\u201327 (2005)","journal-title":"Fundamenta Informaticae"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-19835-9_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Bartocci","year":"2011","unstructured":"Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model Repair for Probabilistic Systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 326\u2013340. Springer, Heidelberg (2011)"},{"key":"3_CR5","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1109\/TAC.2007.911330","volume":"53","author":"G. Batt","year":"2008","unstructured":"Batt, G., Belta, C., Weiss, R.: Temporal logic analysis of gene networks under parameter uncertainty. IEEE Transactions on Automatic Control\u00a053, 215\u2013229 (2008)","journal-title":"IEEE Transactions on Automatic Control"},{"issue":"18","key":"3_CR6","doi-asserted-by":"publisher","first-page":"2415","DOI":"10.1093\/bioinformatics\/btm362","volume":"23","author":"G. Batt","year":"2007","unstructured":"Batt, G., Yordanov, B., Weiss, R., Belta, C.: Robustness analysis and tuning of synthetic gene networks. Bioinformatics\u00a023(18), 2415\u20132422 (2007)","journal-title":"Bioinformatics"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Belta, C., Habets, L., Kumar, V.: Control of multi-affine systems on rectangles with application to hybrid biomolecular networks. In: Proceedings of the 41st IEEE Conference on Decision and Control, pp. 534\u2013539. IEEE (2002)","DOI":"10.1109\/CDC.2002.1184551"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-540-71493-4_9","volume-title":"Hybrid Systems: Computation and Control","author":"S. Berman","year":"2007","unstructured":"Berman, S., Hal\u00e1sz, \u00c1.M., Kumar, V.: MARCO: A Reachability Algorithm for Multi-affine Systems with Applications to Biological Systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol.\u00a04416, pp. 76\u201389. Springer, Heidelberg (2007)"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Bortolussi, L., Policriti, A.: (Hybrid) automata and (stochastic) programs The hybrid automata lattice of a stochastic program. J. Logic Computation, 2052 \u2013 2077 (2010)","DOI":"10.1016\/j.tcs.2010.02.008"},{"issue":"20","key":"3_CR10","doi-asserted-by":"publisher","first-page":"2052","DOI":"10.1016\/j.tcs.2010.02.008","volume":"411","author":"L. Bortolussi","year":"2010","unstructured":"Bortolussi, L., Policriti, A.: Hybrid dynamics of stochastic programs. Theoretical Computer Science\u00a0411(20), 2052\u20132077 (2010)","journal-title":"Theoretical Computer Science"},{"key":"3_CR11","unstructured":"Cacciagrano, D.R., Corradini, F., Merelli, E., Tesei, L.: Multiscale Bone Remodelling with Spatial P Systems. In: Proceedings Compendium of the 4th Workshop on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2010), pp. 69\u201383 (2010)"},{"key":"3_CR12","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/11880646_3","volume-title":"Transactions on Computational Systems Biology VI","author":"M. Calder","year":"2006","unstructured":"Calder, M., Vyshemirsky, V., Gilbert, D., Orton, R.: Analysis of Signalling Pathways Using Continuous Time Markov Chains. In: Priami, C., Plotkin, G. (eds.) Transactions on Computational Systems Biology VI. LNCS (LNBI), vol.\u00a04220, pp. 44\u201367. Springer, Heidelberg (2006)"},{"issue":"33-34","key":"3_CR13","doi-asserted-by":"publisher","first-page":"3065","DOI":"10.1016\/j.tcs.2009.02.037","volume":"410","author":"F. Ciocchetta","year":"2009","unstructured":"Ciocchetta, F., Hillston, J.: Bio-pepa: A framework for the modelling and anal- ysis of biological systems. Theor. Comput. Sci.\u00a0410(33-34), 3065\u20133084 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-642-18275-4_11","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B. Cook","year":"2011","unstructured":"Cook, B., Fisher, J., Krepska, E., Piterman, N.: Proving Stabilization of Biological Systems. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 134\u2013149. Springer, Heidelberg (2011)"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Dayar, T., Mikeev, L., Wolf, V.: On the numerical analysis of stochastic Lotka-Volterra models. In: Proceedings of the 2010 International Multiconference on Computer Science and Information Technology (IMCSIT), pp. 289\u2013296. IEEE (2010)","DOI":"10.1109\/IMCSIT.2010.5680059"},{"issue":"4","key":"3_CR16","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1145\/1364644.1364653","volume":"35","author":"L. Dematt\u00e9","year":"2008","unstructured":"Dematt\u00e9, L., Priami, C., Romanel, A.: Modelling and simulation of biological processes in BlenX. SIGMETRICS Perform. Eval. Rev.\u00a035(4), 32\u201339 (2008)","journal-title":"SIGMETRICS Perform. Eval. Rev."},{"issue":"2","key":"3_CR17","first-page":"46","volume":"4","author":"F. Fages","year":"2004","unstructured":"Fages, F., Soliman, S., Chabrier-Rivier, N.: Modelling and querying interaction networks in the biochemical abstract machine biocham. Journal of Biological Physics and Chemistry\u00a04(2), 46\u201373 (2004)","journal-title":"Journal of Biological Physics and Chemistry"},{"issue":"1895","key":"3_CR18","doi-asserted-by":"publisher","first-page":"2011","DOI":"10.1098\/rsta.2008.0297","volume":"367","author":"F. Gerhard","year":"2009","unstructured":"Gerhard, F., Webster, D., van Lenthe, G., M\u00fcller, R.: In silico biology of bone modelling and remodelling: adaptation. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences\u00a0367(1895), 2011 (2009)","journal-title":"Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences"},{"issue":"1895","key":"3_CR19","doi-asserted-by":"publisher","first-page":"2031","DOI":"10.1098\/rsta.2008.0293","volume":"367","author":"L. Geris","year":"2009","unstructured":"Geris, L., Vander Sloten, J., Van Oosterwyck, H.: In silico biology of bone modelling and remodelling: regeneration. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences\u00a0367(1895), 2031 (2009)","journal-title":"Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences"},{"issue":"25","key":"3_CR20","doi-asserted-by":"publisher","first-page":"2340","DOI":"10.1021\/j100540a008","volume":"81","author":"D. Gillespie","year":"1977","unstructured":"Gillespie, D.: Exact stochastic simulation of coupled chemical reactions. Journal of Physical Chemistry\u00a081(25), 2340\u20132361 (1977)","journal-title":"Journal of Physical Chemistry"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-642-22110-1_31","volume-title":"Computer Aided Verification","author":"R. Grosu","year":"2011","unstructured":"Grosu, R., Batt, G., Fenton, F.H., Glimm, J., Le Guernic, C., Smolka, S.A., Bartocci, E.: From Cardiac Cells to Genetic Regulatory Networks. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 396\u2013411. Springer, Heidelberg (2011)"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"660","DOI":"10.1007\/978-3-642-14295-6_56","volume-title":"Computer Aided Verification","author":"E.M. Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PARAM: A Model Checker for Parametric Markov Models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 660\u2013664. Springer, Heidelberg (2010)"},{"issue":"2","key":"3_CR23","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1016\/S8756-3282(03)00157-1","volume":"33","author":"S. Komarova","year":"2003","unstructured":"Komarova, S., Smith, R., Dixon, S., Sims, S., Wahl, L.: Mathematical model predicts a critical role for osteoclast autocrine regulation in the control of bone remodeling. Bone\u00a033(2), 206\u2013215 (2003)","journal-title":"Bone"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-02658-4_3","volume-title":"Computer Aided Verification","author":"J. Krivine","year":"2009","unstructured":"Krivine, J., Danos, V., Benecke, A.: Modelling Epigenetic Information Maintenance: A Kappa Tutorial. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 17\u201332. Springer, Heidelberg (2009)"},{"issue":"4","key":"3_CR25","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 Performance Evaluation Review\u00a035(4), 14\u201321 (2008)","journal-title":"ACM SIGMETRICS Performance Evaluation Review"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-Time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"3_CR27","first-page":"105","volume":"3","author":"L. Li","year":"2009","unstructured":"Li, L., Yokota, H.: Application of Petri Nets in Bone Remodeling. Gene Regulation and Systems Biology\u00a03, 105 (2009)","journal-title":"Gene Regulation and Systems Biology"},{"key":"3_CR28","doi-asserted-by":"publisher","first-page":"697","DOI":"10.1109\/81.168933","volume":"39","author":"J. Lin","year":"1992","unstructured":"Lin, J., Unbehauen, R.: Canonical piecewise-linear approximations. IEEE Transactions on Circuits and Systems I: Fundamental Theory and Applications\u00a039, 697\u2013699 (1992)","journal-title":"IEEE Transactions on Circuits and Systems I: Fundamental Theory and Applications"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Li\u00f2, P., Merelli, E., Paoletti, N.: Multiple verification in computational modeling of bone pathologies. In: Proceedings of the 3rd International Workshop on Computational Models for Cell Processes (CompMod 2011), pp. 82\u201396 (2011)","DOI":"10.4204\/EPTCS.67.8"},{"key":"3_CR30","unstructured":"Voit, E.O., Ferreira, A.E.: Computational Analysis of Biochemical Systems. Cambridge University Press (2000)"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Paoletti, N., Li\u00f2, P., Merelli, E., Viceconti, M.: Osteoporosis: a multiscale mod- eling viewpoint. In: Proceedings of the 9th International Conference on Computational Methods in Systems Biology (CMSB 2011), pp. 183\u2013193. ACM (2011)","DOI":"10.1145\/2037509.2037536"},{"issue":"5","key":"3_CR32","doi-asserted-by":"publisher","first-page":"1366","DOI":"10.1109\/TCBB.2012.51","volume":"9","author":"N. Paoletti","year":"2012","unstructured":"Paoletti, N., Li\u00f2, P., Merelli, E., Viceconti, M.: Multi-level computational modeling and quantitative analysis of bone remodeling. IEEE\/ACM Transactions on Computational Biology and Bioinformatics\u00a09(5), 1366\u20131378 (2012)","journal-title":"IEEE\/ACM Transactions on Computational Biology and Bioinformatics"},{"issue":"3","key":"3_CR33","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1002\/jcb.240550303","volume":"55","author":"A. Parfitt","year":"1994","unstructured":"Parfitt, A.: Osteonal and hemi-osteonal remodeling: The spatial and temporal framework for signal traffic in adult human bone. Journal of Cellular Biochemistry\u00a055(3), 273\u2013286 (1994)","journal-title":"Journal of Cellular Biochemistry"},{"issue":"3","key":"3_CR34","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1002\/jbmr.239","volume":"26","author":"M. Parfitt","year":"2011","unstructured":"Parfitt, M., Qiu, S., Palnitkar, S., Rao, D.: Abnormal bone remodeling in patients with spontaneous painful vertebral fracture. Journal of Bone and Mineral Research\u00a026(3), 475\u2013485 (2011)","journal-title":"Journal of Bone and Mineral Research"},{"issue":"2","key":"3_CR35","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/j.bone.2010.04.601","volume":"47","author":"P. Pivonka","year":"2010","unstructured":"Pivonka, P., Komarova, S.: Mathematical modeling in bone biology: From intracellular signaling to tissue mechanics. Bone\u00a047(2), 181\u2013189 (2010)","journal-title":"Bone"},{"key":"3_CR36","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th IEEE Annual Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"3_CR37","unstructured":"Pronk, T., de Vink, E., Bo\u0161na\u010dki, D., Breit, T.: Stochastic modeling of codon bias with PRISM. In: Proceedings of the 3rd International Workshop Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems, MTCoord 2007 (2007)"},{"issue":"3","key":"3_CR38","doi-asserted-by":"crossref","first-page":"1","DOI":"10.18637\/jss.v033.i03","volume":"33","author":"K. Soetaert","year":"2010","unstructured":"Soetaert, K., Petzoldt, T., et al.: Inverse modelling, sensitivity and monte carlo analysis in R using package FME. Journal of Statistical Software\u00a033(3), 1\u201328 (2010)","journal-title":"Journal of Statistical Software"},{"key":"3_CR39","volume-title":"Introduction to the numerical solution of Markov chains","author":"W. Stewart","year":"1994","unstructured":"Stewart, W.: Introduction to the numerical solution of Markov chains. Princeton University Press, NJ (1994)"},{"key":"3_CR40","doi-asserted-by":"crossref","unstructured":"Tovar, A.: Bone remodeling as a hybrid cellular automaton optimization process. PhD thesis, University of Notre Dame (2004)","DOI":"10.2514\/6.2004-1914"},{"issue":"1","key":"3_CR41","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S1350-4533(97)00049-0","volume":"20","author":"M. Viceconti","year":"1998","unstructured":"Viceconti, M., Bellingeri, L., Cristofolini, L., Toni, A.: A comparative study on different methods of automatic mesh generation of human femurs. Medical Engineering & Physics\u00a020(1), 1\u201310 (1998)","journal-title":"Medical Engineering & Physics"},{"key":"3_CR42","doi-asserted-by":"crossref","unstructured":"Whitfield, J.: Growing bone. Landes Bioscience (2007)","DOI":"10.1201\/9781498713948"}],"container-title":["Lecture Notes in Computer Science","Transactions on Computational Systems Biology XIV"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35524-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,21]],"date-time":"2025-04-21T06:09:56Z","timestamp":1745215796000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35524-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642355233","9783642355240"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35524-0_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}