{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,19]],"date-time":"2025-10-19T15:50:09Z","timestamp":1760889009519},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2015,6,13]],"date-time":"2015-06-13T00:00:00Z","timestamp":1434153600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2016,4]]},"DOI":"10.1007\/s00236-015-0243-0","type":"journal-article","created":{"date-parts":[[2015,6,12]],"date-time":"2015-06-12T05:58:50Z","timestamp":1434088730000},"page":"301-324","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Metric temporal logic revisited"],"prefix":"10.1007","volume":"53","author":[{"given":"Mark","family":"Reynolds","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,6,13]]},"reference":[{"issue":"1","key":"243_CR1","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). doi: 10.1145\/227595.227602","journal-title":"J. ACM"},{"key":"243_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Logics and models of real time: a survey. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds.) REX Workshop. Lecture Notes in Computer Science, vol. 600, pp. 74\u2013106. Springer, Berlin (1991)","DOI":"10.1007\/BFb0031988"},{"issue":"1","key":"243_CR3","doi-asserted-by":"crossref","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."},{"issue":"1","key":"243_CR4","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R Alur","year":"1994","unstructured":"Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181\u2013203 (1994). doi: 10.1145\/174644.174651","journal-title":"J. ACM"},{"key":"243_CR5","doi-asserted-by":"crossref","unstructured":"Baier, C., Bertrand, N., Bouyer, P., Brihaye, T.: When are timed automata determinizable? In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 5556, pp. 43\u201354. Springer, Berlin (2009). doi: 10.1007\/978-3-642-02930-1_4","DOI":"10.1007\/978-3-642-02930-1_4"},{"key":"243_CR6","doi-asserted-by":"crossref","unstructured":"Bersani, M.M., Rossi, M., Pietro, P.S.: A tool for deciding the satisfiability of continuous-time metric temporal logic. In: Temporal Representation and Reasoning (TIME), 2013 20th International Symposium on, pp. 99\u2013106. IEEE (2013)","DOI":"10.1109\/TIME.2013.20"},{"key":"243_CR7","doi-asserted-by":"crossref","unstructured":"Bian, J., French, T., Reynolds, M.: An efficient tableau for linear time temporal logic. In: Cranefield, S., Nayak, A. (eds.) 26th Australasian Joint Conference on Artificial Intelligence, AI 2013, 1\u20136 December 2013, Dunedin, New Zealand, LNCS, vol. 8272, pp. 289\u2013300. Springer, Berlin (2013)","DOI":"10.1007\/978-3-319-03680-9_31"},{"key":"243_CR8","doi-asserted-by":"crossref","unstructured":"Bianculli, D., Spoletini, P., Morzenti, A., Pradella, M., Pietro, P.S.: Model checking temporal metric specifications with Trio2Promela. In: FSEN\u201907, Proceedings of the International Symposium on Fundamentals of Software Engineering (2007)","DOI":"10.1007\/978-3-540-75698-9_26"},{"key":"243_CR9","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. In: FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference, Hyderabad, India, December 15\u201318, 2005, Proceedings, pp. 432\u2013443. Springer, Berlin (2005)","DOI":"10.1007\/11590156_35"},{"key":"243_CR10","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.: On expressiveness and complexity in real-time model checking. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP (2). Lecture Notes in Computer Science, vol. 5126, pp. 124\u2013135. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-70583-3_11"},{"issue":"2","key":"243_CR11","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1305\/ndjfl\/1093870820","volume":"26","author":"JP Burgess","year":"1985","unstructured":"Burgess, J.P., Gurevich, Y.: The decision problem for linear temporal logic. Notre Dame J. Form. Log. 26(2), 115\u2013128 (1985)","journal-title":"Notre Dame J. Form. Log."},{"key":"243_CR12","doi-asserted-by":"crossref","unstructured":"Chaochen, Z.: Duration calculus, a logical approach to real-time systems. In: Haeberer, A.M. (ed.) AMAST. Lecture Notes in Computer Science, vol. 1548, pp. 1\u20137. Springer, Berlin (1998)","DOI":"10.1007\/3-540-49253-4_1"},{"issue":"7","key":"243_CR13","doi-asserted-by":"crossref","first-page":"985","DOI":"10.1109\/5.871305","volume":"88","author":"J Davoren","year":"2000","unstructured":"Davoren, J., Nerode, A.: Logics for hybrid systems. Proc. IEEE 88(7), 985\u20131010 (2000)","journal-title":"Proc. IEEE"},{"issue":"1","key":"243_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10009-005-0214-9","volume":"9","author":"D D\u2019Souza","year":"2007","unstructured":"D\u2019Souza, D., Prabhakar, P.: On the expressiveness of MTL in the pointwise and continuous semantics. STTT 9(1), 1\u20134 (2007)","journal-title":"STTT"},{"key":"243_CR15","doi-asserted-by":"crossref","unstructured":"Falcon, E., Laroche, C., Fauve, S., Coste, C.: Behaviour of one inelastic ball bouncing repeatedly off the ground. Eur. Phys. J. B B(3), 45\u201357 (1998)","DOI":"10.1007\/s100510050283"},{"key":"243_CR16","doi-asserted-by":"crossref","unstructured":"Furia, C.A., Rossi, M.: On the expressiveness of MTL variants over dense time. In: Raskin, J.F., Thiagarajan, P.S. (eds.) FORMATS. Lecture Notes in Computer Science, vol. 4763, pp. 163\u2013178. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-75454-1_13"},{"key":"243_CR17","doi-asserted-by":"crossref","unstructured":"Furia, C.A., Rossi, M.: MTL with bounded variability: decidability and complexity. In: Cassez, F., Jard, C. (eds.) Formal Modeling and Analysis of Timed Systems, 6th International Conference, FORMATS 2008, Saint Malo, France, September 15\u201317, 2008. Proceedings, Lecture Notes in Computer Science, vol. 5215, pp. 109\u2013123. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-85778-5_9"},{"issue":"2","key":"243_CR18","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1093\/logcom\/1.2.229","volume":"1","author":"DM Gabbay","year":"1990","unstructured":"Gabbay, D.M., Hodkinson, I.M.: An axiomatisation of the temporal logic with until and since over the real numbers. J. Log. Comput. 1(2), 229\u2013260 (1990)","journal-title":"J. Log. Comput."},{"key":"243_CR19","doi-asserted-by":"crossref","unstructured":"Gupta, V., Henzinger, T., Jagadeesan, R.: Robust timed automata. In: Proceedings of the International Workshop on Hybrid and Real-Time Systems (HART). LNCS, vol. 1201, pp. 331\u2013345. Springer, Berlin (1997)","DOI":"10.1007\/BFb0014736"},{"key":"243_CR20","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Proceedings of the 19th International Colloquium on Automata. Languages, and Programming (ICALP), LNCS, vol. 623, pp. 545\u2013558. Springer, Berlin (1992)","DOI":"10.1007\/3-540-55719-9_103"},{"key":"243_CR21","doi-asserted-by":"crossref","unstructured":"Hirshfeld, Y., Rabinovich, A.: An expressive temporal logic for real time. MFCS (2006)","DOI":"10.1007\/11821069_43"},{"key":"243_CR22","doi-asserted-by":"crossref","unstructured":"Hirshfeld, Y., Rabinovich, A.: Expressiveness of metric modalities for continuous time. Log. Methods Comput. Sci. 3(1) (2007)","DOI":"10.2168\/LMCS-3(1:3)2007"},{"key":"243_CR23","doi-asserted-by":"crossref","unstructured":"Hirshfeld, Y., Rabinovich, A.M.: A framework for decidable metrical logics. In: Wiedermann, J., van Emde Boas, P., Nielsen, M. (eds.) ICALP. Lecture Notes in Computer Science, vol. 1644, pp. 422\u2013432. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48523-6_39"},{"issue":"1","key":"243_CR24","first-page":"1","volume":"62","author":"Y Hirshfeld","year":"2004","unstructured":"Hirshfeld, Y., Rabinovich, A.M.: Logics for real time: decidability and complexity. Fundam. Inform. 62(1), 1\u201328 (2004)","journal-title":"Fundam. Inform."},{"key":"243_CR25","unstructured":"Huang, J., Voeten, J., Geilen, M.: Real-time property preservation in approximation of timed systems. In: 1st ACM and IEEE International Conference on Formal Methods and Models for Co-Design (2003)"},{"key":"243_CR26","unstructured":"Kamp, H.: Tense Logic and the Theory of Linear Order. Ph.D. thesis, University of California, Los Angeles (1968)"},{"issue":"4","key":"243_CR27","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 Syst. 2(4), 255\u2013299 (1990). doi: 10.1007\/BF01995674","journal-title":"Real-Time Syst."},{"key":"243_CR28","doi-asserted-by":"crossref","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: From MITL to timed automata. In: Asarin, E., Bouyer, P. (eds.) Formal Modeling and Analysis of Timed Systems, 4th International Conference, FORMATS 2006, Paris, France, September 25\u201327, 2006, Proceedings, Lecture Notes in Computer Science, vol. 4202, pp. 274\u2013289. Springer, Berlin (2006). doi: 10.1007\/11867340_20","DOI":"10.1007\/11867340_20"},{"key":"243_CR29","doi-asserted-by":"crossref","unstructured":"Marx, M., Mikulas, S., Reynolds, M.: The mosaic method for temporal logics. In: Dyckhoff, R. (ed.) Automated Reasoning with Analytic Tableaux and Related Methods, Proceedings of International Conference, TABLEAUX 2000, Saint Andrews, Scotland, July 2000, LNAI 1847, pp. 324\u2013340. Springer, Berlin (2000)","DOI":"10.1007\/10722086_26"},{"key":"243_CR30","doi-asserted-by":"crossref","unstructured":"Nickovic, D., Piterman, N.: From mtl to deterministic timed automata. In: Chatterjee, K., Henzinger, T.A. (eds.) Formal Modeling and Analysis of Timed Systems\u20148th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8\u201310, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6246, pp. 152\u2013167. Springer, Berlin (2010). doi: 10.1007\/978-3-642-15297-9_13","DOI":"10.1007\/978-3-642-15297-9_13"},{"key":"243_CR31","volume-title":"Temporal Logic for Real-Time Systems. Advanced Software Development Series","author":"JS Ostroff","year":"1989","unstructured":"Ostroff, J.S.: Temporal Logic for Real-Time Systems. Advanced Software Development Series. Wiley, New York (1989)"},{"key":"243_CR32","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: Proceedings of the 20th Annual Symposium on Logic in Computer Science (LICS\u201905), pp. 188\u2013197. IEEE Comp. Soc. Press (2005)","DOI":"10.1109\/LICS.2005.33"},{"key":"243_CR33","unstructured":"Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: FORMATS \u201908: Proceedings of the 6th international conference on Formal Modeling and Analysis of Timed Systems, pp. 1\u201313. Springer, Berlin (2008). doi: 10.1007\/978-3-540-85778-5-1"},{"key":"243_CR34","doi-asserted-by":"crossref","unstructured":"Rabinovich, A.: Complexity of metric temporal logics with counting and the Pnueli modalities. In: Cassez, F., Jard, C. (eds.) Formal Modeling and Analysis of Timed Systems, 6th International Conference, FORMATS 2008, Saint Malo, France, September 15\u201317, 2008. Proceedings, Lecture Notes in Computer Science, vol. 5215, pp. 93\u2013108. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-85778-5_8"},{"key":"243_CR35","unstructured":"Raskin, J.: Logics, Automata and Classical Theories for Deciding Real Time. Ph.D. thesis. Universit\u00e9 de Namur, Belgium (1999)"},{"key":"243_CR36","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/BF00370112","volume":"51","author":"M Reynolds","year":"1992","unstructured":"Reynolds, M.: An axiomatization for Until and Since over the reals without the IRR rule. Stud. Log. 51, 165\u2013193 (1992)","journal-title":"Stud. Log."},{"key":"243_CR37","doi-asserted-by":"crossref","unstructured":"Reynolds, M.: Dense time reasoning via mosaics. In: TIME \u201909: Proceedings of the 2009 16th International Symposium on Temporal Representation and Reasoning, pp. 3\u201310. IEEE Computer Society, Washington, DC (2009). doi: 10.1109\/TIME.2009.16","DOI":"10.1109\/TIME.2009.16"},{"issue":"8","key":"243_CR38","doi-asserted-by":"crossref","first-page":"1063","DOI":"10.1016\/j.apal.2010.01.002","volume":"161","author":"M Reynolds","year":"2010","unstructured":"Reynolds, M.: The complexity of the temporal logic over the reals. Ann. Pure Appl. Log. 161(8), 1063\u20131096 (2010). doi: 10.1016\/j.apal.2010.01.002","journal-title":"Ann. Pure Appl. Log."},{"key":"243_CR39","doi-asserted-by":"crossref","first-page":"437","DOI":"10.3166\/jancl.20.437-455","volume":"20","author":"M Reynolds","year":"2010","unstructured":"Reynolds, M.: Metric temporal reasoning with less than 2 clocks. J. Appl. Non-class. Log. 20, 437\u2013455 (2010)","journal-title":"J. Appl. Non-class. Log."},{"key":"243_CR40","doi-asserted-by":"crossref","unstructured":"Reynolds, M.: A new metric temporal logic for hybrid systems. In: Sanchez, C., Venables, B., Zimanyi, E. (eds.) Twentieth International Symposium on Temporal Representation and Reasoning, TIME 2013, 26\u201328 September 2013, Pensacola, FL (USA), pp. 73\u201380. IEEE CPS (2013)","DOI":"10.1109\/TIME.2013.17"},{"key":"243_CR41","doi-asserted-by":"crossref","unstructured":"Reynolds, M.: A tableau for general linear temporal logic. J. Log. Comput. (2013)","DOI":"10.1093\/logcom\/exs042"},{"key":"243_CR42","unstructured":"Reynolds, M.: A tableau for temporal logic over the reals. In: Gor\u00e9, R., Kooi, B., Kurucz, A. (eds.) Advances in Modal Logic, vol. 10, pp. 439\u2013458. College Publications (2014)"},{"key":"243_CR43","doi-asserted-by":"crossref","unstructured":"Wilke, T.: Specifying timed state sequences in powerful decidable logics and timed automata (extended abstract). In: LNCS 863, pp. 694\u2013715. Springer, Berlin (1994)","DOI":"10.1007\/3-540-58468-4_191"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0243-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-015-0243-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0243-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,26]],"date-time":"2019-08-26T19:35:03Z","timestamp":1566848103000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-015-0243-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,13]]},"references-count":43,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,4]]}},"alternative-id":["243"],"URL":"https:\/\/doi.org\/10.1007\/s00236-015-0243-0","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,6,13]]}}}