{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T20:56:45Z","timestamp":1725742605333},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642402289"},{"type":"electronic","value":"9783642402296"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40229-6_4","type":"book-chapter","created":{"date-parts":[[2013,7,23]],"date-time":"2013-07-23T01:47:40Z","timestamp":1374544060000},"page":"47-61","source":"Crossref","is-referenced-by-count":9,"title":["On MITL and Alternating Timed Automata"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Brihaye","sequence":"first","affiliation":[]},{"given":"Morgane","family":"Esti\u00e9venart","sequence":"additional","affiliation":[]},{"given":"Gilles","family":"Geeraerts","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"4_CR1","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. Theor. Comput. Sci.\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"4_CR2","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"},{"issue":"2","key":"4_CR3","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput.\u00a098(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"unstructured":"Brihaye, T., Esti\u00e9venart, M., Geeraerts, G.: On MITL and alternating timed automata Technical report arXiv.org. \n                  \n                    http:\/\/arxiv.org\/abs\/1304.2814","key":"4_CR4"},{"doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press (2001)","key":"4_CR5","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"4_CR6","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. Wulf De","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.\u00a04963, pp. 63\u201377. Springer, Heidelberg (2008)"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-12002-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Doyen","year":"2010","unstructured":"Doyen, L., Raskin, J.-F.: Antichain algorithms for finite automata. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 2\u201322. Springer, Heidelberg (2010)"},{"unstructured":"Henzinger, T.A.: The temporal specification and verification of real-time systems. PhD thesis, Standford University (1991)","key":"4_CR8"},{"issue":"4","key":"4_CR9","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 Systems\u00a02(4), 255\u2013299 (1990)","journal-title":"Real-Time Systems"},{"doi-asserted-by":"crossref","unstructured":"Lasota, S., Walukiewicz, I.: Alternating timed automata. ACM Trans. Comput. Log.\u00a09(2) (2008)","key":"4_CR10","DOI":"10.1145\/1342991.1342994"},{"key":"4_CR11","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.\u00a04202, pp. 274\u2013289. Springer, Heidelberg (2006)"},{"unstructured":"Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: LICS 2005. IEEE (2005)","key":"4_CR12"},{"doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: On the decidability and complexity of metric temporal logic over finite words. Logical Methods in Computer Science\u00a03(1) (2007)","key":"4_CR13","DOI":"10.2168\/LMCS-3(1:8)2007"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-642-33386-6_8","volume-title":"Automated Technology for Verification and Analysis","author":"P.K. Pandya","year":"2012","unstructured":"Pandya, P.K., Shah, S.S.: The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower Bound Constraints. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 77\u201391. Springer, Heidelberg (2012)"},{"unstructured":"Raskin, J.-F., Schobbens, P.-Y.: The Logic of Event Clocks \u2013 Decidability, Complexity and Expressiveness. J. Automata, Languages and Combinatorics\u00a04(3) (1999)","key":"4_CR15"},{"unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: LICS 1986. IEEE (1986)","key":"4_CR16"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40229-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T02:50:16Z","timestamp":1557975016000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40229-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642402289","9783642402296"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40229-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}