{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T13:01:48Z","timestamp":1726059708347},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030349677"},{"type":"electronic","value":"9783030349684"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-34968-4_2","type":"book-chapter","created":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T19:14:54Z","timestamp":1574363694000},"page":"27-45","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Accelerating Parameter Synthesis Using Semi-algebraic Constraints"],"prefix":"10.1007","author":[{"given":"Nikola","family":"Bene\u0161","sequence":"first","affiliation":[]},{"given":"Lubo\u0161","family":"Brim","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Geletka","sequence":"additional","affiliation":[]},{"given":"Samuel","family":"Pastva","sequence":"additional","affiliation":[]},{"given":"David","family":"\u0160afr\u00e1nek","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,11,22]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","unstructured":"Arney, D., Pajic, M., Goldman, J.M., Lee, I., Mangharam, R., Sokolsky, O.: Toward patient safety in closed-loop medical device systems. In: ICCPS 10, pp. 139\u2013148. ACM (2010). \nhttps:\/\/doi.org\/10.1145\/1795194.1795214","DOI":"10.1145\/1795194.1795214"},{"issue":"4","key":"2_CR2","doi-asserted-by":"publisher","first-page":"865","DOI":"10.1137\/0213054","volume":"13","author":"DS Arnon","year":"1984","unstructured":"Arnon, D.S., Collins, G.E., McCallum, S.: Cylindrical algebraic decomposition I: the basic algorithm. SIAM J. Comput. 13(4), 865\u2013877 (1984)","journal-title":"SIAM J. Comput."},{"key":"2_CR3","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/s00236-006-0035-7","volume":"43","author":"E Asarin","year":"2007","unstructured":"Asarin, E., Dang, T., Girard, A.: Hybridization methods for the analysis of nonlinear systems. Acta Informatica 43, 451\u2013476 (2007)","journal-title":"Acta Informatica"},{"issue":"3","key":"2_CR4","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1109\/TCBB.2011.110","volume":"9","author":"J Barnat","year":"2012","unstructured":"Barnat, J., et al.: On parameter synthesis by parallel model checking. IEEE\/ACM Trans. Comput. Biol. Bioinf. 9(3), 693\u2013705 (2012)","journal-title":"IEEE\/ACM Trans. Comput. Biol. Bioinf."},{"key":"2_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.tcs.2015.02.046","volume":"587","author":"E Bartocci","year":"2015","unstructured":"Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: System design of stochastic models using robustness of temporal properties. TCS 587, 3\u201325 (2015)","journal-title":"TCS"},{"issue":"18","key":"2_CR6","doi-asserted-by":"publisher","first-page":"i603","DOI":"10.1093\/bioinformatics\/btq387","volume":"26","author":"G Batt","year":"2010","unstructured":"Batt, G., Page, M., Cantone, I., Goessler, G., Monteiro, P., de Jong, H.: Efficient parameter search for qualitative models of regulatory networks using symbolic model checking. Bioinformatics 26(18), i603\u2013i610 (2010)","journal-title":"Bioinformatics"},{"issue":"18","key":"2_CR7","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 23(18), 2415\u20132422 (2007)","journal-title":"Bioinformatics"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-319-46520-3_13","volume-title":"Automated Technology for Verification and Analysis","author":"N Bene\u0161","year":"2016","unstructured":"Bene\u0161, N., Brim, L., Demko, M., Pastva, S., \u0160afr\u00e1nek, D.: Parallel SMT-based parameter synthesis with application to piecewise multi-affine systems. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 192\u2013208. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-46520-3_13"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1007\/978-3-319-63387-9_29","volume-title":"Computer Aided Verification","author":"N Bene\u0161","year":"2017","unstructured":"Bene\u0161, N., Brim, L., Demko, M., Pastva, S., \u0160afr\u00e1nek, D.: Pithya: a parallel tool for parameter synthesis of piecewise multi-affine dynamical systems. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 591\u2013598. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-63387-9_29"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-24537-9_3","volume-title":"Reachability Problems","author":"B B\u00e9rard","year":"2015","unstructured":"B\u00e9rard, B., Haddad, S., Picaronny, C., El Din, M.S., Sassolas, M.: Polynomial interrupt timed automata. In: Boja\u0144czyk, M., Lasota, S., Potapov, I. (eds.) RP 2015. LNCS, vol. 9328, pp. 20\u201332. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-24537-9_3"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-319-26287-1_2","volume-title":"Hardware and Software: Verification and Testing","author":"S Bogomolov","year":"2015","unstructured":"Bogomolov, S., Schilling, C., Bartocci, E., Batt, G., Kong, H., Grosu, R.: Abstraction-based parameter synthesis for multiaffine systems. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 19\u201335. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-26287-1_2"},{"key":"2_CR12","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/j.ic.2014.01.012","volume":"236","author":"L Brim","year":"2014","unstructured":"Brim, L., Dluho\u0161, P., \u0160afr\u00e1nek, D., Vejpustek, T.: STL*: extending signal temporal logic with signal-value freezing operator. Inf. Comput. 236, 52\u201367 (2014). Special Issue on Hybrid Systems and Biology","journal-title":"Inf. Comput."},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-319-26916-0_4","volume-title":"Hybrid Systems Biology","author":"L Brim","year":"2015","unstructured":"Brim, L., Demko, M., Pastva, S., \u0160afr\u00e1nek, D.: High-performance discrete bifurcation analysis for piecewise-affine dynamical systems. In: Abate, A., \u0160afr\u00e1nek, D. (eds.) HSB 2015. LNCS, vol. 9271, pp. 58\u201374. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-26916-0_4"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-39799-8_7","volume-title":"Computer Aided Verification","author":"L Brim","year":"2013","unstructured":"Brim, L., \u010ce\u0161ka, M., Dra\u017ean, S., \u0160afr\u00e1nek, D.: Exploring parameter space of stochastic biochemical systems using quantitative model checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 107\u2013123. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39799-8_7"},{"issue":"4","key":"2_CR15","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/968708.968710","volume":"37","author":"CW Brown","year":"2003","unstructured":"Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bull. 37(4), 97\u2013108 (2003)","journal-title":"ACM SIGSAM Bull."},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Chen, C., Davenport, J.H., Moreno Maza, M., Xia, B., Xiao, R.: Computing with semi-algebraic sets represented by triangular decomposition. In: ISSAC 2011, pp. 75\u201382. ACM (2011)","DOI":"10.1145\/1993886.1993903"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-540-72788-0_32","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"A Cimatti","year":"2007","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: A simple and flexible way of computing small unsatisfiable cores in SAT modulo theories. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 334\u2013339. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-72788-0_32"},{"issue":"4","key":"2_CR18","doi-asserted-by":"publisher","first-page":"1269","DOI":"10.1002\/aic.14310","volume":"60","author":"RL Clark","year":"2014","unstructured":"Clark, R.L., Cameron, J.C., Root, T.W., Pfleger, B.F.: Insights into the industrial growth of cyanobacteria from a model of the carbon? Concentrating mechanism. AIChE J. 60(4), 1269\u20131277 (2014)","journal-title":"AIChE J."},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Collins, G.E., Akritas, A.G.: Polynomial real root isolation using Descarte\u2019s rule of signs. In: SYMSAC 1976, pp. 272\u2013275. ACM (1976)","DOI":"10.1145\/800205.806346"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-319-19249-9_14","volume-title":"FM 2015: Formal Methods","author":"T Dang","year":"2015","unstructured":"Dang, T., Dreossi, T., Piazza, C.: Parameter synthesis through temporal logic specifications. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 213\u2013230. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-19249-9_14"},{"issue":"21","key":"2_CR21","doi-asserted-by":"publisher","first-page":"2095","DOI":"10.1016\/j.tcs.2011.01.014","volume":"412","author":"T Dang","year":"2011","unstructured":"Dang, T., Guernic, C.L., Maler, O.: Computing reachable states for nonlinear biological models. Theor. Comput. Sci. 412(21), 2095\u20132107 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR22","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.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-642-00602-9_12","volume-title":"Hybrid Systems: Computation and Control","author":"A Donz\u00e9","year":"2009","unstructured":"Donz\u00e9, A., Krogh, B., Rajhans, A.: Parameter synthesis for hybrid systems with an application to simulink models. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol. 5469, pp. 165\u2013179. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-00602-9_12"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-33386-6_9","volume-title":"Automated Technology for Verification and Analysis","author":"A Donz\u00e9","year":"2012","unstructured":"Donz\u00e9, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., Smolka, S.: On temporal logic and signal processing. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 92\u2013106. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-33386-6_9"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-38574-2_14","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Gao","year":"2013","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208\u2013214. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-38574-2_14"},{"key":"2_CR26","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., et al.: From cardiac cells to genetic regulatory networks. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 396\u2013411. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_31"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Guthmann, O., Strichman, O., Trostanetski, A.: Minimal unsatisfiable core extraction for SMT. In: FMCAD 2016, pp. 57\u201364. IEEE (2016)","DOI":"10.1109\/FMCAD.2016.7886661"},{"key":"2_CR28","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1016\/j.bulm.2003.08.010","volume":"66","author":"H Jong de","year":"2004","unstructured":"de Jong, H., Gouz\u00e9, J., Hernandez, C., Page, M., Sari, T., Geiselmann, J.: Qualitative simulations of genetic regulatory networks using piecewise linear models. Bull. Math. Biol. 66, 301\u2013340 (2004)","journal-title":"Bull. Math. Biol."},{"issue":"1","key":"2_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"MH Liffiton","year":"2008","unstructured":"Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning 40(1), 1\u201333 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"2_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-319-23401-4_16","volume-title":"Computational Methods in Systems Biology","author":"C Madsen","year":"2015","unstructured":"Madsen, C., Shmarov, F., Zuliani, P.: BioPSy: an SMT-based tool for guaranteed parameter set synthesis of biological models. In: Roux, O., Bourdon, J. (eds.) CMSB 2015. LNCS, vol. 9308, pp. 182\u2013194. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-23401-4_16"},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT -2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-30206-3_12"},{"issue":"5","key":"2_CR32","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1093\/comjnl\/36.5.432","volume":"36","author":"S McCallum","year":"1993","unstructured":"McCallum, S.: Solving polynomial strict inequalities using cylindrical algebraic decomposition. Comput. J. 36(5), 432\u2013438 (1993). \nhttps:\/\/doi.org\/10.1093\/comjnl\/36.5.432","journal-title":"Comput. J."},{"issue":"113","key":"2_CR33","doi-asserted-by":"publisher","first-page":"20150831","DOI":"10.1098\/rsif.2015.0831","volume":"12","author":"Andreas Milias-Argeitis","year":"2015","unstructured":"Milias-Argeitis, A., Engblom, S., Bauer, P., Khammash, M.: Stochastic focusing coupled with negative feedback enables robust regulation in biochemical reaction networks. J. Roy. Soc. Interface 12(113) (2015)","journal-title":"Journal of The Royal Society Interface"},{"key":"2_CR34","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1016\/j.cpc.2018.09.005","volume":"235","author":"S Poslavsky","year":"2019","unstructured":"Poslavsky, S.: Rings: an efficient Java\/Scala library for polynomial rings. Comput. Phys. Commun. 235, 400\u2013413 (2019)","journal-title":"Comput. Phys. Commun."},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"Raman, V., Donz\u00e9, A., Sadigh, D., Murray, R.M., Seshia, S.A.: Reactive synthesis from signal temporal logic specifications. In: HSCC 2015, pp. 239\u2013248. ACM (2015)","DOI":"10.1145\/2728606.2728628"},{"issue":"12","key":"2_CR36","doi-asserted-by":"publisher","first-page":"i169","DOI":"10.1093\/bioinformatics\/btp200","volume":"25","author":"A. Rizk","year":"2009","unstructured":"Rizk, A., Batt, G., Fages, F., Soliman, S.: A general computational method for robustness analysis with applications to synthetic gene networks. Bioinformatics 25(12) (2009)","journal-title":"Bioinformatics"},{"issue":"3","key":"2_CR37","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1006\/jsco.1999.0327","volume":"29","author":"A Strzebo\u0144ski","year":"2000","unstructured":"Strzebo\u0144ski, A.: Solving systems of strict polynomial inequalities. J. Symbolic Comput. 29(3), 471\u2013480 (2000)","journal-title":"J. Symbolic Comput."},{"issue":"4","key":"2_CR38","first-page":"74","volume":"4","author":"AW Strzebonski","year":"1994","unstructured":"Strzebonski, A.W.: An algorithm for systems of strong polynomial inequalities. Mathe. J. 4(4), 74\u201377 (1994)","journal-title":"Mathe. J."},{"issue":"10","key":"2_CR39","doi-asserted-by":"publisher","first-page":"1506","DOI":"10.1093\/bioinformatics\/bth110","volume":"20","author":"M Swat","year":"2004","unstructured":"Swat, M., Kel, A., Herzel, H.: Bifurcation analysis of the regulatory modules of the mammalian G1\/S transition. Bioinformatics 20(10), 1506\u20131511 (2004)","journal-title":"Bioinformatics"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-34968-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T19:17:05Z","timestamp":1574363825000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-34968-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030349677","9783030349684"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-34968-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"22 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bergen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Norway","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/ifm2019.hvl.no\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}