{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:16:05Z","timestamp":1748751365190,"version":"3.41.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319269153"},{"type":"electronic","value":"9783319269160"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-26916-0_7","type":"book-chapter","created":{"date-parts":[[2016,1,9]],"date-time":"2016-01-09T05:44:21Z","timestamp":1452318261000},"page":"119-140","source":"Crossref","is-referenced-by-count":9,"title":["Synthesising Robust and Optimal Parameters for Cardiac Pacemakers Using Symbolic and Evolutionary Computation Techniques"],"prefix":"10.1007","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandru","family":"Mereacre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicola","family":"Paoletti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Patan\u00e8","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,1,10]]},"reference":[{"issue":"05","key":"7_CR1","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1142\/S0129054109006905","volume":"20","author":"\u00c9 Andr\u00e9","year":"2009","unstructured":"Andr\u00e9, \u00c9., Chatain, T., Fribourg, L., Encrenaz, E.: An inverse method for parametric timed automata. Int. J. Found. Comput. Sci. 20(05), 819\u2013836 (2009)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-15349-5_5","volume-title":"Reachability Problems","author":"\u00c9 Andr\u00e9","year":"2010","unstructured":"Andr\u00e9, \u00c9., Fribourg, L.: Behavioral cartography of timed automata. In: Ku\u010dera, A., Potapov, I. (eds.) Reachability Problems. LNCS, vol. 6227, pp. 76\u201390. Springer, Heidelberg (2010)"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Arai, T., Lee, K., Cohen, R.J.: Cardiac output and stroke volume estimation using a hybrid of three windkessel models. In: EMBC, pp. 4971\u20134974. IEEE (2010)","DOI":"10.1109\/IEMBS.2010.5627225"},{"issue":"1","key":"7_CR4","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10009-008-0091-0","volume":"11","author":"A Armando","year":"2009","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. STTT 11(1), 69\u201383 (2009)","journal-title":"STTT"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-23401-4_1","volume-title":"Computational Methods in Systems Biology","author":"B Barbot","year":"2015","unstructured":"Barbot, B., Kwiatkowska, M., Mereacre, A., Paoletti, N.: Estimation and verification of hybrid heart models for personalised medical and wearable devices. In: Roux, O., Bourdon, J. (eds.) CMSB 2015. LNCS, vol. 9308, pp. 3\u20137. Springer, Heidelberg (2015)"},{"issue":"1","key":"7_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1023\/A:1015059928466","volume":"1","author":"H-G Beyer","year":"2002","unstructured":"Beyer, H.-G., Schwefel, H.-P.: Evolution strategies-a comprehensive introduction. Nat. Comput. 1(1), 3\u201352 (2002)","journal-title":"Nat. Comput."},{"issue":"2","key":"7_CR7","first-page":"121","volume":"35","author":"L Bozzelli","year":"2009","unstructured":"Bozzelli, L., La Torre, S.: Decision problems for lower\/upper bound parametric timed automata. FMSD 35(2), 121\u2013151 (2009)","journal-title":"FMSD"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-540-24597-1_9","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"V Bruy\u00e8re","year":"2003","unstructured":"Bruy\u00e8re, V., Raskin, J.-F.: Real-time model-checking: parameters everywhere. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 100\u2013111. Springer, Heidelberg (2003)"},{"key":"7_CR9","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/j.ic.2014.01.014","volume":"236","author":"T Chen","year":"2014","unstructured":"Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Quantitative verification of implantable cardiac pacemakers over hybrid heart models. Inf. Comput. 236, 87\u2013101 (2014)","journal-title":"Inf. Comput."},{"key":"7_CR10","unstructured":"Cimatti, A., Mover, S., Tonetta, S.: SMT-based verification of hybrid systems. In: Hoffmann, J., Selman, B. (eds.) Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence, 22\u201326 July 2012, Toronto, Ontario, Canada. AAAI Press (2012)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)"},{"issue":"1","key":"7_CR12","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/s10479-007-0176-2","volume":"153","author":"B Colson","year":"2007","unstructured":"Colson, B., Marcotte, P., Savard, G.: An overview of bilevel optimization. Ann. Oper. Res. 153(1), 235\u2013256 (2007)","journal-title":"Ann. Oper. Res."},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"2","key":"7_CR14","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/S0045-7825(99)00389-8","volume":"186","author":"K Deb","year":"2000","unstructured":"Deb, K.: An efficient constraint handling method for genetic algorithms. Comput. Methods Appl. Mech. Eng. 186(2), 311\u2013338 (2000)","journal-title":"Comput. Methods Appl. Mech. Eng."},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Diciolla, M., Kim, C.H.P., Kwiatkowska, M., Mereacre, A.: Synthesising optimal timing delays for timed I\/O automata. In: EMSOFT 2014. ACM (2014)","DOI":"10.1145\/2656045.2656073"},{"issue":"5","key":"7_CR16","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1016\/j.ipl.2006.11.018","volume":"102","author":"L Doyen","year":"2007","unstructured":"Doyen, L.: Robust parametric reachability for timed automata. Inf. Process. Lett. 102(5), 208\u2013213 (2007)","journal-title":"Inf. Process. Lett."},{"key":"7_CR17","doi-asserted-by":"publisher","first-page":"736","DOI":"10.3389\/fphys.2012.00298","volume":"3","author":"N Fazeli","year":"2012","unstructured":"Fazeli, N., Hahn, J.-O.: Estimation of cardiac output and peripheral resistance using square-wave-approximated aortic flow signal. Front. Physiol 3, 736\u2013743 (2012)","journal-title":"Front. Physiol"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Gao, S., Kong, S., Clarke, E.M.: Satisfiability modulo ODEs. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 105\u2013112. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679398"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-642-05089-3_44","volume-title":"FM 2009: Formal Methods","author":"AO Gomes","year":"2009","unstructured":"Gomes, A.O., Oliveira, M.V.M.: Formal specification of a cardiac pacing system. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 692\u2013707. Springer, Heidelberg (2009)"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-540-70545-1_18","volume-title":"Computer Aided Verification","author":"S Gulwani","year":"2008","unstructured":"Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 190\u2013203. Springer, Heidelberg (2008)"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-28756-5_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Z Jiang","year":"2012","unstructured":"Jiang, Z., Pajic, M., Moarref, S., Alur, R., Mangharam, R.: Modeling and verification of a dual chamber implantable pacemaker. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 188\u2013203. Springer, Heidelberg (2012)"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/978-3-319-11439-2_14","volume-title":"Reachability Problems","author":"A Jovanovi\u0107","year":"2014","unstructured":"Jovanovi\u0107, A., Kwiatkowska, M.: Parameter synthesis for probabilistic timed automata using stochastic game abstractions. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 176\u2013189. Springer, Heidelberg (2014)"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-642-36742-7_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Jovanovi\u0107","year":"2013","unstructured":"Jovanovi\u0107, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 401\u2013415. Springer, Heidelberg (2013)"},{"key":"7_CR24","unstructured":"Kerner, D.R.: Solving windkessel models with mlab (2007). http:\/\/www.civilized.com\/mlabexamples\/windkesmodel.htmld"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-30793-5_6","volume-title":"Formal Techniques for Distributed Systems","author":"R Kindermann","year":"2012","unstructured":"Kindermann, R., Junttila, T., Niemel\u00e4, I.: Beyond lassos: complete SMT-based bounded model checking for timed automata. In: Giese, H., Rosu, G. (eds.) FORTE 2012 and FMOODS 2012. LNCS, vol. 7273, pp. 84\u2013100. Springer, Heidelberg (2012)"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-33365-1_13","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"R Kindermann","year":"2012","unstructured":"Kindermann, R., Junttila, T., Niemel\u00e4, I.: SMT-based induction methods for timed systems. In: Jurdzi\u0144ski, M., Ni\u010dkovi\u0107, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 171\u2013187. Springer, Heidelberg (2012)"},{"key":"7_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-29072-5_6","volume-title":"Transactions on Petri Nets and Other Models of Concurrency V","author":"M Knapik","year":"2012","unstructured":"Knapik, M., Penczek, W.: Bounded model checking for parametric timed automata. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) ToPNoC V. LNCS, vol. 6900, pp. 141\u2013159. Springer, Heidelberg (2012)"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Kov\u00e1sznai, G., Fr\u00f6hlich, A., Biere, A.: On the complexity of fixed-size bit-vector logics with binary encoded bit-width. In: SMT, pp. 44\u201356 (2012)","DOI":"10.1007\/978-3-642-38536-0_33"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Lea-Banks, H., Mereacre, A., Paoletti, N.: Formal modelling and validation of rate-adaptive pacemakers. In: ICHI, pp. 23\u201332. IEEE (2014)","DOI":"10.1109\/ICHI.2014.11"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Mereacre, A., Paoletti, N., Patan\u00e8, A.: Synthesising robust and optimal parameters for cardiac pacemakers using symbolic and evolutionary computation techniques. Technical Report RR-15-09, Department of Computer Science, University of Oxford (2015)","DOI":"10.1007\/978-3-319-26916-0_7"},{"key":"7_CR31","first-page":"4","volume":"3","author":"J Lian","year":"2010","unstructured":"Lian, J., Kr\u00e4tschmer, H., M\u00fcssig, D., Stotts, L.: Open source modeling of heart rhythm and cardiac pacing. Open Pacing Electrophysiol. Ther. J. 3, 4 (2010)","journal-title":"Open Pacing Electrophysiol. Ther. J."},{"key":"7_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-39088-3_10","volume-title":"Foundations of Health Information Engineering and Systems","author":"D M\u00e9ry","year":"2013","unstructured":"M\u00e9ry, D., Singh, N.K.: Closed-loop modeling of cardiac pacemaker and heart. In: Weber, J., Perseil, I. (eds.) FHIES 2012. LNCS, vol. 7789, pp. 151\u2013166. Springer, Heidelberg (2013)"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, LICS 2005, pp. 188\u2013197. IEEE (2005)","DOI":"10.1109\/LICS.2005.33"},{"issue":"22","key":"7_CR34","doi-asserted-by":"publisher","first-page":"2331","DOI":"10.1016\/j.tcs.2010.03.017","volume":"411","author":"A Rabinovich","year":"2010","unstructured":"Rabinovich, A.: Complexity of metric temporal logics with counting and the pnueli modalities. Theor. Comput. Sci. 411(22), 2331\u20132342 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/3-540-58484-6_258","volume-title":"Parallel Problem Solving from Nature \u2013 PPSN III","author":"G Rudolph","year":"1994","unstructured":"Rudolph, G.: An evolutionary algorithm for integer programming. In: Davidor, Y., Schwefel, H.-P., M\u00e4nner, R. (eds.) PPSN III. LNCS, vol. 866, pp. 139\u2013148. Springer, Heidelberg (1994)"},{"key":"7_CR36","unstructured":"Boston Scientific: Pacemaker System Specification. Boston Scientific, Boston (2007)"},{"key":"7_CR37","doi-asserted-by":"crossref","unstructured":"Sturm, T., Tiwari, A.: Verification and synthesis using real quantifier elimination. In: Proceedings of the 36th International Symposium on Symbolic and Algebraic Computation, pp. 329\u2013336. ACM (2011)","DOI":"10.1145\/1993886.1993935"},{"key":"7_CR38","doi-asserted-by":"crossref","unstructured":"Traonouez, L.-M.: A parametric counterexample refinement approach for robust timed specifications. arXiv preprint arXiv:1207.4269 (2012)","DOI":"10.4204\/EPTCS.87.3"}],"container-title":["Lecture Notes in Computer Science","Hybrid Systems Biology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-26916-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T02:49:40Z","timestamp":1748746180000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-26916-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319269153","9783319269160"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-26916-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}