{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T00:59:36Z","timestamp":1770339576233,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662452301","type":"print"},{"value":"9783662452318","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-45231-8_30","type":"book-chapter","created":{"date-parts":[[2014,9,26]],"date-time":"2014-09-26T15:42:39Z","timestamp":1411746159000},"page":"391-403","source":"Crossref","is-referenced-by-count":35,"title":["Temporal Logic Based Monitoring of Assisted Ventilation in Intensive Care Patients"],"prefix":"10.1007","author":[{"given":"Sara","family":"Bufo","sequence":"first","affiliation":[]},{"given":"Ezio","family":"Bartocci","sequence":"additional","affiliation":[]},{"given":"Guido","family":"Sanguinetti","sequence":"additional","affiliation":[]},{"given":"Massimo","family":"Borelli","sequence":"additional","affiliation":[]},{"given":"Umberto","family":"Lucangelo","sequence":"additional","affiliation":[]},{"given":"Luca","family":"Bortolussi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"30_CR1","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\u00a043(1), 116\u2013146 (1996)","journal-title":"J. ACM"},{"key":"30_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-29860-8_12","volume-title":"Runtime Verification","author":"E. Asarin","year":"2012","unstructured":"Asarin, E., Donz\u00e9, A., Maler, O., Nickovic, D.: Parametric Identification of Temporal Properties. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol.\u00a07186, pp. 147\u2013160. Springer, Heidelberg (2012)"},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: On the robustness of temporal properties for stochastic models. In: Proc. of HSB 2013, pp. 3\u201319 (2013)","DOI":"10.4204\/EPTCS.125.1"},{"key":"30_CR4","unstructured":"Bartocci, E., Bortolussi, L., Sanguinetti, G.: Learning temporal logical properties discriminating ECG models of cardiac arrhytmias. CoRR abs\/1312.7523 (2013)"},{"key":"30_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a08711, pp. 23\u201337. Springer, Heidelberg (2014)"},{"key":"30_CR6","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.\u00a07687, pp. 168\u2013182. Springer, Heidelberg (2013)"},{"key":"30_CR7","unstructured":"Bishop, C.M.: Pattern Recognition and Machine Learning. Springer (2006)"},{"key":"30_CR8","unstructured":"Blanch, L., Sales, B., Montanya, J., Lucangelo, U., Garcia-Esquirol, O., Villagra, A., Chacon, E., Estruga, A., Borelli, M., Burgue\u00f1o, M., Oliva, J., Fernandez, R., Villar, J., Kacmarek, R., Murias, G.: Validation of the better care system to detect ineffective efforts during expiration in mechanically ventilated patients: A pilot study. Intensive Care Med. (in press)"},{"key":"30_CR9","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.\u00a08054, pp. 89\u2013105. Springer, Heidelberg (2013)"},{"issue":"1","key":"30_CR10","doi-asserted-by":"publisher","first-page":"15","DOI":"10.4187\/respcare.00937","volume":"56","author":"R. Branson","year":"2011","unstructured":"Branson, R.: Patient-ventilator interaction: The last 40 years. Respir. Care\u00a056(1), 15\u201324 (2011)","journal-title":"Respir. Care"},{"key":"30_CR11","doi-asserted-by":"crossref","unstructured":"Bujorianu, M.L., Lygeros, J.: General stochastic hybrid systems. In: IEEE Mediterranean Conference on Control and Automation MED, vol.\u00a04, pp. 1872\u20131877 (2004)","DOI":"10.1109\/CDC.2004.1430320"},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"Calzone, L., Chabrier-Rivier, N., Fages, F., Soliman, S.: Machine learning biochemical networks from temporal logic properties. In: Priami, C., Plotkin, G. (eds.) Trans. on Comput. Syst. Biol. VI. LNCS (LNBI), vol.\u00a04220, pp. 68\u201394. Springer, Heidelberg (2006)","DOI":"10.1007\/11880646_4"},{"issue":"2","key":"30_CR13","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1097\/01.CCM.0000299734.34469.D9","volume":"36","author":"C. Chen","year":"2008","unstructured":"Chen, C., Lin, W., Hsu, C., Cheng, K., Lo, C.: Detecting ineffective triggering in the expiratory phase in mechanically ventilated patients based on airway flow and pressure deflection: Feasibility of using a computer algorithm. Crit. Care Med.\u00a036(2), 455\u2013461 (2008)","journal-title":"Crit. Care Med."},{"issue":"2","key":"30_CR14","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s10703-009-0076-y","volume":"36","author":"E. Clarke","year":"2010","unstructured":"Clarke, E., Donz\u00e9, A., Legay, A.: On simulation-based probabilistic model checking of mixed-analog circuits. Formal Methods in System Design\u00a036(2), 97\u2013113 (2010)","journal-title":"Formal Methods in System Design"},{"issue":"3","key":"30_CR15","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1159\/000264606","volume":"80","author":"A. Cuvelier","year":"2010","unstructured":"Cuvelier, A., Achour, L., Rabarimanantsoa, H., Letellier, C., Muir, J., Fauroux, B.: A noninvasive method to identify ineffective triggering in patients with noninvasive pressure support ventilation. Respiration\u00a080(3), 198\u2013206 (2010)","journal-title":"Respiration"},{"key":"30_CR16","doi-asserted-by":"crossref","unstructured":"Davis, M.: Markov Models and Optimization. Chapman & Hall (1993)","DOI":"10.1007\/978-1-4899-4483-2"},{"key":"30_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-33386-6_9","volume-title":"Automated Technology for Verification and Analysis","author":"A. Donz\u00e9","year":"2012","unstructured":"Donz\u00e9, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., Smolka, S.: On temporal logic and signal processing. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 92\u2013106. Springer, Heidelberg (2012)"},{"key":"30_CR18","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: Proc. of HSB 2012. EPTCS, vol.\u00a092 (2012)","DOI":"10.4204\/EPTCS.92.3"},{"issue":"3","key":"30_CR19","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/1467247.1467271","volume":"52","author":"R. Grosu","year":"2009","unstructured":"Grosu, R., Smolka, S.A., Corradini, F., Wasilewska, A., Entcheva, E., Bartocci, E.: Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM\u00a052(3), 97\u2013105 (2009)","journal-title":"Commun. ACM"},{"key":"30_CR20","unstructured":"Hoos, H.H., St\u00fctzle, T.: Stochastic local search: Foundations & applications. Elsevier (2004)"},{"key":"30_CR21","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.\u00a08174, pp. 149\u2013166. Springer, Heidelberg (2013)"},{"issue":"3","key":"30_CR22","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1586\/ers.09.13","volume":"3","author":"E. Kondili","year":"2009","unstructured":"Kondili, E., Akoumianaki, E., Alexopoulou, C., Georgopoulos, D.: Identifying and relieving asynchrony during mechanical ventilation. Expert Rev. Respir. Med.\u00a03(3), 231\u2013243 (2009)","journal-title":"Expert Rev. Respir. Med."},{"issue":"1","key":"30_CR23","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1093\/bja\/aeg129","volume":"91","author":"E. Kondili","year":"2003","unstructured":"Kondili, E., Prinianakis, G., Georgopoulos, D.: Patient-ventilator interaction. Br. J. Anaesth.\u00a091(1), 106\u2013119 (2003)","journal-title":"Br. J. Anaesth."},{"key":"30_CR24","doi-asserted-by":"crossref","unstructured":"Kong, Z., Jones, A., Ayala, A.M., Gol, E.A., Belta, C.: Temporal Logic Inference for Classification and Prediction from Data. In: Proc. of HSCC 2014 (2014)","DOI":"10.1145\/2562059.2562146"},{"key":"30_CR25","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R. Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst.\u00a02, 255\u2013299 (1990)","journal-title":"Real-Time Syst."},{"key":"30_CR26","doi-asserted-by":"crossref","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT 2004. LNCS, vol.\u00a03253, pp. 152\u2013166. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-30206-3_12"},{"issue":"3","key":"30_CR27","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/j.hrtlng.2014.02.002","volume":"43","author":"K. Mellott","year":"2014","unstructured":"Mellott, K., Grap, M., Munro, C., Sessler, C., Wetzel, P., Nilsestuen, J., Ketchum, J.: Patient ventilator asynchrony in critically ill adults: Frequency and types. Heart Lung\u00a043(3), 231\u2013243 (2014)","journal-title":"Heart Lung"},{"issue":"11","key":"30_CR28","doi-asserted-by":"publisher","first-page":"2014","DOI":"10.1007\/s00134-007-0767-z","volume":"33","author":"Q. Mulqueeny","year":"2007","unstructured":"Mulqueeny, Q., Ceriana, P., Carlucci, A., Fanfulla, F., Delmastro, M., Nava, S.: Automatic detection of ineffective triggering and double triggering during mechanical ventilation. Intensive Care Med.\u00a033(11), 2014\u20132018 (2007)","journal-title":"Intensive Care Med."},{"key":"30_CR29","doi-asserted-by":"crossref","unstructured":"Mulqueeny, Q., Redmond, S., Tassaux, D., Vignaux, L., Jolliet, P., Ceriana, P., Nava, S., Schindhelm, K., Lovell, N.: Automated detection of asynchrony in patient-ventilator interaction. In: Conf. Proc. IEEE Eng. Med. Biol. Soc., pp. 5324\u20135327 (2009)","DOI":"10.1109\/IEMBS.2009.5332684"},{"issue":"1","key":"30_CR30","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1097\/00075198-200102000-00005","volume":"7","author":"C. Sassoon","year":"2001","unstructured":"Sassoon, C., Foster, G.: Patient-ventilator asynchrony. Curr. Opin. Crit. Care\u00a07(1), 28\u201333 (2001)","journal-title":"Curr. Opin. Crit. Care"},{"key":"30_CR31","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1186\/cc13063","volume":"17","author":"C. Sinderby","year":"2013","unstructured":"Sinderby, C., Liu, S., Colombo, D., Camarotta, G., Slutsky, A., Navalesi, P., Beck, J.: An automated and standardized neural index to quantify patient-ventilator interaction. Critical Care\u00a017, 239 (2013)","journal-title":"Critical Care"},{"issue":"12","key":"30_CR32","doi-asserted-by":"publisher","first-page":"1433","DOI":"10.1038\/71012","volume":"5","author":"C. Sinderby","year":"1999","unstructured":"Sinderby, C., Navalesi, P., Beck, J., Skrobik, Y., Comtois, N., Friberg, S., Gottfried, S.B., Lindstr\u00f6m, L.: Neural control of mechanical ventilation in respiratory failure. Nat. Med.\u00a05(12), 1433\u20131436 (1999)","journal-title":"Nat. Med."},{"issue":"5","key":"30_CR33","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.M., Seeger, M.W.: Information-theoretic regret bounds for gaussian process optimization in the bandit setting. IEEE Transactions on Information Theory\u00a058(5), 3250\u20133265 (2012)","journal-title":"IEEE Transactions on Information Theory"},{"key":"30_CR34","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":"S.D. 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.\u00a07186, pp. 193\u2013207. Springer, Heidelberg (2012)"},{"issue":"10","key":"30_CR35","doi-asserted-by":"publisher","first-page":"1515","DOI":"10.1007\/s00134-006-0301-8","volume":"32","author":"A. Thille","year":"2006","unstructured":"Thille, A., Rodriguez, P., Cabello, B., Lellouche, F., Brochard, L.: Patient-ventilator asynchrony during assisted mechanical ventilation. Intensive Care Med.\u00a032(10), 1515\u20131522 (2006)","journal-title":"Intensive Care Med."},{"issue":"5","key":"30_CR36","doi-asserted-by":"publisher","first-page":"1059","DOI":"10.1164\/ajrccm.163.5.2005125","volume":"163","author":"M.J. Tobin","year":"2001","unstructured":"Tobin, M.J., Jubran, A., Laghi, F.: Patient-ventilator interaction. Am. J. Respir. Crit. Care Med.\u00a0163(5), 1059\u20131063 (2001)","journal-title":"Am. J. Respir. Crit. Care Med."},{"issue":"5","key":"30_CR37","doi-asserted-by":"publisher","first-page":"840","DOI":"10.1007\/s00134-009-1416-5","volume":"35","author":"L. Vignaux","year":"2009","unstructured":"Vignaux, L., Vargas, F., Roeseler, J., Tassaux, D., Thille, A., Kossowsky, M.P., Brochard, L., Jolliet, P.: Patient-ventilator asynchrony during non-invasive ventilation for acute respiratory failure: A multicenter study. Intensive Care Med.\u00a035(5), 840\u2013846 (2009)","journal-title":"Intensive Care Med."},{"issue":"10","key":"30_CR38","doi-asserted-by":"publisher","first-page":"2740","DOI":"10.1097\/CCM.0b013e3181a98a05","volume":"37","author":"M. Wit de","year":"2009","unstructured":"de Wit, M., Miller, K., Green, D., Ostman, H., Gennings, C., Epstein, S.: Ineffective triggering predicts increased duration of mechanical ventilation. Crit. Care Med.\u00a037(10), 2740\u20132745 (2009)","journal-title":"Crit. Care Med."},{"issue":"9","key":"30_CR39","doi-asserted-by":"publisher","first-page":"2240","DOI":"10.1097\/CCM.0b013e3182978cf1","volume":"41","author":"H. Wrigge","year":"2013","unstructured":"Wrigge, H., Reske, A.: Patient-ventilator asynchrony: Adapt the ventilator, not the patient! Crit. Care Med.\u00a041(9), 2240\u20132241 (2013)","journal-title":"Crit. Care Med."},{"key":"30_CR40","doi-asserted-by":"crossref","unstructured":"Xiaoqing, J., Donz\u00e9, A., Deshmukh, J.V., Seshia, S.A.: Mining Requirements from Closed-loop Control Models. In: Proc. of HSCC 2013, pp. 43\u201352. ACM (2013)","DOI":"10.1145\/2461328.2461337"},{"key":"30_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-34691-0_11","volume-title":"Testing Software and Systems","author":"H. Yang","year":"2012","unstructured":"Yang, H., Hoxha, B., Fainekos, G.: Querying Parametric Temporal Logic Properties on Embedded Systems. In: Nielsen, B., Weise, C. (eds.) ICTSS 2012. LNCS, vol.\u00a07641, pp. 136\u2013151. Springer, Heidelberg (2012)"},{"key":"30_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-540-24730-2_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H.L.S. Younes","year":"2004","unstructured":"Younes, H.L.S., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking: An empirical study. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 46\u201360. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-45231-8_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T21:15:03Z","timestamp":1746393303000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-45231-8_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662452301","9783662452318"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-45231-8_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}