{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,15]],"date-time":"2026-07-15T14:30:30Z","timestamp":1784125830068,"version":"3.55.0"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319238197","type":"print"},{"value":"9783319238203","type":"electronic"}],"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-23820-3_23","type":"book-chapter","created":{"date-parts":[[2015,9,19]],"date-time":"2015-09-19T14:21:39Z","timestamp":1442672499000},"page":"323-341","source":"Crossref","is-referenced-by-count":9,"title":["Machine Learning Methods in Statistical Model Checking and System Design \u2013 Tutorial"],"prefix":"10.1007","author":[{"given":"Luca","family":"Bortolussi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dimitrios","family":"Milios","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Guido","family":"Sanguinetti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,11,15]]},"reference":[{"key":"23_CR1","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.: Model checking continuous-time Markov chains by transient analysis. In: Proceedings of CAV, pp. 358\u2013372 (2000)","DOI":"10.1007\/10722167_28"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Katoen, J.-P., Khattri, M., Zapreevt, I.S.: A markov reward model checker. In: Proceedings of QEST, pp. 243\u2013244 (2005)","DOI":"10.1109\/QEST.2005.2"},{"issue":"6","key":"23_CR5","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1049\/iet-syb.2010.0005","volume":"4","author":"M Mateescu","year":"2010","unstructured":"Mateescu, M., Wolf, V., Didier, F., Henzinger, T.: Fast adaptive uniformisation of the chemical master equation. IET Syst. Biol. 4(6), 441\u2013452 (2010)","journal-title":"IET Syst. Biol."},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Proceeding of RV, pp. 122\u2013135 (2010)","DOI":"10.1007\/978-3-642-16612-9_11"},{"issue":"9","key":"23_CR7","doi-asserted-by":"publisher","first-page":"1368","DOI":"10.1016\/j.ic.2006.05.002","volume":"204","author":"HL Younes","year":"2006","unstructured":"Younes, H.L., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Inf. Comput. 204(9), 1368\u20131409 (2006)","journal-title":"Inf. Comput."},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to simulink\/stateflow verification. In: Proceedings of HSCC, pp. 243\u2013252 (2010)","DOI":"10.21236\/ADA531406"},{"key":"23_CR9","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)"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1007\/978-3-319-12982-2_7","volume-title":"Computational Methods in Systems Biology","author":"M \u010ce\u0161ka","year":"2014","unstructured":"\u010ce\u0161ka, M., Dannenberg, F., Kwiatkowska, M., Paoletti, N.: Precise parameter synthesis for stochastic biochemical systems. In: Mendes, P., Dada, J.O., Smallbone, K. (eds.) CMSB 2014. LNCS, vol. 8859, pp. 86\u201398. Springer, Heidelberg (2014)"},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-40196-1_7","volume-title":"Quantitative Evaluation of Systems","author":"L Bortolussi","year":"2013","unstructured":"Bortolussi, L., Sanguinetti, G.: Learning and designing stochastic processes from logical constraints. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 89\u2013105. Springer, Heidelberg (2013)"},{"key":"23_CR12","unstructured":"Bortolussi, L., Milios, D., Sanguinetti, G.: Smoothed model checking for uncertain continuous time Markov chains. CoRR \n                      arXiv:1402.1450"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: On the robustness of temporal properties for stochastic models. In: Proceedings of HSB, vol. 125. EPTCS, pp. 3\u201319 (2013)","DOI":"10.4204\/EPTCS.125.1"},{"issue":"2:3","key":"23_CR14","first-page":"1","volume":"11","author":"L Bortolussi","year":"2015","unstructured":"Bortolussi, L., Sanguinetti, G.: Learning and designing stochastic processes from logical constraints. Logical Methods Comput. Sci. 11(2:3), 1\u201324 (2015)","journal-title":"Logical Methods Comput. Sci."},{"key":"23_CR15","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. Theoret. Comput. Sci. 587, 3\u201325 (2015)","journal-title":"Theoret. Comput. Sci."},{"key":"23_CR16","series-title":"Lecture Notes in Computer Science","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.: U-Check: model checking and parameter synthesis under uncertainty. In: Campos, J., Haverkort, B.R. (eds.) QEST 2015. LNCS, vol. 9259, pp. 89\u2013104. Springer, Heidelberg (2015)"},{"key":"23_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4614-3615-7","volume-title":"Essentials of Stochastic Processes","author":"R Durrett","year":"2012","unstructured":"Durrett, R.: Essentials of Stochastic Processes. Springer, Berlin (2012)"},{"issue":"5","key":"23_CR18","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/j.peva.2013.01.001","volume":"70","author":"L Bortolussi","year":"2013","unstructured":"Bortolussi, L., Hillston, J., Latella, D., Massink, M.: Continuous approximation of collective systems behaviour: a tutorial. Perform. Eval. 70(5), 317\u2013349 (2013)","journal-title":"Perform. Eval."},{"issue":"1","key":"23_CR19","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116\u2013146 (1996)","journal-title":"J. ACM"},{"key":"23_CR20","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 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004)"},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-15297-9_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92\u2013106. Springer, Heidelberg (2010)"},{"key":"23_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-642-39799-8_19","volume-title":"Computer Aided Verification","author":"A Donz\u00e9","year":"2013","unstructured":"Donz\u00e9, A., Ferr\u00e8re, T., Maler, O.: Efficient robust monitoring for STL. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 264\u2013279. Springer, Heidelberg (2013)"},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-24310-3_4","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"T Chen","year":"2011","unstructured":"Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Time-bounded verification of CTMCs against real-time specifications. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 26\u201342. Springer, Heidelberg (2011)"},{"issue":"25","key":"23_CR24","doi-asserted-by":"publisher","first-page":"2340","DOI":"10.1021\/j100540a008","volume":"81","author":"DT Gillespie","year":"1977","unstructured":"Gillespie, D.T.: Exact stochastic simulation of coupled chemical reactions. J. Phys. Chem. 81(25), 2340\u20132361 (1977)","journal-title":"J. Phys. Chem."},{"key":"23_CR25","volume-title":"Pattern Recognition and Machine Learning","author":"CM Bishop","year":"2006","unstructured":"Bishop, C.M.: Pattern Recognition and Machine Learning. Springer, Berlin (2006)"},{"key":"23_CR26","volume-title":"Gaussian Processes for Machine Learning","author":"CE Rasmussen","year":"2006","unstructured":"Rasmussen, C.E., Williams, C.K.I.: Gaussian Processes for Machine Learning. MIT Press, Caambridge (2006)"},{"key":"23_CR27","first-page":"67","volume":"2","author":"I Steinwart","year":"2002","unstructured":"Steinwart, I.: On the influence of the kernel on the consistency of support vector machines. J. Mach. Lear. Res. 2, 67\u201393 (2002)","journal-title":"J. Mach. Lear. Res."},{"key":"23_CR28","first-page":"1","volume":"1","author":"A Andreychenko","year":"2012","unstructured":"Andreychenko, A., Mikeev, L., Spieler, D., Wolf, V.: Approximate maximum likelihood estimation for stochastic chemical kinetics. EURASIP J. Bioinf. Syst. Biol. 1, 1\u201314 (2012)","journal-title":"EURASIP J. Bioinf. Syst. Biol."},{"key":"23_CR29","unstructured":"Opper, M., Sanguinetti, G.: Variational inference for Markov jump processes. In: Proceedings of NIPS, pp. 1105\u20131112 (2007)"},{"issue":"5","key":"23_CR30","doi-asserted-by":"publisher","first-page":"3250","DOI":"10.1109\/TIT.2011.2182033","volume":"58","author":"N Srinivas","year":"2012","unstructured":"Srinivas, N., Krause, A., Kakade, S., Seeger, M.: Information-theoretic regret bounds for Gaussian process optimisation in the bandit setting. IEEE Trans. Inf. Theory 58(5), 3250\u20133265 (2012)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"23_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/978-3-319-10512-3_3","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"E Bartocci","year":"2014","unstructured":"Bartocci, E., Bortolussi, L., Sanguinetti, G.: Data-driven statistical learning of temporal logic properties. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 23\u201337. Springer, Heidelberg (2014)"},{"issue":"33\u201334","key":"23_CR32","doi-asserted-by":"publisher","first-page":"3065","DOI":"10.1016\/j.tcs.2009.02.037","volume":"410","author":"F Ciocchetta","year":"2009","unstructured":"Ciocchetta, F., Hillston, J.: Bio-PEPA: a framework for the modelling and analysis of biological systems. Theoret. Comput. Sci. 410(33\u201334), 3065\u20133084 (2009)","journal-title":"Theoret. Comput. Sci."},{"key":"23_CR33","doi-asserted-by":"crossref","unstructured":"Bortolussi, L., Galpin, V., Hillston, J.: Hybrid performance modelling of opportunistic networks. In: EPTCS, vol. 85, pp. 106\u2013121 (2012)","DOI":"10.4204\/EPTCS.85.8"},{"key":"23_CR34","unstructured":"Bortolussi, L., Nenzi, L.: Specifying and monitoring properties of stochastic spatio-temporal systems in signal temporal logic. In: Proceedings of VALUETOOLS (2014)"},{"issue":"15","key":"23_CR35","doi-asserted-by":"publisher","first-page":"6959","DOI":"10.1063\/1.1505860","volume":"117","author":"EL Haseltine","year":"2002","unstructured":"Haseltine, E.L., Rawlings, J.B.: Approximate simulation of coupled fast and slow reactions for stochastic chemical kinetics. J. Chem. Phys. 117(15), 6959 (2002)","journal-title":"J. Chem. Phys."},{"key":"23_CR36","series-title":"Lecture Notes in Computer Science (Lecture Notes in Bioinformatics)","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-540-88562-7_20","volume-title":"Computational Methods in Systems Biology","author":"R Donaldson","year":"2008","unstructured":"Donaldson, R., Gilbert, D.: A model checking approach to the parameter estimation of biochemical pathways. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol. 5307, pp. 269\u2013287. Springer, Heidelberg (2008)"},{"key":"23_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/978-3-662-45231-8_30","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"S Bufo","year":"2014","unstructured":"Bufo, S., Bartocci, E., Sanguinetti, G., Borelli, M., Lucangelo, U., Bortolussi, L.: Temporal logic based monitoring of assisted ventilation in intensive care patients. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part II. LNCS, vol. 8803, pp. 391\u2013403. Springer, Heidelberg (2014)"},{"key":"23_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-19835-9_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Bartocci","year":"2011","unstructured":"Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 326\u2013340. Springer, Heidelberg (2011)"},{"key":"23_CR39","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/2562059.2562146","volume":"2014","author":"Z Kong","year":"2014","unstructured":"Kong, Z., Jones, A., Ayala, A.M., Gol, E.A., Belta, C.: Temporal logic inference for classification and prediction from data. Proc. HSCC 2014, 273\u2013282 (2014)","journal-title":"Proc. HSCC"},{"key":"23_CR40","doi-asserted-by":"crossref","unstructured":"Bortolussi, L., Milios, D., Sanguinetti, G.: Efficient stochastic simulation of systems with multiple time scales via statistical abstraction. In: Proceedings of CMSB (2015)","DOI":"10.1007\/978-3-319-23401-4_5"},{"key":"23_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1007\/978-3-662-45234-9_2","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"A Legay","year":"2014","unstructured":"Legay, A., Sedwards, S.: Statistical abstraction boosts design and test efficiency of evolving critical systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part I. LNCS, vol. 8802, pp. 4\u201325. Springer, Heidelberg (2014)"},{"key":"23_CR42","doi-asserted-by":"crossref","unstructured":"Georgoulas, A., Clark, A., Ocone, A., Gilmore, S., Sanguinetti, G.: A subsystems approach for parameter estimation of ode models of hybrid systems. In: Proceedings of HSB, vol. 92. EPTCS (2012)","DOI":"10.4204\/EPTCS.92.3"},{"key":"23_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/978-3-319-10696-0_21","volume-title":"Quantitative Evaluation of Systems","author":"A Georgoulas","year":"2014","unstructured":"Georgoulas, A., Hillston, J., Milios, D., Sanguinetti, G.: Probabilistic programming process algebra. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 249\u2013264. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23820-3_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T00:45:36Z","timestamp":1559263536000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-23820-3_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319238197","9783319238203"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23820-3_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}