{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T04:01:38Z","timestamp":1746417698658,"version":"3.40.4"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319105116"},{"type":"electronic","value":"9783319105123"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10512-3_6","type":"book-chapter","created":{"date-parts":[[2014,8,11]],"date-time":"2014-08-11T05:20:44Z","timestamp":1407734444000},"page":"69-84","source":"Crossref","is-referenced-by-count":3,"title":["On MITL and Alternating Timed Automata over Infinite Words"],"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":"6_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":"4","key":"6_CR2","first-page":"419","volume":"89","author":"P.A. Abdulla","year":"2008","unstructured":"Abdulla, P.A., Deneux, J., Ouaknine, J., Quaas, K., Worrell, J.: Universality Analysis for One-Clock Timed Automata. Fundam. Inform.\u00a089(4), 419\u2013450 (2008)","journal-title":"Fundam. Inform."},{"issue":"1","key":"6_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\u00a043(1), 116\u2013146 (1996)","journal-title":"J. ACM"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Bouyer, P.: Timed Automata may cause some troubles. Research Report LSV-02-9, Lab. Sp\u00e9cification et V\u00e9rification, CNRS & ENS de Cachan, France (2002)","DOI":"10.7146\/brics.v9i35.21750"},{"key":"6_CR5","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.\u00a08053, pp. 47\u201361. Springer, Heidelberg (2013)"},{"key":"6_CR6","unstructured":"Brihaye, T., Esti\u00e9venart, M., Geeraerts, G.: On MITL and Alternating Timed Automata over infinite words. Technical report arXiv.org., http:\/\/arxiv.org\/abs\/1406.4395"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata. Real-Time Systems, 73\u201381 (1996)","DOI":"10.1109\/REAL.1996.563702"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-15643-4_13","volume-title":"Automated Technology for Verification and Analysis","author":"G. Geeraerts","year":"2010","unstructured":"Geeraerts, G., Kalyon, G., Le Gall, T., Maquet, N., Raskin, J.-F.: Lattice-Valued Binary Decision Diagrams. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol.\u00a06252, pp. 158\u2013172. Springer, Heidelberg (2010)"},{"key":"6_CR10","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.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"issue":"4","key":"6_CR11","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"},{"issue":"3","key":"6_CR12","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Log.\u00a02(3), 408\u2013429 (2001)","journal-title":"ACM Trans. Comput. Log."},{"key":"6_CR13","unstructured":"Maquet, N.: New Algorithms and Data Structures for the Emptiness Problem of Alternating Automata. PhD thesis, Universit\u00e9 Libre de Bruxelles (2011)"},{"key":"6_CR14","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S. Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating Finite Automata on omega-Words. Theor. Comput. Sci.\u00a032, 321\u2013330 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: LICS 2005, pp. 188\u2013197. IEEE (2005)","DOI":"10.1109\/LICS.2005.33"},{"key":"6_CR16","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)","DOI":"10.2168\/LMCS-3(1:8)2007"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Parys, P., Walukiewicz, I.: Weak Alternating Timed Automata. Logical Methods in Computer Science\u00a08(3) (2012)","DOI":"10.2168\/LMCS-8(3:18)2012"}],"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-319-10512-3_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T03:55:00Z","timestamp":1746330900000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10512-3_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319105116","9783319105123"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10512-3_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}