{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T19:46:04Z","timestamp":1742931964291,"version":"3.40.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319682693"},{"type":"electronic","value":"9783319682709"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-68270-9_15","type":"book-chapter","created":{"date-parts":[[2017,9,26]],"date-time":"2017-09-26T07:17:19Z","timestamp":1506410239000},"page":"297-315","source":"Crossref","is-referenced-by-count":2,"title":["Discretization of Continuous Dynamical Systems Using UPPAAL"],"prefix":"10.1007","author":[{"given":"Stefano","family":"Schivo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rom","family":"Langerak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. In: Proceedings of the IEEE, pp. 971\u2013984 (2000)","DOI":"10.1109\/5.871304"},{"key":"15_CR3","unstructured":"Bos, W.: Interactive signaling network analysis tool. Master\u2019s thesis, University of Twente (2009)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-319-22975-1_5","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"P Bouyer","year":"2015","unstructured":"Bouyer, P., Markey, N., Perrin, N., Schlehuber-Caissier, P.: Timed-automata abstraction of switched dynamical systems using control funnels. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 60\u201375. Springer, Cham (2015). doi: 10.1007\/978-3-319-22975-1_5"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-642-38874-3_3","volume-title":"Formal Methods for Dynamical Systems","author":"L Brim","year":"2013","unstructured":"Brim, L., \u010ce\u0161ka, M., \u0160afr\u00e1nek, D.: Model checking of biological systems. In: Bernardo, M., de Vink, E., Di Pierro, A., Wiklicky, H. (eds.) SFM 2013. LNCS, vol. 7938, pp. 63\u2013112. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38874-3_3"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Brim, L., Fabrikov\u00e1, J., Drazan, S., Safr\u00e1nek, D.: Reachability in biochemical dynamical systems by quantitative discrete approximation. CoRR, abs\/1107.5924 (2011)","DOI":"10.4204\/EPTCS.67.9"},{"key":"15_CR7","doi-asserted-by":"crossref","DOI":"10.1002\/9780470753767","volume-title":"Numerical Methods for Ordinary Differential Equations","author":"J Butcher","year":"2008","unstructured":"Butcher, J.: Numerical Methods for Ordinary Differential Equations, 2nd edn. Wiley, Chichester (2008)","edition":"2"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-662-54580-5_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Cardelli","year":"2017","unstructured":"Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: ERODE: a tool for the evaluation and reduction of ordinary differential equations. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 310\u2013328. Springer, Heidelberg (2017). doi: 10.1007\/978-3-662-54580-5_19"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-642-33365-1_6","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"R Carter","year":"2012","unstructured":"Carter, R., Navarro-L\u00f3pez, E.M.: Dynamically-driven timed automaton abstractions for proving liveness of continuous systems. In: Jurdzi\u0144ski, M., Ni\u010dkovi\u0107, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 59\u201374. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33365-1_6"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/BFb0058022","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"EM Clarke","year":"1997","unstructured":"Clarke, E.M.: Model checking. In: Ramesh, S., Sivakumar, G. (eds.) FSTTCS 1997. LNCS, vol. 1346, pp. 54\u201356. Springer, Heidelberg (1997). doi: 10.1007\/BFb0058022"},{"key":"15_CR11","unstructured":"Cytoscape 3 ANIMO app. http:\/\/apps.cytoscape.org\/apps\/animo"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-642-25271-6_18","volume-title":"Formal Methods for Components and Objects","author":"A David","year":"2011","unstructured":"David, A., Grunnet, J.D., Jessen, J.J., Larsen, K.G., Rasmussen, J.I.: Application of model-checking technology to controller synthesis. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 336\u2013351. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-25271-6_18"},{"issue":"3","key":"15_CR13","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/s10009-014-0323-4","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B., Sedwards, S.: Statistical model checking for biological systems. Int. J. Softw. Tools Technol. Transfer 17(3), 351\u2013367 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"15_CR14","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). doi: 10.1007\/978-3-642-00602-9_12"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-10003-2_69","volume-title":"Automata, Languages and Programming","author":"EA Emerson","year":"1980","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 169\u2013181. Springer, Heidelberg (1980). doi: 10.1007\/3-540-10003-2_69"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Fehnker, A.: Scheduling a steel plant with timed automata. In: Proceedings of the Sixth International Conference on Real-Time Computing Systems and Applications, RTCSA 1999, p. 280. IEEE Computer Society, Washington, DC (1999)","DOI":"10.1109\/RTCSA.1999.811256"},{"key":"15_CR17","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/j.entcs.2013.02.019","volume":"293","author":"SV Goethem","year":"2013","unstructured":"Goethem, S.V., Jacquet, J.-M., Brim, L., \u0160afr\u00e1nek, D.: Timed modelling of gene networks with arbitrarily precise expression discretization. Electron. Notes Theoret. Comput. Sci. 293, 67\u201381 (2013). Proceedings of the Third International Workshop on Interactions Between Computer Science and Biology (CS2Bio 2012)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/3-540-45351-2_23","volume-title":"Hybrid Systems: Computation and Control","author":"LCGJM Habets","year":"2001","unstructured":"Habets, L.C.G.J.M., van Schuppen, J.H.: Control of piecewise-linear hybrid systems on simplices and rectangles. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 261\u2013274. Springer, Heidelberg (2001). doi: 10.1007\/3-540-45351-2_23"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Habets, L.C.G.J.M., van Schuppen, J.H.: Control to facet problems for affine systems on simplices and polytopes - with applications to control of hybrid systems. In: Proceedings of the 44th IEEE Conference on Decision and Control, pp. 4175\u20134180, December 2005","DOI":"10.1109\/CDC.2005.1582817"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Jongerden, M., Haverkort, B., Bohnenkamp, H., Katoen, J.: Maximizing system lifetime by battery scheduling. In: 39th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks, DSN 2009, Los Alamitos. IEEE Computer Society Press, June 2009","DOI":"10.1109\/DSN.2009.5270351"},{"key":"15_CR21","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/978-1-60761-175-2_12","volume":"563","author":"S Killcoyne","year":"2009","unstructured":"Killcoyne, S., Carter, G.W., Smith, J., Boyle, J.: Cytoscape: a community-based framework for network modeling. Methods Mol. Biol. (Clifton, N.J.) 563, 219\u2013239 (2009)","journal-title":"Methods Mol. Biol. (Clifton, N.J.)"},{"key":"15_CR22","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. (STTT) 1, 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","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, pp. 154\u2013169. Springer, Heidelberg (2000). doi: 10.1007\/10722167_15"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-68413-8_6","volume-title":"Formal Methods in Systems Biology","author":"O Maler","year":"2008","unstructured":"Maler, O., Batt, G.: Approximating continuous systems by timed automata. In: Fisher, J. (ed.) FMSB 2008. LNCS, vol. 5054, pp. 77\u201389. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-68413-8_6"},{"issue":"16","key":"15_CR25","doi-asserted-by":"crossref","first-page":"i227","DOI":"10.1093\/bioinformatics\/btn275","volume":"24","author":"PT Monteiro","year":"2008","unstructured":"Monteiro, P.T., Ropers, D., Mateescu, R., Freitas, A.T., de Jong, H.: Temporal logic patterns for querying dynamic models of cellular interaction networks. Bioinformatics 24(16), i227\u2013i233 (2008)","journal-title":"Bioinformatics"},{"key":"15_CR26","unstructured":"PPlane. http:\/\/math.rice.edu\/~dfield\/dfpp.html"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Schivo, S., Scholma, J., Karperien, H.B.J., Post, J.N., van de Pol, J.C., Langerak, R.: Setting parameters for biological models with ANIMO. In: Andr\u00e9, E., Frehse, G. (eds.) Proceedings 1st International Workshop on Synthesis of Continuous Parameters, Grenoble, France. Electronic Proceedings in Theoretical Computer Science, vol. 145, pp. 35\u201347. Open Publishing Association, April 2014","DOI":"10.4204\/EPTCS.145.5"},{"issue":"1","key":"15_CR28","doi-asserted-by":"crossref","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, P.E., Karperien, M., Post, J.N., van de Pol, J., Langerak, R.: Modelling with ANIMO: between fuzzy logic and differential equations. BMC Syst. Biol. 10(1), 56 (2016)","journal-title":"BMC Syst. Biol."},{"issue":"3","key":"15_CR29","doi-asserted-by":"crossref","first-page":"832","DOI":"10.1109\/JBHI.2013.2292880","volume":"18","author":"S Schivo","year":"2013","unstructured":"Schivo, S., Scholma, J., Wanders, B., Urquidi Camacho, R., van der Vet, P., Karperien, M., Langerak, R., van de Pol, J., Post, J.: Modelling biological pathway dynamics with Timed Automata. IEEE J. Biomed. Health Inform. 18(3), 832\u2013839 (2013)","journal-title":"IEEE J. Biomed. Health Inform."},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"Schivo, S., Scholma, J., Wanders, B., Urquidi Camacho, R.A., van der Vet, P.E., Karperien, H.B.J., Langerak, R., van de Pol, J.C., Post, J.N.: Modelling biological pathway dynamics with timed automata. In: 12th IC on Bioinformatics and Bioengineering (BIBE 2012), pp. 447\u2013453. IEEE Computer Society (2012)","DOI":"10.1109\/BIBE.2012.6399719"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Scholma, J., Kerkhofs, J., Schivo, S., Langerak, R., van der Vet, P.E., Karperien, H.B.J., van de Pol, J.C., Geris, L., Post, J.N.: Mathematical modeling of signalingpathways in osteoarthritis. In: Lohmander, S. (ed.) 2013 Osteoarthritis Research Society International (OARSI) World Congress, Philadelphia, USA, vol. 21, Supplement, p. S123. Elsevier, Amsterdam, April 2013","DOI":"10.1016\/j.joca.2013.02.259"},{"key":"15_CR32","unstructured":"Scholma, J., Schivo, S., Kerkhofs, J., Langerak, R., Karperien, H.B.J., van de Pol, J.C., Geris, L., Post, J.N.: ECHO: the executable chondrocyte. In: Tissue Engineering & Regenerative Medicine International Society, European Chapter Meeting, Genova, Italy, vol. 8, p. 54. Wiley, Malden, June 2014"},{"issue":"1","key":"15_CR33","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1016\/j.gene.2013.10.010","volume":"533","author":"J Scholma","year":"2014","unstructured":"Scholma, J., Schivo, S., Urquidi Camacho, R., van de Pol, J., Karperien, M., Post, J.: Biological networks 101: computational modeling for molecular biologists. Gene 533(1), 379\u2013384 (2014)","journal-title":"Gene"},{"issue":"3","key":"15_CR34","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1016\/j.tcs.2007.11.010","volume":"391","author":"H Siebert","year":"2008","unstructured":"Siebert, H., Bockmayr, A.: Temporal constraints in the logical analysis of regulatory networks. Theoret. Comput. Sci. 391(3), 258\u2013275 (2008). Converging Sciences: Informatics and Biology","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"15_CR35","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/s10703-011-0118-0","volume":"39","author":"C Sloth","year":"2011","unstructured":"Sloth, C., Wisniewski, R.: Verification of continuous dynamical systems by timed automata. Formal Methods Syst. Des. 39(1), 47\u201382 (2011)","journal-title":"Formal Methods Syst. Des."},{"issue":"1","key":"15_CR36","first-page":"80","volume":"7","author":"C Sloth","year":"2013","unstructured":"Sloth, C., Wisniewski, R.: Complete abstractions of dynamical systems by timed automata. Nonlinear Anal.: Hybrid Syst. 7(1), 80\u2013100 (2013). (IFAC) World Congress 2011","journal-title":"Nonlinear Anal.: Hybrid Syst."},{"issue":"1","key":"15_CR37","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1076\/1387-3954(200003)6:1;1-Q;FT051","volume":"6","author":"O Stursberg","year":"2000","unstructured":"Stursberg, O., Kowalewski, S., Engell, S.: On the generation of timed discrete approximations for continuous systems. Math. Comput. Modell. Dyn. Syst. 6(1), 51\u201370 (2000)","journal-title":"Math. Comput. Modell. Dyn. Syst."},{"key":"15_CR38","unstructured":"UPPAAL. www.uppaal.org"},{"key":"15_CR39","unstructured":"Urquidi Camacho, R.: Modeling osteoarthritic cartilage with ANIMO: an executable biology approach to osteoarthritic signaling and gene expression. Master\u2019s thesis, University of Twente, The Netherlands, July 2013"},{"issue":"2","key":"15_CR40","doi-asserted-by":"crossref","first-page":"79","DOI":"10.4173\/mic.2011.2.3","volume":"32","author":"R Wisniewski","year":"2011","unstructured":"Wisniewski, R., Sloth, C.: Abstraction of dynamical systems by timed automata. Model. Ident. Control 32(2), 79 (2011)","journal-title":"Model. Ident. Control"},{"key":"15_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-642-16561-0_20","volume-title":"Leveraging Applications of Formal Methods, Verification, and Validation","author":"J Xing","year":"2010","unstructured":"Xing, J., Theelen, B.D., Langerak, R., van de Pol, J., Tretmans, J., Voeten, J.P.M.: UPPAAL in practice: quantitative verification of a RapidIO network. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6416, pp. 160\u2013174. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-16561-0_20"}],"container-title":["Lecture Notes in Computer Science","ModelEd, TestEd, TrustEd"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68270-9_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T19:51:53Z","timestamp":1570132313000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68270-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319682693","9783319682709"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68270-9_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}