{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T01:47:29Z","timestamp":1768009649579,"version":"3.49.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2022,7,1]],"date-time":"2022-07-01T00:00:00Z","timestamp":1656633600000},"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 SIGLOG News"],"published-print":{"date-parts":[[2022,7]]},"abstract":"<jats:p>\n            Given a timed automaton\n            <jats:italic>A<\/jats:italic>\n            and a control state\n            <jats:italic>q<\/jats:italic>\n            , does there exist a run of\n            <jats:italic>A<\/jats:italic>\n            that visits\n            <jats:italic>q<\/jats:italic>\n            ? This problem of control state reachability in timed automata was posed in [Alur and Dill 1994] and is known to be PSPACE-complete. One does not hope to have efficient algorithms for this problem, in theory. Nevertheless, research in this subject over the last three decades has led to industry-strength award-winning tools implementing this problem. This topic continues to be an active area of research even now. In this article, we present one successful algorithmic framework for attacking this problem.\n          <\/jats:p>","DOI":"10.1145\/3559736.3559738","type":"journal-article","created":{"date-parts":[[2022,8,25]],"date-time":"2022-08-25T22:32:53Z","timestamp":1661466773000},"page":"6-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Reachability in timed automata"],"prefix":"10.1145","volume":"9","author":[{"given":"B","family":"Srivathsan","sequence":"first","affiliation":[{"name":"Chennai Mathematical Institute, India"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,8,25]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.11.018"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of CONCUR'22","author":"Akshay S.","unstructured":"S. Akshay , Paul Gastin , R. Govind , and B. Srivathsan . 2022. Simulations for Event-Clock Automata . In Proceedings of CONCUR'22 , the 33rd International Conference on Concurrency Theory (LIPIcs). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Warsaw, Poland, To appear. S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan. 2022. Simulations for Event-Clock Automata. In Proceedings of CONCUR'22, the 33rd International Conference on Concurrency Theory (LIPIcs). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Warsaw, Poland, To appear."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8\\_30"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/167088.167242"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1059"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8\\_26"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36135-9\\_16"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24310-3\\_13"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X\\_18"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2\\_25"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-005-0190-0"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3\\_14"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6\\_30"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055643"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/b98282"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36494-3\\_54"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000026093.21513.31"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4\\_28"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-17(1:21)2021"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452\\_9"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00709157"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050028"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0020947"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054180"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52148-8\\_17"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2010.36"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2\\_21"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.12.004"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2018.28"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4\\_3"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2020.47"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2019.16"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of LICS'22","author":"Govind R.","year":"2022","unstructured":"R. Govind , Fr\u00e9d\u00e9ric Herbreteau , B. Srivathsan , and Igor Walukiewicz . 2022 . Abstrations for the local-time semantics of timed automata: a foundation for partial-order methods . In Proceedings of LICS'22 , the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science. Haifa, Israel. To appear. R. Govind, Fr\u00e9d\u00e9ric Herbreteau, B. Srivathsan, and Igor Walukiewicz. 2022. Abstrations for the local-time semantics of timed automata: a foundation for partial-order methods. In Proceedings of LICS'22, the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science. Haifa, Israel. To appear."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9\\_26"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2011.78"},{"key":"e_1_2_1_38_1","unstructured":"F. Herbreteau and G. Point. 2019. The TChecker tool and librairies. https:\/\/github.com\/ticktac-project\/tchecker. (2019).  F. Herbreteau and G. Point. 2019. The TChecker tool and librairies. https:\/\/github.com\/ticktac-project\/tchecker. (2019)."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372310"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.48"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8\\_71"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.07.004"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0\\_61"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1\\_53"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_25"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59152-6\\_10"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60385-9"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80671-6"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45739-9\\_15"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0177-x"},{"key":"e_1_2_1_53_1","unstructured":"G\u00e9rald Point. 2022a. TChecker online demonstration. https:\/\/tchecker.labri.fr\/. (2022).  G\u00e9rald Point. 2022a. TChecker online demonstration. https:\/\/tchecker.labri.fr\/. (2022)."},{"key":"e_1_2_1_54_1","unstructured":"G\u00e9rald Point. 2022b. UPPAAL-To-TChecker: a tool to translate UPPAAL models into TChecker models. https:\/\/github.com\/ticktac-project\/uppaal-to-tchecker. (2022).  G\u00e9rald Point. 2022b. UPPAAL-To-TChecker: a tool to translate UPPAAL models into TChecker models. https:\/\/github.com\/ticktac-project\/uppaal-to-tchecker. (2022)."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4\\_2"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4\\_59"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102257"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008734703554"},{"key":"e_1_2_1_59_1","volume-title":"Proceedings of FORTE'01","volume":"197","author":"Wang Farn","year":"2001","unstructured":"Farn Wang . 2001 . Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram . In Proceedings of FORTE'01 , IFIP TC6\/WG6.1 - 21st International Conference on Formal Techniques for Networked and Distributed Systems (IFIP Conference Proceedings), Myungchul Kim, Byoungmoon Chin, Sungwon Kang, and Danhyung Lee (Eds.) , Vol. 197 . Kluwer, Cheju Island, Korea, 235--250. Farn Wang. 2001. Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram. In Proceedings of FORTE'01, IFIP TC6\/WG6.1 - 21st International Conference on Formal Techniques for Networked and Distributed Systems (IFIP Conference Proceedings), Myungchul Kim, Byoungmoon Chin, Sungwon Kang, and Danhyung Lee (Eds.), Vol. 197. Kluwer, Cheju Island, Korea, 235--250."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISoLA.2006.68"},{"key":"e_1_2_1_61_1","volume-title":"A quadratic-time DBM-based successor algorithm for checking timed automata. Information processing letters 96, 3","author":"Zhao Jianhua","year":"2005","unstructured":"Jianhua Zhao , Xuandong Li , and Guoliang Zheng . 2005. A quadratic-time DBM-based successor algorithm for checking timed automata. Information processing letters 96, 3 ( 2005 ), 101--105. Jianhua Zhao, Xuandong Li, and Guoliang Zheng. 2005. A quadratic-time DBM-based successor algorithm for checking timed automata. Information processing letters 96, 3 (2005), 101--105."}],"container-title":["ACM SIGLOG News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3559736.3559738","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3559736.3559738","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:07:57Z","timestamp":1750183677000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3559736.3559738"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7]]},"references-count":60,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,7]]}},"alternative-id":["10.1145\/3559736.3559738"],"URL":"https:\/\/doi.org\/10.1145\/3559736.3559738","relation":{},"ISSN":["2372-3491"],"issn-type":[{"value":"2372-3491","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,7]]},"assertion":[{"value":"2022-08-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}