{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:59:04Z","timestamp":1776333544675,"version":"3.51.2"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319633862","type":"print"},{"value":"9783319633879","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63387-9_21","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:43Z","timestamp":1499849623000},"page":"421-440","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":22,"title":["MightyL: A Compositional Translation from MITL to Timed Automata"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Brihaye","sequence":"first","affiliation":[]},{"given":"Gilles","family":"Geeraerts","sequence":"additional","affiliation":[]},{"given":"Hsi-Ming","family":"Ho","sequence":"additional","affiliation":[]},{"given":"Benjamin","family":"Monmege","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"issue":"1\/2","key":"21_CR1","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1504\/IJCCBS.2014.059593","volume":"5","author":"N Abid","year":"2014","unstructured":"Abid, N., Dal-Zilio, S., Botlan, D.L.: A formal framework to specify and verify real-time properties on critical systems. Int. J. Crit. Comput.-Based Syst. 5(1\/2), 4\u201330 (2014)","journal-title":"Int. J. Crit. Comput.-Based Syst."},{"issue":"2","key":"21_CR2","doi-asserted-by":"publisher","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(2), 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"21_CR3","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"},{"issue":"1","key":"21_CR4","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/inco.1993.1025","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. Inf. Comput. 104(1), 35\u201377 (1993)","journal-title":"Inf. Comput."},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"863","DOI":"10.1007\/978-3-642-39799-8_60","volume-title":"Computer Aided Verification","author":"J Barnat","year":"2013","unstructured":"Barnat, J., et al.: DiVinE 3.0 \u2013 an explicit-state model checker for multithreaded C & C++ programs. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 863\u2013868. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39799-8_60"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-642-40708-6_13","volume-title":"Computational Methods in Systems Biology","author":"E Bartocci","year":"2013","unstructured":"Bartocci, E., Bortolussi, L., Nenzi, L.: A temporal logic approach to modular design of synthetic biological circuits. In: Gupta, A., Henzinger, T.A. (eds.) CMSB 2013. LNCS, vol. 8130, pp. 164\u2013177. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-40708-6_13"},{"issue":"2","key":"21_CR7","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/s00236-015-0229-y","volume":"53","author":"MM Bersani","year":"2016","unstructured":"Bersani, M.M., Rossi, M., San Pietro, P.: A tool for deciding the satisfiability of continuous-time metric temporal logic. Acta Inform. 53(2), 171\u2013206 (2016)","journal-title":"Acta Inform."},{"issue":"4","key":"21_CR8","doi-asserted-by":"publisher","first-page":"727","DOI":"10.1142\/S0129054107004942","volume":"18","author":"R Bloem","year":"2007","unstructured":"Bloem, R., Cimatti, A., Pill, I., Roveri, M.: Symbolic implementation of alternating automata. Int. J. Found. Comput. Sci. 18(4), 727\u2013743 (2007)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/978-3-319-41528-4_28","volume-title":"Computer Aided Verification","author":"P Bouyer","year":"2016","unstructured":"Bouyer, P., Colange, M., Markey, N.: Symbolic optimal reachability in weighted timed automata. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 513\u2013530. Springer, Cham (2016). doi:10.1007\/978-3-319-41528-4_28"},{"key":"21_CR10","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). doi:10.1007\/978-3-642-40229-6_4"},{"key":"21_CR11","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). doi:10.1007\/978-3-319-10512-3_6"},{"issue":"3\u20134","key":"21_CR12","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/s00236-013-0189-z","volume":"51","author":"PE Bulychev","year":"2014","unstructured":"Bulychev, P.E., David, A., Larsen, K.G., Li, G.: Efficient controller synthesis for a fragment of MTL$$_{0,\\infty }$$. Acta Inform. 51(3\u20134), 165\u2013192 (2014)","journal-title":"Acta Inform."},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). doi:10.1007\/3-540-45657-0_29"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Claessen, K., Een, N., Sterin, B.: A circuit approach to LTL model checking. In: FMCAD 2013. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679391"},{"issue":"9","key":"21_CR15","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L De Moura","year":"2011","unstructured":"De Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Dokhanchi, A., Hoxha, B., Fainekos, G.: Formal requirement debugging for testing and verification of cyber-physical systems. Research report 1607.02549. arXiv (2016)","DOI":"10.4204\/EPTCS.232.4"},{"key":"21_CR17","unstructured":"D\u2019Souza, D., Matteplackel, R.: A clock-optimal hierarchical monitoring automaton construction for MITL. Research report 2013\u20131, IIS (2013). http:\/\/www.csa.iisc.ernet.in\/TR\/2013\/1\/lics2013-tr.pdf"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Fu, J., Topcu, U.: Computational methods for stochastic control with metric interval temporal logic specifications. In: CDC 2015, pp. 7440\u20137447. IEEE (2015)","DOI":"10.1109\/CDC.2015.7403395"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53\u201365. Springer, Heidelberg (2001). doi:10.1007\/3-540-44585-4_6"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: PSTV 1995. pp. 3\u201318. Chapman & Hall (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-540-31980-1_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Hammer","year":"2005","unstructured":"Hammer, M., Knapp, A., Merz, S.: Truly on-the-fly LTL model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 191\u2013205. Springer, Heidelberg (2005). doi:10.1007\/978-3-540-31980-1_13"},{"issue":"1","key":"21_CR22","first-page":"1","volume":"62","author":"Y Hirshfeld","year":"2004","unstructured":"Hirshfeld, Y., Rabinovich, A.M.: Logics for real time: decidability and complexity. Fundam. Informaticae 62(1), 1\u201328 (2004)","journal-title":"Fundam. Informaticae"},{"key":"21_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/11821069_43","volume-title":"Mathematical Foundations of Computer Science 2006","author":"Y Hirshfeld","year":"2006","unstructured":"Hirshfeld, Y., Rabinovich, A.: An expressive temporal logic for real time. In: Kr\u00e1lovi\u010d, R., Urzyczyn, P. (eds.) MFCS 2006. LNCS, vol. 4162, pp. 492\u2013504. Springer, Heidelberg (2006). doi:10.1007\/11821069_43"},{"key":"21_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692\u2013707. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46681-0_61"},{"key":"21_CR25","unstructured":"Karaman, S.: Optimal planning with temporal logic specifications. Master\u2019s thesis, Massachussetts Institute of Technology (2009)"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. In: ISTCS 1997, pp. 147\u2013158. IEEE (1997)","DOI":"10.1109\/ISTCS.1997.595167"},{"issue":"1\u20132","key":"21_CR27","doi-asserted-by":"publisher","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. Transfer 1(1\u20132), 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"21_CR28","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). doi:10.1007\/11867340_20"},{"key":"21_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/3-540-16761-7_77","volume-title":"Automata, Languages and Programming","author":"DE Muller","year":"1986","unstructured":"Muller, D.E., Saoudi, A., Schupp, P.E.: Alternating automata, the weak monadic theory of the tree, and its complexity. In: Kott, L. (ed.) ICALP 1986. LNCS, vol. 226, pp. 275\u2013283. Springer, Heidelberg (1986). doi:10.1007\/3-540-16761-7_77"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: On the decidability and complexity of metric temporal logic over finite words. In: Logical Methods in Computer Science, vol. 3, no. 1 (2007)","DOI":"10.2168\/LMCS-3(1:8)2007"},{"key":"21_CR31","doi-asserted-by":"publisher","first-page":"151","DOI":"10.3233\/AIC-150682","volume":"29","author":"E Plaku","year":"2016","unstructured":"Plaku, E., Karaman, S.: Motion planning with temporal-logic specifications: progress and challenges. AI Communications 29, 151\u2013162 (2016)","journal-title":"AI Communications"},{"key":"21_CR32","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS 1977. pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"3","key":"21_CR33","first-page":"247","volume":"4","author":"JF Raskin","year":"1999","unstructured":"Raskin, J.F., Schobbens, P.Y.: The logic of event clocks: decidability, complexity and expressiveness. J. Automata Lang. Comb. 4(3), 247\u2013282 (1999)","journal-title":"J. Automata Lang. Comb."},{"key":"21_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/978-3-642-21437-0_31","volume-title":"FM 2011: Formal Methods","author":"KY Rozier","year":"2011","unstructured":"Rozier, K.Y., Vardi, M.Y.: A multi-encoding approach for LTL symbolic satisfiability checking. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 417\u2013431. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-21437-0_31"},{"key":"21_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-662-46681-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Thierry-Mieg","year":"2015","unstructured":"Thierry-Mieg, Y.: Symbolic model-checking using ITS-tools. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 231\u2013237. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46681-0_20"},{"key":"21_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"MY Vardi","year":"1996","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238\u2013266. Springer, Heidelberg (1996). doi:10.1007\/3-540-60915-6_6"},{"key":"21_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"694","DOI":"10.1007\/3-540-58468-4_191","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"T Wilke","year":"1994","unstructured":"Wilke, T.: Specifying timed state sequences in powerful decidable logics and timed automata. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994. LNCS, vol. 863, pp. 694\u2013715. Springer, Heidelberg (1994). doi:10.1007\/3-540-58468-4_191"},{"key":"21_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-540-78800-3_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M de Wulf","year":"2008","unstructured":"de Wulf, M., Doyen, L., Maquet, N., Raskin, J.-F.: Antichains: alternative algorithms for LTL satisfiability and model-checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 63\u201377. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-78800-3_6"},{"key":"21_CR39","doi-asserted-by":"crossref","unstructured":"Zhou, Y., Maity, D., Baras, J.S.: Timed automata approach for motion planning using metric interval temporal logic. Research report 1603.08246. arXiv (2016)","DOI":"10.1109\/ECC.2016.7810369"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63387-9_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T01:09:55Z","timestamp":1750554595000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63387-9_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633862","9783319633879"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63387-9_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}