{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T19:51:42Z","timestamp":1777578702243,"version":"3.51.4"},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2020,3,3]],"date-time":"2020-03-03T00:00:00Z","timestamp":1583193600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Infosys Foundation, India, Tata Consultancy Services, India, and the MATRICS project of the Science and Education Research Board, India"},{"name":"CNRS, Inria, and DST"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2020,7,31]]},"abstract":"<jats:p>\n            The\n            <jats:italic>reachability problem<\/jats:italic>\n            for timed automata asks if a given automaton has a run leading to an accepting state, and the\n            <jats:italic>liveness problem<\/jats:italic>\n            asks if the automaton has an infinite run that visits accepting states infinitely often. Both of these problems are known to be P\n            <jats:sc>space<\/jats:sc>\n            -complete.\n          <\/jats:p>\n          <jats:p>\n            We show that if P \u2260P\n            <jats:sc>space<\/jats:sc>\n            , the liveness problem is more difficult than the reachability problem; in other words, we exhibit a family of automata for which solving the reachability problem with the standard algorithm is in P but solving the liveness problem is P\n            <jats:sc>space<\/jats:sc>\n            -hard. This leads us to revisit the algorithmics for the liveness problem. We propose a notion of a witness for the fact that a timed automaton violates a liveness property. We give an algorithm for computing such a witness and compare it to existing solutions.\n          <\/jats:p>","DOI":"10.1145\/3372310","type":"journal-article","created":{"date-parts":[[2020,3,3]],"date-time":"2020-03-03T10:21:42Z","timestamp":1583230902000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Why Liveness for Timed Automata Is Hard, and What We Can Do About It"],"prefix":"10.1145","volume":"21","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Herbreteau","sequence":"first","affiliation":[{"name":"Universit\u00e9 de Bordeaux and UMI 2000 ReLaX"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2666-0691","authenticated-orcid":false,"given":"B.","family":"Srivathsan","sequence":"additional","affiliation":[{"name":"Chennai Mathematical Institute and UMI 2000 ReLaX"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thanh-Tung","family":"Tran","sequence":"additional","affiliation":[{"name":"International University--Vietnam National University, Viet Nam"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Igor","family":"Walukiewicz","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Bordeaux and UMI 2000 ReLaX"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,3,3]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 254--270","author":"Behrmann G.","unstructured":"G. Behrmann , P. Bouyer , E. Fleury , and K. G. Larsen . 2003. Static guard analysis in timed automata verification . In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 254--270 . G. Behrmann, P. Bouyer, E. Fleury, and K. G. Larsen. 2003. Static guard analysis in timed automata verification. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 254--270."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220880.3220966"},{"key":"e_1_2_1_4_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science","volume":"1384","author":"Daws C.","unstructured":"C. Daws and S. Tripakis . 1998. Model checking of real-time reachability properties using abstractions . In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science , Vol. 1384 . Springer, 313--329. C. Daws and S. Tripakis. 1998. Model checking of real-time reachability properties using abstractions. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, Vol. 1384. Springer, 313--329."},{"key":"e_1_2_1_5_1","series-title":"Lecture Notes in Computer Science","volume-title":"Automatic Verification Methods for Finite State Systems","author":"Dill D. L.","unstructured":"D. L. Dill . 1989. Timing assumptions and verification of finite-state concurrent systems . In Automatic Verification Methods for Finite State Systems . Lecture Notes in Computer Science , Vol. 407 . Springer , 197--212. D. L. Dill. 1989. Timing assumptions and verification of finite-state concurrent systems. In Automatic Verification Methods for Finite State Systems. Lecture Notes in Computer Science, Vol. 407. Springer, 197--212."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(1:6)2013"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Article 48","author":"Herbreteau F.","unstructured":"F. Herbreteau , B. Srivathsan , T.-T. Tran , and I. Walukiewicz . 2016. Why liveness for timed automata is hard, and what we can do about it . In Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Article 48 , 14 pages. F. Herbreteau, B. Srivathsan, T.-T. Tran, and I. Walukiewicz. 2016. Why liveness for timed automata is hard, and what we can do about it. In Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Article 48, 14 pages."},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 2012 27th Annual IEEE\/ACM Symposium on Logic in Computer Science (LICS\u201912)","author":"Herbreteau F.","unstructured":"F. Herbreteau , B. Srivathsan , and I. Walukiewicz . 2012. Better abstractions for timed automata . In Proceedings of the 2012 27th Annual IEEE\/ACM Symposium on Logic in Computer Science (LICS\u201912) . IEEE, Los Alamitos, CA, 375--384. F. Herbreteau, B. Srivathsan, and I. Walukiewicz. 2012. Better abstractions for timed automata. In Proceedings of the 2012 27th Annual IEEE\/ACM Symposium on Logic in Computer Science (LICS\u201912). IEEE, Los Alamitos, CA, 375--384."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0133-1"},{"key":"e_1_2_1_10_1","volume-title":"Computer Aided Verification. Lecture Notes in Computer Science","volume":"8044","author":"Herbreteau F.","unstructured":"F. Herbreteau , B. Srivathsan , and I. Walukiewicz . 2013. Lazy abstractions for timed automata . In Computer Aided Verification. Lecture Notes in Computer Science , Vol. 8044 . Springer, 990--1005. F. Herbreteau, B. Srivathsan, and I. Walukiewicz. 2013. Lazy abstractions for timed automata. In Computer Aided Verification. Lecture Notes in Computer Science, Vol. 8044. Springer, 990--1005."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.07.004"},{"key":"e_1_2_1_12_1","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"Herbreteau F.","unstructured":"F. Herbreteau and T.-T. Tran . 2015. Improving search order for reachability testing in timed automata . In Formal Modeling and Analysis of Timed Systems . Lecture Notes in Computer Science , Vol. 9268 . Springer , 124--139. F. Herbreteau and T.-T. Tran. 2015. Improving search order for reachability testing in timed automata. In Formal Modeling and Analysis of Timed Systems. Lecture Notes in Computer Science, Vol. 9268. Springer, 124--139."},{"key":"e_1_2_1_13_1","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"Laarman A.","unstructured":"A. Laarman , M. C. Olesen , A. E. Dalsgaard , K. G. Larsen , and J. van de Pol . 2013. Multi-core emptiness checking of timed B\u00fcchi automata using inclusion abstraction . In Computer Aided Verification . Lecture Notes in Computer Science , Vol. 8044 . Springer , 968--983. A. Laarman, M. C. Olesen, A. E. Dalsgaard, K. G. Larsen, and J. van de Pol. 2013. Multi-core emptiness checking of timed B\u00fcchi automata using inclusion abstraction. In Computer Aided Verification. Lecture Notes in Computer Science, Vol. 8044. Springer, 968--983."},{"key":"e_1_2_1_14_1","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"G. Li.","unstructured":"G. Li. 2009. Checking timed B\u00fcchi automata emptiness using LU-abstractions . In Formal Modeling and Analysis of Timed Systems . Lecture Notes in Computer Science , Vol. 5813 . Springer , 228--242. G. Li. 2009. Checking timed B\u00fcchi automata emptiness using LU-abstractions. In Formal Modeling and Analysis of Timed Systems. Lecture Notes in Computer Science, Vol. 5813. Springer, 228--242."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1507244.1507245"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008734703554"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1632-8"},{"key":"e_1_2_1_18_1","unstructured":"UPPAAL [n.d.]. UPPAAL CSMA\/CD Model. Retrieved October 8 2014 from https:\/\/www.it.uu.se\/research\/group\/darts\/uppaal\/benchmarks\/genCSMA_CD.awk.  UPPAAL [n.d.]. UPPAAL CSMA\/CD Model. Retrieved October 8 2014 from https:\/\/www.it.uu.se\/research\/group\/darts\/uppaal\/benchmarks\/genCSMA_CD.awk."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372310","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372310","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:20Z","timestamp":1750197740000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372310"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,3,3]]},"references-count":18,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,7,31]]}},"alternative-id":["10.1145\/3372310"],"URL":"https:\/\/doi.org\/10.1145\/3372310","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,3,3]]},"assertion":[{"value":"2018-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-03-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}