{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:10:09Z","timestamp":1751663409094,"version":"3.41.0"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319929699"},{"type":"electronic","value":"9783319929705"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-92970-5_13","type":"book-chapter","created":{"date-parts":[[2018,5,29]],"date-time":"2018-05-29T12:54:12Z","timestamp":1527598452000},"page":"205-220","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["$$\\mathcal {P}revent$$: A Predictive Run-Time Verification Framework Using Statistical Learning"],"prefix":"10.1007","author":[{"given":"Reza","family":"Babaee","sequence":"first","affiliation":[]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[]},{"given":"Sebastian","family":"Fischmeister","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,5,30]]},"reference":[{"key":"13_CR1","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-642-35632-2_18","volume-title":"Runtime Verification","author":"E Bartocci","year":"2013","unstructured":"Bartocci, E., Grosu, R., Karmarkar, A., Smolka, S.A., Stoller, S.D., Zadok, E., Seyster, J.: Adaptive runtime verification. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 168\u2013182. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35632-2_18"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-77395-5_11","volume-title":"Runtime Verification","author":"A Bauer","year":"2007","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly? In: Sokolsky, O., Ta\u015f\u0131ran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 126\u2013138. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-77395-5_11"},{"issue":"3","key":"13_CR4","doi-asserted-by":"crossref","first-page":"651","DOI":"10.1093\/logcom\/exn075","volume":"20","author":"A Bauer","year":"2010","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Log. Comput. 20(3), 651\u2013674 (2010)","journal-title":"J. Log. Comput."},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Beal, M.J., Ghahramani, Z., Rasmussen, C.E.: The infinite hidden Markov model. In: Proceedings of the 14th International Conference on Neural Information Processing Systems: Natural and Synthetic, NIPS 2001, pp. 577\u2013584. MIT Press, Cambridge (2001)","DOI":"10.7551\/mitpress\/1120.003.0079"},{"key":"13_CR6","unstructured":"Bilmes, J.A.: A gentle tutorial of the EM algorithm and its applications to parameter estimation for Gaussian mixture and hidden Markov models. Technical report TR-97-021, International Computer Science Institute, Berkeley, CA (1997)"},{"key":"13_CR7","series-title":"Cambridge Series in Statistical and Probabilistic Mathematics","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511790485","volume-title":"Model Selection and Model Averaging","author":"G Claeskens","year":"2008","unstructured":"Claeskens, G., Hjort, N.L.: Model Selection and Model Averaging. Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, Cambridge (2008)"},{"issue":"3","key":"13_CR8","doi-asserted-by":"crossref","first-page":"31","DOI":"10.3390\/fi8030031","volume":"8","author":"S DeDeo","year":"2016","unstructured":"DeDeo, S.: Conflict and computation on Wikipedia: a finite-state machine analysis of editor interactions. Futur. Internet 8(3), 31 (2016)","journal-title":"Futur. Internet"},{"issue":"1","key":"13_CR9","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/s00446-003-0102-z","volume":"17","author":"M Duflot","year":"2004","unstructured":"Duflot, M., Fribourg, L., Picaronny, C.: Randomized dining philosophers without fairness assumption. Distrib. Comput. 17(1), 65\u201376 (2004)","journal-title":"Distrib. Comput."},{"key":"13_CR10","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511790492","volume-title":"Biological Sequence Analysis: Probabilistic Models of Proteins and Nucleic Acids","author":"R Durbin","year":"1998","unstructured":"Durbin, R., Eddy, S.R., Krogh, A., Mitchison, G.J.: Biological Sequence Analysis: Probabilistic Models of Proteins and Nucleic Acids. Cambridge University Press, Cambridge (1998)"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 1999 International Conference on Software Engineering, pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-04694-0_4","volume-title":"Runtime Verification","author":"Y Falcone","year":"2009","unstructured":"Falcone, Y., Fernandez, J.-C., Mounier, L.: Runtime verification of safety-progress properties. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, pp. 40\u201359. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04694-0_4"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-40787-1_9","volume-title":"Runtime Verification","author":"K Kalajdzic","year":"2013","unstructured":"Kalajdzic, K., Bartocci, E., Smolka, S.A., Stoller, S.D., Grosu, R.: Runtime verification with particle filtering. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 149\u2013166. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40787-1_9"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-319-47166-2_4","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"K Kalajdzic","year":"2016","unstructured":"Kalajdzic, K., Jegourel, C., Lukina, A., Bartocci, E., Legay, A., Smolka, S.A., Grosu, R.: Feedback control for statistical model checking of cyber-physical systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 46\u201361. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_4"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-75454-1_1","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"J-P Katoen","year":"2007","unstructured":"Katoen, J.-P.: Abstraction of probabilistic systems. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 1\u20133. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75454-1_1"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-72522-0_6","volume-title":"Formal Methods for Performance Evaluation","author":"M Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220\u2013270. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-72522-0_6"},{"issue":"5","key":"13_CR17","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebr. Program. 78(5), 293\u2013303 (2009)","journal-title":"J. Log. Algebr. Program."},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Mao, H., Chen, Y., Jaeger, M., Nielsen, T.D., Larsen, K.G., Nielsen, B.: Learning probabilistic automata for model checking. In: 2011 Eighth International Conference on Quantitative Evaluation of Systems, pp. 111\u2013120, September 2011","DOI":"10.1109\/QEST.2011.21"},{"key":"13_CR19","series-title":"The International Series on Discrete Event Dynamic Systems","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5711-1","volume-title":"Supervisory Control of Discrete Event Systems Using Petri Nets","author":"J Moody","year":"1998","unstructured":"Moody, J., Antsaklis, P.: Supervisory Control of Discrete Event Systems Using Petri Nets. The International Series on Discrete Event Dynamic Systems. Springer, New York (1998). https:\/\/doi.org\/10.1007\/978-1-4615-5711-1"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-28717-6_24","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A Morgenstern","year":"2012","unstructured":"Morgenstern, A., Gesell, M., Schneider, K.: An asymptotically correct finite path semantics for LTL. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 304\u2013319. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_24"},{"key":"13_CR21","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/j.sigpro.2014.03.045","volume":"104","author":"K Mukherjee","year":"2014","unstructured":"Mukherjee, K., Ray, A.: State splitting and merging in probabilistic finite state automata for signal representation and analysis. Sig. Process. 104, 105\u2013119 (2014)","journal-title":"Sig. Process."},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-319-11164-3_28","volume-title":"Runtime Verification","author":"A Nouri","year":"2014","unstructured":"Nouri, A., Raman, B., Bozga, M., Legay, A., Bensalem, S.: Faster statistical model checking by means of abstraction and learning. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 340\u2013355. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_28"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"13_CR24","unstructured":"Qnx neutrino rtos. http:\/\/blackberry.qnx.com\/en\/products\/neutrino-rtos\/neutrino-rtos . Accessed 14 Aug 2017"},{"key":"13_CR25","unstructured":"Rabin, M.O., Lehmann, D.: The advantages of free choice: a symmetric and fully distributed solution for the dining philosophers problem. In: Roscoe, A.W. (ed.) A Classical Mind, pp. 333\u2013352. Prentice Hall International (UK) Ltd., Hertfordshire (1994)"},{"issue":"2","key":"13_CR26","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1109\/5.18626","volume":"77","author":"LR Rabiner","year":"1989","unstructured":"Rabiner, L.R.: A tutorial on hidden Markov models and selected applications in speech recognition. Proc. IEEE 77(2), 257\u2013286 (1989)","journal-title":"Proc. IEEE"},{"key":"13_CR27","unstructured":"Radomised dining philosophers case study. http:\/\/www.prismmodelchecker.org\/casestudies\/phil.php . Accessed 24 Jan 2018"},{"issue":"2","key":"13_CR28","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1162\/089976699300016674","volume":"11","author":"ST Roweis","year":"1999","unstructured":"Roweis, S.T., Ghahramani, Z.: A unifying review of linear Gaussian models. Neural Comput. 11(2), 305\u2013345 (1999)","journal-title":"Neural Comput."},{"key":"13_CR29","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107298019","volume-title":"Understanding Machine Learning: From Theory to Algorithms","author":"S Shalev-Shwartz","year":"2014","unstructured":"Shalev-Shwartz, S., Ben-David, S.: Understanding Machine Learning: From Theory to Algorithms. Cambridge University Press, Cambridge (2014)"},{"key":"13_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-78163-9_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AP Sistla","year":"2008","unstructured":"Sistla, A.P., Srinivas, A.R.: Monitoring temporal properties of stochastic systems. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 294\u2013308. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78163-9_25"},{"key":"13_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"720","DOI":"10.1007\/978-3-642-22110-1_58","volume-title":"Computer Aided Verification","author":"AP Sistla","year":"2011","unstructured":"Sistla, A.P., \u017defran, M., Feng, Y.: Monitorability of stochastic dynamical systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 720\u2013736. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_58"},{"key":"13_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-642-29860-8_21","volume-title":"Runtime Verification","author":"AP Sistla","year":"2012","unstructured":"Sistla, A.P., \u017defran, M., Feng, Y.: Runtime monitoring of stochastic cyber-physical systems with hybrid state. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 276\u2013293. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_21"},{"key":"13_CR33","doi-asserted-by":"crossref","unstructured":"Sistla, A.P., Zefran, M., Feng, Y., Ben, Y.: Timely monitoring of partially observable stochastic systems. In: HSCC, 17th International Conference (Part of CPS Week), pp. 61\u201370 (2014)","DOI":"10.1145\/2562059.2562136"},{"key":"13_CR34","unstructured":"Stolcke, A., Omohundro, S.M.: Best-first model merging for hidden Markov model induction. CoRR, abs\/cmp-lg\/9405017 (1994)"},{"key":"13_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-642-29860-8_15","volume-title":"Runtime Verification","author":"SD Stoller","year":"2012","unstructured":"Stoller, S.D., Bartocci, E., Seyster, J., Grosu, R., Havelund, K., Smolka, S.A., Zadok, E.: Runtime verification with state estimation. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 193\u2013207. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_15"},{"key":"13_CR36","volume-title":"Distributed Systems - Principles and Paradigms","author":"AS Tanenbaum","year":"2007","unstructured":"Tanenbaum, A.S., van Steen, M.: Distributed Systems - Principles and Paradigms, 2nd edn. Pearson Education, London (2007)","edition":"2"},{"key":"13_CR37","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/3-540-45790-9_21","volume-title":"Grammatical Inference: Algorithms and Applications","author":"SA Terwijn","year":"2002","unstructured":"Terwijn, S.A.: On the learnability of hidden Markov models. In: Adriaans, P., Fernau, H., van Zaanen, M. (eds.) ICGI 2002. LNCS (LNAI), vol. 2484, pp. 261\u2013268. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45790-9_21"},{"issue":"2","key":"13_CR38","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1109\/TIT.1967.1054010","volume":"13","author":"AJ Viterbi","year":"1967","unstructured":"Viterbi, A.J.: Error bounds for convolutional codes and an asymptotically optimum decoding algorithm. IEEE Trans. Inf. Theory 13(2), 260\u2013269 (1967)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"13_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-642-16612-9_34","volume-title":"Runtime Verification","author":"CM Wilcox","year":"2010","unstructured":"Wilcox, C.M., Williams, B.C.: Runtime verification of stochastic, faulty systems. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 452\u2013459. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16612-9_34"},{"key":"13_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-319-46982-9_25","volume-title":"Runtime Verification","author":"A Yavolovsky","year":"2016","unstructured":"Yavolovsky, A., \u017defran, M., Sistla, A.P.: Decision-theoretic monitoring of cyber-physical systems. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 404\u2013419. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46982-9_25"},{"key":"13_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11562436_9","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2005","author":"L Zhang","year":"2005","unstructured":"Zhang, L., Hermanns, H., Jansen, D.N.: Logic and model checking for hidden Markov models. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 98\u2013112. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11562436_9"},{"issue":"99","key":"13_CR42","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/MIS.2017.3711639","volume":"PP","author":"X Zheng","year":"2017","unstructured":"Zheng, X., Julien, C., Podorozhny, R., Cassez, F., Rakotoarivelo, T.: Efficient and scalable runtime monitoring for cyber-physical system. IEEE Syst. J. PP(99), 1\u201312 (2017)","journal-title":"IEEE Syst. J."}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-92970-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:38:46Z","timestamp":1751661526000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-92970-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319929699","9783319929705"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-92970-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}