{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T22:56:04Z","timestamp":1776552964483,"version":"3.51.2"},"publisher-location":"Cham","reference-count":12,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319737201","type":"print"},{"value":"9783319737218","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T00:00:00Z","timestamp":1514505600000},"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-73721-8_22","type":"book-chapter","created":{"date-parts":[[2017,12,28]],"date-time":"2017-12-28T04:13:05Z","timestamp":1514434385000},"page":"474-494","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Revisiting MITL to Fix Decision Procedures"],"prefix":"10.1007","author":[{"given":"Nima","family":"Roohi","sequence":"first","affiliation":[]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,12,29]]},"reference":[{"issue":"2","key":"22_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. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"22_CR2","doi-asserted-by":"crossref","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":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-540-78499-9_12","volume-title":"Foundations of Software Science and Computational Structures","author":"P Bouyer","year":"2008","unstructured":"Bouyer, P., Markey, N., Reynier, P.-A.: Robust analysis of timed automata via channel machines. In: Amadio, R. (ed.) FoSSaCS 2008. LNCS, vol. 4962, pp. 157\u2013171. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78499-9_12"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-40229-6_4","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"T Brihaye","year":"2013","unstructured":"Brihaye, T., Esti\u00e9venart, M., Geeraerts, G.: On MITL and alternating timed automata. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 47\u201361. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-40229-6_4"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-10512-3_6","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"T Brihaye","year":"2014","unstructured":"Brihaye, T., Esti\u00e9venart, M., Geeraerts, G.: On MITL and alternating timed automata over infinite words. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 69\u201384. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-10512-3_6"},{"issue":"1","key":"22_CR6","first-page":"1","volume":"62","author":"Y Hirshfeld","year":"2004","unstructured":"Hirshfeld, Y., Rabinovich, A.: Logics for Real Time: Decidability and Complexity. Fundam. Inf. 62(1), 1\u201328 (2004)","journal-title":"Fundam. Inf."},{"issue":"4","key":"22_CR7","doi-asserted-by":"crossref","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 Systems 2(4), 255\u2013299 (1990)","journal-title":"Real-Time Systems"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/11867340_20","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"O Maler","year":"2006","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: From MITL to timed automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 274\u2013289. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11867340_20"},{"key":"22_CR9","unstructured":"Madhavan M.: Finite-state Automata on Infinite Inputs (1996)"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-85778-5_1","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"J Ouaknine","year":"2008","unstructured":"Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 1\u201313. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-85778-5_1"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). \nhttps:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The Temporal Logic of Programs. In: SFCS, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-73721-8_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,12,28]],"date-time":"2017-12-28T04:26:52Z","timestamp":1514435212000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-73721-8_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,29]]},"ISBN":["9783319737201","9783319737218"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-73721-8_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,29]]}}}