{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T05:19:51Z","timestamp":1726031991419},"publisher-location":"Cham","reference-count":96,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030172961"},{"type":"electronic","value":"9783030172978"}],"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-17297-8_1","type":"book-chapter","created":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T09:04:12Z","timestamp":1560243852000},"page":"3-35","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Model Checking Approach to the Analysis of Biological Systems"],"prefix":"10.1007","author":[{"given":"Nikola","family":"Bene\u0161","sequence":"first","affiliation":[]},{"given":"Lubo\u0161","family":"Brim","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,6,12]]},"reference":[{"issue":"2","key":"1_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2699712","volume":"25","author":"Alexander Andreychenko","year":"2015","unstructured":"Andreychenko A, Mikeev L, Wolf V (2015) Model reconstruction for moment-based stochastic chemical kinetics. ACM Trans Model Comput Simul 25(2):12:1\u201312:19","journal-title":"ACM Transactions on Modeling and Computer Simulation"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Areces C, ten Cate B (2007) Hybrid logics. In: Blackburn P, van Benthem J, Wolter F (eds) Handbook of modal logic, vol 3, 1st edn. Elsevier","DOI":"10.1016\/S1570-2464(07)80017-6"},{"issue":"1","key":"1_CR3","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1186\/1471-2105-12-490","volume":"12","author":"Gustavo Arellano","year":"2011","unstructured":"Arellano G, Argil J, Azpeitia E, Ben\u00edtez M, Carrillo M, G\u00f3ngora P, Rosenblueth D, Alvarez-Buylla E (2011) \u201cAntelope\u201d a hybrid-logic model checker for branching-time boolean grn analysis. BMC Bioinform 12(1):490","journal-title":"BMC Bioinformatics"},{"issue":"4","key":"1_CR4","doi-asserted-by":"publisher","first-page":"1180","DOI":"10.1109\/TCBB.2017.2775219","volume":"15","author":"M Backenk\u00f6hler","year":"2018","unstructured":"Backenk\u00f6hler M, Bortolussi L, Wolf V (2018) Moment-based parameter estimation for stochastic reaction networks in equilibrium. IEEE\/ACM Trans Comput Biol Bioinform 15(4):1180\u20131192","journal-title":"IEEE\/ACM Trans Comput Biol Bioinform"},{"key":"1_CR5","unstructured":"Baier C, Katoen JP (2008) Principles of model checking. The MIT Press"},{"issue":"3","key":"1_CR6","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1109\/TCBB.2011.110","volume":"9","author":"J Barnat","year":"2012","unstructured":"Barnat J, Brim L, Krej\u010d\u00ed A, \u0160treck A, \u0160afr\u00e1nek D, Vejn\u00e1r M, Vejpustek T (2012) On parameter synthesis by parallel model checking. IEEE\/ACM Trans Comput Biol Bioinform 9(3):693\u2013705","journal-title":"IEEE\/ACM Trans Comput Biol Bioinform"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Barnat J, Brim L, \u010cern\u00e1 I, Dra\u017ean S, Fabrikov\u00e1 J, L\u00e1n\u00edk J, \u0160afr\u00e1nek D, Ma H (2009) BioDiVinE: A framework for parallel analysis of biological models. In: Computational models for cell processes (COMPMOD). EPTCS, vol 6, pp 31\u201345","DOI":"10.4204\/EPTCS.6.3"},{"issue":"3","key":"1_CR8","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1093\/bib\/bbp074","volume":"11","author":"J Barnat","year":"2010","unstructured":"Barnat J, Brim L, \u0160afr\u00e1nek D (2010) High-performance analysis of biological systems dynamics with the DiVinE model checker. Brief Bioinform 11(3):301\u2013312","journal-title":"Brief Bioinform"},{"issue":"20","key":"1_CR9","doi-asserted-by":"publisher","first-page":"1999","DOI":"10.1016\/j.tcs.2009.12.019","volume":"411","author":"E Bartocci","year":"2010","unstructured":"Bartocci E, Corradini F, Merelli E, Tesei L (2010) Detecting synchronisation of biological oscillators by model checking. Theor Comput Sci 411(20):1999\u20132018","journal-title":"Theor Comput Sci"},{"issue":"1","key":"1_CR10","doi-asserted-by":"publisher","first-page":"e1004591","DOI":"10.1371\/journal.pcbi.1004591","volume":"12","author":"Ezio Bartocci","year":"2016","unstructured":"Bartocci E, Li\u00f2 P (2016) Computational modeling, formal analysis, and tools for systems biology. PLOS Comput Biol 12(1):1\u201322","journal-title":"PLOS Computational Biology"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Batt G, Belta C, Weiss R (2007) Model checking liveness properties of genetic regulatory networks. In: TACAS. LNCS, vol 4424. Springer, pp 323\u2013338","DOI":"10.1007\/978-3-540-71209-1_25"},{"issue":"18","key":"1_CR12","doi-asserted-by":"publisher","first-page":"603","DOI":"10.1093\/bioinformatics\/btq387","volume":"26","author":"G Batt","year":"2010","unstructured":"Batt G, Page M, Cantone I, G\u00f6ssler G, Monteiro P, de Jong H (2010) Efficient parameter search for qualitative models of regulatory networks using symbolic model checking. Bioinformatics 26(18):603\u2013610","journal-title":"Bioinformatics"},{"key":"1_CR13","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1093\/bioinformatics\/bti1048","volume":"21","author":"G Batt","year":"2005","unstructured":"Batt G, Ropers D, Jong HD, Geiselmann J, Mateescu R, Schneider D (2005) Validation of qualitative models of genetic regulatory networks by model checking: analysis of the nutritional stress response in escherichia coli. Bioinformatics 21:19\u201328","journal-title":"Bioinformatics"},{"key":"1_CR14","first-page":"38","volume-title":"Lecture Notes in Computer Science","author":"Gr\u00e9gory Batt","year":"2007","unstructured":"Batt G, Salah RB, Maler O (2007) On timed models of gene networks. In: Formal modeling and analysis of timed systems (FORMATS). LNCS, Springer, Berlin, pp 38\u201352"},{"issue":"18","key":"1_CR15","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 (2007) Robustness analysis and tuning of synthetic gene networks. Bioinformatics 23(18):2415\u20132422","journal-title":"Bioinformatics"},{"key":"1_CR16","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.scico.2010.07.002","volume":"76","author":"MH Beek ter","year":"2011","unstructured":"ter Beek MH, Fantechi A, Gnesi S, Mazzanti F (2011) A state\/event-based model-checking approach for the analysis of abstract system properties. Sci Comput Prog 76:119\u2013135","journal-title":"Sci Comput Prog"},{"key":"1_CR17","first-page":"200","volume-title":"Lecture Notes in Computer Science","author":"Gerd Behrmann","year":"2004","unstructured":"Behrmann G, David A, Larsen KG (2004) A tutorial on uppaal. In: 4th international school on formal methods for the design of computer, communication, and software systems in formal methods for the design of real-time systems (SFM-RT), No. 3185. LNCS, Springer, Berlin, pp 200\u2013236"},{"issue":"11","key":"1_CR18","doi-asserted-by":"publisher","first-page":"1749","DOI":"10.1109\/TAC.2006.884957","volume":"51","author":"Calin Belta","year":"2006","unstructured":"Belta C, Habets LCGJM (2006) Controlling a class of nonlinear systems on rectangles. IEEE Trans Automat Contr 51(11):1749\u20131759","journal-title":"IEEE Transactions on Automatic Control"},{"key":"1_CR19","first-page":"192","volume":"9938","author":"N Bene\u0161","year":"2016","unstructured":"Bene\u0161 N, Brim L, Demko M, Pastva S, \u0160afr\u00e1nek D (2016) Parallel SMT-based parameter synthesis with application to piecewise multi-affine systems. ATVA. LNCS 9938:192\u2013208","journal-title":"ATVA. LNCS"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Bene\u0161 N, Brim L, Demko M, Pastva S, \u0160afr\u00e1nek D (2016) A model checking approach to discrete bifurcation analysis. In: Fitzgerald J, Heitmeyer C, Gnesi S, Philippou A (eds.) FM 2016, vol 9995. LNCS, Springer, pp 85\u2013101","DOI":"10.1007\/978-3-319-48989-6_6"},{"issue":"3","key":"1_CR21","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1016\/j.jtbi.2004.04.003","volume":"229","author":"G Bernot","year":"2004","unstructured":"Bernot G, Comet JP, Richard A, Guespin J (2004) Application of formal methods to biological regulatory networks: extending thomas\u2019 asynchronous logical approach with temporal logic. J Theor Biol 229(3):339\u2013347","journal-title":"J Theor Biol"},{"key":"1_CR22","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Armin Biere","year":"1999","unstructured":"Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without BDDs. In: Cleaveland WR (ed) Tools and algorithms for the construction and analysis of systems, vol 6806. LNCS, Springer, Berlin, pp 193\u2013207"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R (2015) Abstraction-based parameter synthesis for multiaffine systems. In: Hardware and software: verification and testing, lecture notes in computer science, vol 9434, Springer International Publishing, pp 19\u201335","DOI":"10.1007\/978-3-319-26287-1_2"},{"key":"1_CR24","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-642-05089-3_2","volume-title":"FM 2009: Formal Methods","author":"Nicola Bonzanni","year":"2009","unstructured":"Bonzanni N, Feenstra KA, Fokkink W, Krepska E (2009) What can formal methods bring to systems biology? In: FM 2009: formal methods, second world congress, eindhoven, The Netherlands, November 2-6, 2009. Proceedings, Lecture notes in computer science, vol 5850, Springer, Berlin, pp 16\u201322"},{"key":"1_CR25","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-319-43425-4_5","volume-title":"Quantitative Evaluation of Systems","author":"Luca Bortolussi","year":"2016","unstructured":"Bortolussi L, Cardelli L, Kwiatkowska M, Laurenti L (2016) Approximation of probabilistic reachability for chemical reaction networks using the linear noise approximation. In: Quantitative evaluation of system (QEST 2016), vol 9826, Springer, Berlin, pp 72\u201388"},{"key":"1_CR26","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-319-22264-6_6","volume-title":"Quantitative evaluation of systems","author":"L Bortolussi","year":"2015","unstructured":"Bortolussi L, Milios D, Sanguinetti G (2015) U-check: model checking and parameter synthesis under uncertainty. In: Campos J, Haverkort BR (eds) Quantitative evaluation of systems. Springer International Publishing, Cham, pp 89\u2013104"},{"key":"1_CR27","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/j.ic.2016.01.004","volume":"247","author":"L Bortolussi","year":"2016","unstructured":"Bortolussi L, Milios D, Sanguinetti G (2016) Smoothed model checking for uncertain continuous-time markov chains. Inf Comput 247:235\u2013253","journal-title":"Inf Comput"},{"key":"1_CR28","first-page":"63","volume-title":"Lecture Notes in Computer Science","author":"Lubo\u0161 Brim","year":"2013","unstructured":"Brim L, \u010ce\u0161ka M, \u0160afr\u00e1nek D (2013) Model checking of biological system. In: 13th International school on formal methods for the design of computer, communication and software systems: dynamical systems"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Brim L, Barnat J (2007) Tutorial: Parallel model checking. In: Bosnacki D, Edelkamp S (eds) Model checking software, 14th International SPIN workshop, Berlin, Germany, July 1-3, 2007, Proceedings, Lecture notes in computer science, vol 4595, Springer, Berlin, pp 187\u2013203","DOI":"10.1007\/978-3-540-73370-6_2"},{"key":"1_CR30","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-319-26916-0_4","volume-title":"Hybrid Systems Biology","author":"Lubo\u0161 Brim","year":"2015","unstructured":"Brim L, Demko M, Pastva S, \u0160afr\u00e1nek D (2015) High-performance discrete bifurcation analysis for piecewise-affine dynamical systems. In: Hybrid systems biology, Springer, Berlin, pp 58\u201374"},{"key":"1_CR31","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, Vejpu\u00a0stek T (2014) STL*: extending signal temporal logic with signal-value freezing operator. Information and computation 236, 52\u201367, special Issue on Hybrid Systems and Biology","journal-title":"Information and Computation"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Brim L, \u010ce\u0161ka M, Demko M, Pastva S, \u0160afr\u00e1nek D (2015) Parameter synthesis by parallel coloured CTL model checking. In: Roux O, Bourdon J (eds) Computational methods in systems biology, Lecture notes in computer science, vol 9308, pp 251\u2013263. Springer International Publishing (2015)","DOI":"10.1007\/978-3-319-23401-4_21"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: \n                    \n                      \n                    \n                    $$10^{20}$$\n                   states and beyond. Inf Comput 98(2):142\u2013170","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"1_CR34","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/11880646_4","volume-title":"Transactions on Computational Systems Biology VI","author":"Laurence Calzone","year":"2006","unstructured":"Calzone L, Chabrier-Rivier N, Fages F, Soliman S (2006) Machine learning biochemical networks from temporal logic properties. In: Transactions on computational systems biology VI, LNCS, Springer, Berlin, Heidelberg, pp 68\u201394"},{"key":"1_CR35","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-1-4419-9863-7_270","volume-title":"Encyclopedia of Systems Biology","author":"Alan Champneys","year":"2013","unstructured":"Champneys A, Tsaneva-Atanasova K (2013) Dynamical systems theory, bifurcation analysis. In: Encyclopedia of systems biology, Springer, Berlin, pp 632\u2013637"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Chaouiya C, Remy E, Moss\u00e9 B, Thieffry D (2003) Qualitative analysis of regulatory graphs: a computational tool based on a discrete formal framework. In: Positive systems, vol 294, LNCIS, Springer, pp 830\u2013832","DOI":"10.1007\/978-3-540-44928-7_17"},{"key":"1_CR37","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"Alessandro Cimatti","year":"2002","unstructured":"Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV 2: an OpenSource tool for symbolic model checking. Computer aided verification (CAV), vol 2404, LNCS, Springer, Berlin, Heidelberg, pp 359\u2013364"},{"issue":"1\u20132","key":"1_CR38","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"EM Clarke","year":"1996","unstructured":"Clarke EM, Enders R, Filkorn T, Jha S (1996) Exploiting symmetry in temporal logic model checking. Form Methods Syst Des 9(1\u20132):77\u2013104","journal-title":"Form Methods Syst Des"},{"key":"1_CR39","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge"},{"key":"1_CR40","first-page":"1","volume-title":"Automated Technology for Verification and Analysis","author":"Edmund M. Clarke","year":"2011","unstructured":"Clarke E, Zuliani P (2011) Statistical model checking for cyber-physical systems. Automated technology for verification and analysis (ATVA), vol 6996. LNCS, Springer, Berlin Heidelberg, pp 1\u201312"},{"key":"1_CR41","first-page":"176","volume-title":"Lecture Notes in Computer Science","author":"Edmund Clarke","year":"2001","unstructured":"Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2001) Progress on the state explosion problem in model checking. In: Informatics - 10 Years back. 10 Years ahead, vol 2000, LNCS, Springer, Berlin, pp 176\u2013194"},{"issue":"1","key":"1_CR42","doi-asserted-by":"publisher","first-page":"14869","DOI":"10.3182\/20110828-6-IT-1002.03317","volume":"44","author":"Pieter J. Collins","year":"2011","unstructured":"Collins P, Habets LC, van Schuppen JH, \u010cern\u00e1 I, Fabrikov\u00e1 J, \u0160afr\u00e1nek D (2011) Abstraction of biochemical reaction systems on polytopes. In: Proceedings of the 18th IFAC world congress, vol 18, pp 14869\u201314875","journal-title":"IFAC Proceedings Volumes"},{"key":"1_CR43","doi-asserted-by":"crossref","unstructured":"Dang T, Donze A, Maler O, Shalev N (2008) Sensitive state-space exploration. In: IEEE conference on decision and control, pp 4049\u20134054","DOI":"10.1109\/CDC.2008.4739371"},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"Didier F, Henzinger TA, Mateescu M, Wolf V (2010) Sabre: a tool for stochastic analysis of biochemical reaction networks. CoRR \n                    arXiv:abs\/1005.2819","DOI":"10.1109\/QEST.2010.33"},{"key":"1_CR45","doi-asserted-by":"crossref","unstructured":"Dluho\u0161 P, Brim L, \u0160afr\u00e1nek D (2012) On expressing and monitoring oscillatory dynamics. In: Hybrid systems and biology (HSB), vol 92, EPTCS, pp 73\u201387","DOI":"10.4204\/EPTCS.92.6"},{"key":"1_CR46","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-540-88562-7_20","volume-title":"Computational Methods in Systems Biology","author":"Robin Donaldson","year":"2008","unstructured":"Donaldson R, Gilbert D (2008) A model checking approach to the parameter estimation of biochemical pathways. In: CMSB, vol 5307, LNCS, Springer, Berlin, pp 269\u2013287"},{"key":"1_CR47","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-14295-6_17","volume-title":"Computer Aided Verification","author":"Alexandre Donz\u00e9","year":"2010","unstructured":"Donz\u00e9 A (2010) Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Computer aided verification (CAV). LNCS, Springer, Berlin, Heidelberg, pp 167\u2013170"},{"key":"1_CR48","doi-asserted-by":"crossref","unstructured":"Donz\u00e9 A (2010) Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: CAV. vol 10, Springer, pp 167\u2013170","DOI":"10.1007\/978-3-642-14295-6_17"},{"issue":"3","key":"1_CR49","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1089\/cmb.2009.0172","volume":"17","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9 A, Clermont G, Langmead CJ (2010) Parameter synthesis in nonlinear dynamical systems: application to systems biology. J Comput Biol 17(3):325\u2013336","journal-title":"J Comput Biol"},{"key":"1_CR50","unstructured":"Eker S, Knapp M, Laderoute K, Lincoln P, Meseguer J, Sonmez K (2002) Pathway logic: symbolic analysis of biological signaling. In: Pacific symposium on biocomputing, pp 400\u2013412"},{"issue":"1\u20132","key":"1_CR51","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"EA Emerson","year":"1996","unstructured":"Emerson EA, Sistla AP (1996) Symmetry and model checking. Form Methods Syst Des 9(1\u20132):105\u2013131","journal-title":"Form Methods Syst Des"},{"key":"1_CR52","doi-asserted-by":"crossref","unstructured":"Fages F, Soliman S (2008) Formal cell biology in Biocham. In: 8th International school on formal methods for the design of computer, communication and software systems: computational systems biology SFM08, vol 5016, pp 54\u201380","DOI":"10.1007\/978-3-540-68894-5_3"},{"issue":"1","key":"1_CR53","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.tcs.2008.07.004","volume":"408","author":"F Fages","year":"2008","unstructured":"Fages F, Rizk A (2008) On temporal logic constraint solving for analyzing numerical data time series. Theor Comput Sci 408(1):55\u201365","journal-title":"Theor Comput Sci"},{"issue":"11","key":"1_CR54","doi-asserted-by":"publisher","first-page":"1239","DOI":"10.1038\/nbt1356","volume":"25","author":"J Fisher","year":"2007","unstructured":"Fisher J, Henzinger TA (2007) Executable cell biology. Nat Biotechnol 25(11):1239\u20131249","journal-title":"Nat Biotechnol"},{"key":"1_CR55","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-319-12982-2_5","volume-title":"Computational Methods in Systems Biology","author":"Fabian Fr\u00f6hlich","year":"2014","unstructured":"Fr\u00f6hlich F, Theis F, Hasenauer J (2014) Uncertainty analysis for non-identifiable dynamical systems: profile likelihoods, bootstrapping and more. In: CMBS, vol 8859, LNCS, Springer, Berlin, pp 61\u201372"},{"key":"1_CR56","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-319-12982-2_4","volume-title":"Computational Methods in Systems Biology","author":"Attila G\u00e1bor","year":"2014","unstructured":"G\u00e1bor, A., Banga, J.R.: Improved parameter estimation in kinetic models: selection and tuning of regularization methods. In: CMSB, vol 8859, LNCS, Springer, Berlin, pp 45\u201360"},{"key":"1_CR57","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-38574-2_14","volume-title":"Automated Deduction \u2013 CADE-24","author":"Sicun Gao","year":"2013","unstructured":"Gao S, Kong S, Clarke EM (2013) dReal: An SMT solver for nonlinear theories over the reals. In: CADE-24. , vol. 7898, LNCS, Springer, Berlin, pp 208\u2013214"},{"key":"1_CR58","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/3-540-48234-2_2","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"J Geldenhuys","year":"1999","unstructured":"Geldenhuys J, de Villiers PJA (1999) Runtime efficient state compaction in SPIN. In: Model checking software (SPIN), vol 1680. LNCS, Springer, Berlin, pp 12\u201321"},{"key":"1_CR59","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-3-540-95885-7_2","volume-title":"Membrane Computing","author":"David Gilbert","year":"2009","unstructured":"Gilbert D, Breitling R, Heiner M, Donaldson R (2009) An introduction to biomodel engineering, illustrated for signal transduction pathways. Membrane computing, vol 5391, LNCS, Springer, Berlin, pp 13\u201328"},{"key":"1_CR60","unstructured":"Goethem SV, Jacquet JM, Brim L, \u0160afr\u00e1nek D (2013) Timed modelling of gene networks with arbitrary expression level discretization. In: Interactions between computer science and biology. ENTCS, Elsevier"},{"key":"1_CR61","first-page":"396","volume":"6806","author":"R Grosu","year":"2011","unstructured":"Grosu R, Batt G, Fenton FH, Glimm J, Guernic CL, Smolka SA, Bartocci E (2011) From cardiac cells to genetic regulatory networks. CAV LNCS 6806:396\u2013411","journal-title":"CAV LNCS"},{"key":"1_CR62","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-319-47151-8_4","volume-title":"Hybrid Systems Biology","author":"Matej Hajnal","year":"2016","unstructured":"Hajnal M, \u0160afr\u00e1nek D, Demko M, Pastva S, Krej\u010d\u00ed P, Brim L (2016) Toward modelling and analysis of transient and sustained behaviour of signalling pathways. In: Hybrid systems biology - 5th international workshop, HSB 2016, Grenoble, France, October 20-21, 2016, Proceedings. Springer, Berlin, pp 57\u201366"},{"issue":"3","key":"1_CR63","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/j.tcs.2007.11.013","volume":"319","author":"J Heath","year":"2008","unstructured":"Heath J, Kwiatkowska M, Norman G, Parker D, Tymchyshyn O (2008) Probabilistic model checking of complex biological pathways. Theor Comput Sci 319(3):239\u2013257","journal-title":"Theor Comput Sci"},{"key":"1_CR64","doi-asserted-by":"crossref","unstructured":"Heiner M, Gilbert D, Donaldson R (2008) Petri nets for systems and synthetic biology. In: Formal methods for the design of computer, communication, and software systems 8th international conference on formal methods for computational systems biology (SFM), vol 5016, LNCS, Springer, Berlin, pp 215\u2013264","DOI":"10.1007\/978-3-540-68894-5_7"},{"key":"1_CR65","unstructured":"Holzmann GJ (2003) The Spin model checker: primer and reference manual. Addison-Wesley"},{"key":"1_CR66","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-642-03845-7_15","volume-title":"Computational Methods in Systems Biology","author":"Sumit K. Jha","year":"2009","unstructured":"Jha SK, Clarke EM, Langmead CJ, Legay A, Platzer A, Zuliani P (2009) A bayesian approach to model checking biological systems. In: Computational methods in systems biology. Springer, Berlin, pp 218\u2013234"},{"key":"1_CR67","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-642-33636-2_13","volume-title":"Computational Methods in Systems Biology","author":"Hannes Klarner","year":"2012","unstructured":"Klarner H, Streck A, \u0160afr\u00e1nek D, Kol\u010d\u00e1k J, Siebert H (2012) Parameter identification and model ranking of thomas networks. In: Computational methods in systems biology (CMSB), LNCS, Springer, Berlin, pp 207\u2013226"},{"key":"1_CR68","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"Marta Kwiatkowska","year":"2011","unstructured":"Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Computer aided verification (CAV), vol 6806, LNCS, Springer, Berlin, pp 585\u2013591"},{"key":"1_CR69","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime Verification","author":"Axel Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S (2010) Statistical model checking: an overview. In: Runtime verification, Springer, Berlin, Heidelberg, pp 122\u2013135"},{"key":"1_CR70","doi-asserted-by":"crossref","unstructured":"Li Y, Albarghouthi A, Kincaid Z, Gurfinkel A, Chechik M (2014) Symbolic optimization with SMT solvers. In: POPL \u201914. ACM, pp 607\u2013618","DOI":"10.1145\/2535838.2535857"},{"key":"1_CR71","unstructured":"Liu B, Kong S, Gao S, Zuliani P, Clarke EM (2014) Parameter synthesis for cardiac cell hybrid models using \n                    \n                      \n                    \n                    $$\\delta $$\n                  -decisions. In: CMSB, vol 8859, LNCS, Springer, Berlin, pp 99\u2013113"},{"key":"1_CR72","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-319-23401-4_16","volume-title":"Computational Methods in Systems Biology","author":"Curtis Madsen","year":"2015","unstructured":"Madsen C, Shmarov F, Zuliani P (2015) BioPSy: An SMT-based tool for guaranteed parameter set synthesis of biological models. In: CMSB\u201915, vol 9308, LNCS, Springer, Berlin, pp 182\u2013194"},{"key":"1_CR73","doi-asserted-by":"crossref","unstructured":"Maler O, Batt G (2008) Approximating continuous systems by timed automata. In: Formal methods in systems biology (FMSB), LNCS, Springer, Berlin, pp 77\u201389","DOI":"10.1007\/978-3-540-68413-8_6"},{"key":"1_CR74","doi-asserted-by":"crossref","unstructured":"Maler O, Nickovic D, Pnueli A (2008) Checking temporal properties of discrete, timed and continuous behaviors. In: Pillars of computer science, Springer, Berlin, Heidelberg, pp 475\u2013505","DOI":"10.1007\/978-3-540-78127-1_26"},{"issue":"26","key":"1_CR75","doi-asserted-by":"publisher","first-page":"2854","DOI":"10.1016\/j.tcs.2010.05.009","volume":"412","author":"R Mateescu","year":"2011","unstructured":"Mateescu R, Monteiro PT, Dumas E, de Jong H (2011) CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks. Theor Comput Sci 412(26):2854\u20132883","journal-title":"Theor Comput Sci"},{"key":"1_CR76","doi-asserted-by":"publisher","first-page":"1172","DOI":"10.1007\/978-1-4614-1806-1_71","volume-title":"Mathematics of Complexity and\u00a0Dynamical Systems","author":"Hil Meijer","year":"2012","unstructured":"Meijer H, Dercole F, Oldeman B (2011) Numerical bifurcation analysis. In: Mathematics of complexity and dynamical systems, Springer, Berlin, pp 1172\u20131194"},{"issue":"1","key":"1_CR77","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S0959-437X(98)80057-9","volume":"8","author":"S Mittnacht","year":"1998","unstructured":"Mittnacht S (1998) Control of pRB phosphorylation. Curr Opin Genet Dev 8(1):21\u201327","journal-title":"Curr Opin Genet Dev"},{"key":"1_CR78","unstructured":"Monteiro PT, Ropers D, Mateescu R, Freitas AT, de\u00a0Jong H (2008) Temporal logic patterns for querying qualitative models of genetic regulatory networks. In: ECAI, vol 178, FAIA, IOS Press, pp 229\u2013233"},{"key":"1_CR79","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-319-99154-2_20","volume-title":"Quantitative Evaluation of Systems","author":"Laura Nenzi","year":"2018","unstructured":"Nenzi L, Silvetti S, Bartocci E, Bortolussi L (2018) A robust genetic algorithm for learning temporal specifications from data. In: Quantitative evaluation of systems, Springer International Publishing, Cham, pp. 323\u2013338"},{"key":"1_CR80","doi-asserted-by":"crossref","unstructured":"Niu W, Wang D (2008) Algebraic analysis of bifurcation and limit cycles for biological systems. In: Algebraic biology, AB \u201908, Springer, Berlin, pp 156\u2013171","DOI":"10.1007\/978-3-540-85101-1_12"},{"key":"1_CR81","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-642-03240-0_7","volume-title":"Formal Methods for Industrial Critical Systems","author":"Radek Pel\u00e1nek","year":"2009","unstructured":"Pel\u00e1nek R (2009) Fighting state space explosion: review and evaluation. In: Formal methods for industrial critical systems (FMICS), vol 5596, LNCS, Springer, Berlin, pp 37\u201352"},{"key":"1_CR82","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/BFb0028727","volume-title":"Computer Aided Verification","author":"Doron Peled","year":"1998","unstructured":"Peled D (1988) Ten years of partial order reduction. In: Computer aided verification (CAV), LNCS, Springer, Berlin, pp 17\u201328"},{"issue":"5","key":"1_CR83","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1145\/1506409.1506427","volume":"52","author":"C Priami","year":"2009","unstructured":"Priami C (2009) Algorithmic systems biology. Commun ACM 52(5):80\u201388","journal-title":"Commun ACM"},{"key":"1_CR84","doi-asserted-by":"crossref","unstructured":"Raman V, Donz\u00e9 A, Sadigh D, Murray RM, Seshia SA (2015) Reactive synthesis from signal temporal logic specifications. In: HSCC\u201915, ACM, New York, NY, USA, pp 239\u2013248","DOI":"10.1145\/2728606.2728628"},{"key":"1_CR85","doi-asserted-by":"crossref","unstructured":"Raue A, Karlsson J, Saccomani MP, Jirstrand M, Timmer J (2014) Comparison of approaches for parameter identifiability analysis of biological systems. Bioinformatics","DOI":"10.1093\/bioinformatics\/btu006"},{"issue":"12","key":"1_CR86","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 (2009) A general computational method for robustness analysis with applications to synthetic gene networks. Bioinformatics 25(12)","journal-title":"Bioinformatics"},{"issue":"4","key":"1_CR87","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1038\/ncb1233","volume":"7","author":"Satoru Sasagawa","year":"2005","unstructured":"Sasagawa S, Ozaki Yi, Fujita K, Kuroda S (2005) Prediction and validation of the distinct dynamics of transient and sustained ERK activation. Nat Cell Biol 7(4):365\u2013373","journal-title":"Nature Cell Biology"},{"issue":"1","key":"1_CR88","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1186\/1752-0509-1-4","volume":"1","author":"M Schaub","year":"2007","unstructured":"Schaub M, Henzinger T, Fisher J (2007) Qualitative networks: a symbolic approach to analyze biological signaling networks. BMC Syst Biol 1(1):4","journal-title":"BMC Syst Biol"},{"key":"1_CR89","doi-asserted-by":"crossref","unstructured":"Schivo DS, Scholma J, Wanders, B, Urquidi Camacho R, van der PV, Karperien H, Langerak R, van de JP, Post J (2012) Modelling biological pathway dynamics with timed automata. In: IEEE international conference on bioinformatics and bioengineering (ICBB), IEEE Computer Society, pp 447\u2013453","DOI":"10.1109\/BIBE.2012.6399719"},{"issue":"1","key":"1_CR90","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1186\/s12918-016-0286-z","volume":"10","author":"S Schivo","year":"2016","unstructured":"Schivo S, Scholma J, van der Vet PE, Karperien M, Post JN, van de Pol J, Langerak R (2016) Modelling with animo: between fuzzy logic and differential equations. BMC Syst Biol 10(1):56","journal-title":"BMC Syst Biol"},{"key":"1_CR91","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-642-03845-7_20","volume-title":"Computational Methods in Systems Biology","author":"Martin Schwarick","year":"2009","unstructured":"Schwarick M, Heiner M (2009) CSL model checking of biochemical networks with interval decision diagrams. In: Computational methods in systems biology (CMSB), vol 5688, LNCS\/LNBI, Springer, Berlin, pp 296\u2013312"},{"key":"1_CR92","doi-asserted-by":"crossref","unstructured":"Schwarick M, Rohr C, Heiner M (2011) MARCIE - Model checking And Reachability analysis done effiCIEntly . In: Quantitative evaluation of systems (QEST 2011). IEEE Computer Society, pp 91\u2013100","DOI":"10.1109\/QEST.2011.19"},{"key":"1_CR93","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/11885191_12","volume-title":"Computational Methods in Systems Biology","author":"Heike Siebert","year":"2006","unstructured":"Siebert H, Bockmayr A (2006) Incorporating time delays into the logical analysis of gene regulatory networks. Computational Methods in Systems Biology (CMSB), vol 4210. LNCS, Springer, Berlin Heidelberg, pp 169\u2013183"},{"issue":"10","key":"1_CR94","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 (2004) Bifurcation analysis of the regulatory modules of the mammalian G1\/S transition. Bioinformatics 20(10):1506\u20131511","journal-title":"Bioinformatics"},{"issue":"4","key":"1_CR95","doi-asserted-by":"publisher","first-page":"1113","DOI":"10.1016\/j.bbrc.2004.01.009","volume":"314","author":"S Yamada","year":"2004","unstructured":"Yamada S, Taketomi T, Yoshimura A (2004) Model analysis of difference between EGF pathway and FGF pathway. Biochem Biophys Res Commun 314(4):1113\u20131120","journal-title":"Biochem Biophys Res Commun"},{"key":"1_CR96","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S Yovine","year":"1997","unstructured":"Yovine S (1997) Kronos: a verification tool for real-time systems. Int J Softw Tools Technol Transf 1:123\u2013133","journal-title":"Int J Softw Tools Technol Transf"}],"container-title":["Computational Biology","Automated Reasoning for Systems Biology and Medicine"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17297-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T09:11:59Z","timestamp":1560244319000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17297-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030172961","9783030172978"],"references-count":96,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17297-8_1","relation":{},"ISSN":["1568-2684","2662-2432"],"issn-type":[{"type":"print","value":"1568-2684"},{"type":"electronic","value":"2662-2432"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"12 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}