{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:15:04Z","timestamp":1750306504203,"version":"3.41.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2016,2,17]],"date-time":"2016-02-17T00:00:00Z","timestamp":1455667200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2016,7,22]]},"abstract":"<jats:p>\n            Metric temporal logic (MTL) is one of the most prominent specification formalisms for real-time systems. Over infinite timed words, full MTL is undecidable, but satisfiability for a syntactially defined safety fragment, called safety MTL, was proved decidable several years ago. Satisfiability for safety MTL is also known to be equivalent to a fair termination problem for a class of channel machines with insertion errors. However, hitherto, its precise computational complexity has remained elusive, with only a nonelementary lower bound. Via another equivalent problem, namely termination for a class of rational relations, we show that satisfiability for safety MTL is A\n            <jats:sc>ckermann<\/jats:sc>\n            -complete (i.e., among the easiest nonprimitive recursive problems). This is surprising since decidability was originally established using Higman\u2019s Lemma, suggesting a much higher nonmultiply recursive complexity.\n          <\/jats:p>","DOI":"10.1145\/2874774","type":"journal-article","created":{"date-parts":[[2016,2,22]],"date-time":"2016-02-22T13:07:16Z","timestamp":1456146436000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Zeno, Hercules, and the Hydra"],"prefix":"10.1145","volume":"17","author":[{"given":"Ranko","family":"Lazi\u0107","sequence":"first","affiliation":[{"name":"University of Warwick"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[{"name":"University of Oxford"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Worrell","sequence":"additional","affiliation":[{"name":"University of Oxford"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,2,17]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000033962.51898.1a"},{"volume-title":"CONCUR (LNCS)","author":"Abdulla Parosh Aziz","key":"e_1_2_1_2_1","unstructured":"Parosh Aziz Abdulla , Bengt Jonsson , Marcus Nilsson , and Mayank Saksena . 2004b. A survey of regular model checking . In CONCUR (LNCS) , Vol. 3170 . Springer , Berlin, Heidelberg , 35--48. Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, and Mayank Saksena. 2004b. A survey of regular model checking. In CONCUR (LNCS), Vol. 3170. Springer, Berlin, Heidelberg, 35--48."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1992.267774"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0234-7"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.49"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0003"},{"volume-title":"FSTTCS (LNCS)","author":"Chambart Pierre","key":"e_1_2_1_7_1","unstructured":"Pierre Chambart and Philippe Schnoebelen . 2007. Post embedding problem is not primitive recursive, with applications to channel systems . In FSTTCS (LNCS) , Vol. 4855 . Springer , Berlin, Heidelberg , 265--276. Pierre Chambart and Philippe Schnoebelen. 2007. Post embedding problem is not primitive recursive, with applications to channel systems. In FSTTCS (LNCS), Vol. 4855. Springer, Berlin, Heidelberg, 265--276."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.47"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.39"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcta.2000.3154"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(92)90005-G"},{"volume-title":"CONCUR (LNCS)","author":"Henzinger T. A.","key":"e_1_2_1_14_1","unstructured":"T. A. Henzinger . 1998. It\u2019s about time: Real-time logics reviewed . In CONCUR (LNCS) , Vol. 1466 . Springer , Berlin, Heidelberg , 439--454. T. A. Henzinger. 1998. It\u2019s about time: Real-time logics reviewed. In CONCUR (LNCS), Vol. 1466. Springer, Berlin, Heidelberg, 439--454."},{"volume-title":"Synthesis and Alternating Automata over Real Time. D. Phil. thesis","author":"Jenkins Mark","key":"e_1_2_1_15_1","unstructured":"Mark Jenkins . 2012. Synthesis and Alternating Automata over Real Time. D. Phil. thesis . Oxford University . Mark Jenkins. 2012. Synthesis and Alternating Automata over Real Time. D. Phil. thesis. Oxford University."},{"key":"e_1_2_1_16_1","unstructured":"Pierre Jullien. 1969. Contribution \u00c0 L\u2019\u00c9tude Des Types D\u2019Ordres Dispers\u00e9s. Th\u00e8se de doctorat. Universit\u00e9 de Marseille.  Pierre Jullien. 1969. Contribution \u00c0 L\u2019\u00c9tude Des Types D\u2019Ordres Dispers\u00e9s. Th\u00e8se de doctorat. Universit\u00e9 de Marseille."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37075-5_18"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1112\/blms\/14.4.285"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802201"},{"volume-title":"MFCS (LNCS)","author":"Lazi\u0107 Ranko","key":"e_1_2_1_20_1","unstructured":"Ranko Lazi\u0107 , Jo\u00ebl Ouaknine , and James Worrell . 2013. Zeno , Hercules and the Hydra: Downward rational termination is Ackermannian . In MFCS (LNCS) , Vol. 8087 . Springer , Berlin , 643--654. Ranko Lazi\u0107, Jo\u00ebl Ouaknine, and James Worrell. 2013. Zeno, Hercules and the Hydra: Downward rational termination is Ackermannian. In MFCS (LNCS), Vol. 8087. Springer, Berlin, 643--654."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.16"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01967649"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11690634_15"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_27"},{"key":"e_1_2_1_25_1","volume-title":"Article 8","author":"Ouaknine Jo\u00ebl","year":"2007","unstructured":"Jo\u00ebl Ouaknine and James Worrell . 2007. On the decidability of metric temporal logic over finite words. Log. Meth. Comput. Sci. 3, 1 , Article 8 ( 2007 ), 27 pages. Jo\u00ebl Ouaknine and James Worrell. 2007. On the decidability of metric temporal logic over finite words. Log. Meth. Comput. Sci. 3, 1, Article 8 (2007), 27 pages."},{"volume-title":"Elements of Automata Theory","author":"Sakarovitch Jacques","key":"e_1_2_1_26_1","unstructured":"Jacques Sakarovitch . 2009. Elements of Automata Theory . Cambridge University Press , UK. I--XXIV, 1--758&nbsp;pages. Jacques Sakarovitch. 2009. Elements of Automata Theory. Cambridge University Press, UK. I--XXIV, 1--758&nbsp;pages."},{"key":"e_1_2_1_27_1","unstructured":"Sylvain Schmitz. 2012. Scientific Report - ESF Short Visit to Oxford University. (2012).  Sylvain Schmitz. 2012. Scientific Report - ESF Short Visit to Oxford University. (2012)."},{"volume-title":"MFCS (LNCS)","author":"Schnoebelen Philippe","key":"e_1_2_1_29_1","unstructured":"Philippe Schnoebelen . 2010. Revisiting Ackermann-hardness for lossy counter machines and reset petri nets . In MFCS (LNCS) , Vol. 6281 . Springer , Berlin , 616--628. Philippe Schnoebelen. 2010. Revisiting Ackermann-hardness for lossy counter machines and reset petri nets. In MFCS (LNCS), Vol. 6281. Springer, Berlin, 616--628."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2874774","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2874774","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:54Z","timestamp":1750225734000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2874774"}},"subtitle":["Safety Metric Temporal Logic is A\n            <scp>ckermann<\/scp>\n            -Complete"],"short-title":[],"issued":{"date-parts":[[2016,2,17]]},"references-count":27,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,7,22]]}},"alternative-id":["10.1145\/2874774"],"URL":"https:\/\/doi.org\/10.1145\/2874774","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2016,2,17]]},"assertion":[{"value":"2015-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-02-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}