{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:11:43Z","timestamp":1773655903908,"version":"3.50.1"},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2008,3,1]],"date-time":"2008-03-01T00:00:00Z","timestamp":1204329600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Polish government","award":["N206 008 32\/0810"],"award-info":[{"award-number":["N206 008 32\/0810"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2008,3]]},"abstract":"<jats:p>A notion of alternating timed automata is proposed. It is shown that such automata with only one clock have decidable emptiness problem over finite words. This gives a new class of timed languages that is closed under boolean operations and which has an effective presentation. We prove that the complexity of the emptiness problem for alternating timed automata with one clock is nonprimitive recursive. The proof gives also the same lower bound for the universality problem for nondeterministic timed automata with one clock. We investigate extension of the model with epsilon-transitions and prove that emptiness is undecidable. Over infinite words, we show undecidability of the universality problem.<\/jats:p>","DOI":"10.1145\/1342991.1342994","type":"journal-article","created":{"date-parts":[[2008,4,8]],"date-time":"2008-04-08T15:40:00Z","timestamp":1207669200000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["Alternating timed automata"],"prefix":"10.1145","volume":"9","author":[{"given":"Slawomir","family":"Lasota","sequence":"first","affiliation":[{"name":"Institute of Informatics, Warsaw University, Banacha, Warszawa"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Igor","family":"Walukiewicz","sequence":"additional","affiliation":[{"name":"LaBRI, Universit\u00e9 Bordeaux-1, Talence cedex, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,4,7]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the International Conference Tools and Algorithms for the Construction and Analysis of System (TACAS'98)","author":"Abdulla P.","unstructured":"Abdulla , P. and Jonsson , B . 1998. Veryfying networks of timed processes . In Proceedings of the International Conference Tools and Algorithms for the Construction and Analysis of System (TACAS'98) . Lecture Notes in Computer Science. Springer-Verlag, New York, 298--312. Abdulla, P. and Jonsson, B. 1998. Veryfying networks of timed processes. In Proceedings of the International Conference Tools and Algorithms for the Construction and Analysis of System (TACAS'98). Lecture Notes in Computer Science. Springer-Verlag, New York, 298--312."},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the ICATPN'01","author":"Abdulla P.","unstructured":"Abdulla , P. and Jonsson , B . 2001. Timed petri nets and BQOs . In Proceedings of the ICATPN'01 . 53--70. Abdulla, P. and Jonsson, B. 2001. Timed petri nets and BQOs. In Proceedings of the ICATPN'01. 53--70."},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the IEEE Symposium on Logic in Computer Science (LICS'96)","author":"Abdulla P.","unstructured":"Abdulla , P. , \u010cer &abar;ns, K., Jonsson , B. , and Tsay , Y . 1996. General decidability theorems for infinite state systems . In Proceedings of the IEEE Symposium on Logic in Computer Science (LICS'96) . IEEE Computer Society Press, Los Alamitos, CA, 313--323. Abdulla, P., \u010cer&abar;ns, K., Jonsson, B., and Tsay, Y. 1996. General decidability theorems for infinite state systems. In Proceedings of the IEEE Symposium on Logic in Computer Science (LICS'96). IEEE Computer Society Press, Los Alamitos, CA, 313--323."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_88"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science","volume":"3124","author":"Alur R.","unstructured":"Alur , R. , Bernadsky , M. , and Madhusudan , P . 2004. Optimal reachability for weighted timed games . In Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science , vol. 3124 . Springer-Verlag, New York, 122--133. Alur, R., Bernadsky, M., and Madhusudan, P. 2004. Optimal reachability for weighted timed games. In Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science, vol. 3124. Springer-Verlag, New York, 122--133."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00173-4"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/167088.167242"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the IFAC Symposium on System Structure and Control. 469--474","author":"Asarin E.","unstructured":"Asarin , E. , Maler , O. , Pnueli , A. , , and Sifakis , J . 1998. Controller synthesis for timed automata . In Proceedings of the IFAC Symposium on System Structure and Control. 469--474 . Asarin, E., Maler, O., Pnueli, A., , and Sifakis, J. 1998. Controller synthesis for timed automata. In Proceedings of the IFAC Symposium on System Structure and Control. 469--474."},{"key":"e_1_2_1_10_1","first-page":"145","article-title":"Characterization of the expressive power of silent transitions in timed automata","volume":"36","author":"B\u00e9rard B.","year":"1998","unstructured":"B\u00e9rard , B. , Diekert , V. , Gastin , P. , and Petit , A. 1998 . Characterization of the expressive power of silent transitions in timed automata . Fund. Inf. 36 , 2, 145 -- 182 . B\u00e9rard, B., Diekert, V., Gastin, P., and Petit, A. 1998. Characterization of the expressive power of silent transitions in timed automata. Fund. Inf. 36, 2, 145--182.","journal-title":"Fund. Inf."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_13"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Bouyer P. D'Souza D. Madhusudan P. and \n      Petit A\n  . \n  2003\n  . Timed control with partial observability. In Proceedings of the CAV'03 Lecture Notes in Computer Science vol. \n  2725\n  . \n  Springer-Verlag 180--192.  Bouyer P. D'Souza D. Madhusudan P. and Petit A. 2003. Timed control with partial observability. In Proceedings of the CAV'03 Lecture Notes in Computer Science vol. 2725. Springer-Verlag 180--192.","DOI":"10.1007\/978-3-540-45069-6_18"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/322374.322380"},{"key":"e_1_2_1_14_1","volume-title":"-F","author":"Cassez F.","year":"2002","unstructured":"Cassez , F. , Henzinger , T. A. , and Raskin , J . -F . 2002 . A comparison of control problems for timed and hybrid systems. In Proceedings of the Hybrid Systems Computation and Control (HSCC '02). 134--148. Cassez, F., Henzinger, T. A., and Raskin, J.-F. 2002. A comparison of control problems for timed and hybrid systems. In Proceedings of the Hybrid Systems Computation and Control (HSCC'02). 134--148."},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the International Colloquium on Automata, Language and Programming (ICALP'99)","volume":"1644","author":"Dickh\u00f6fer M.","unstructured":"Dickh\u00f6fer , M. and Wilke , T . 1999. Timed alternating tree automata: the automata-theoretic solution to the TCTL model checking problem . In Proceedings of the International Colloquium on Automata, Language and Programming (ICALP'99) . Lecture Notes in Computer Science , vol. 1644 . Springer-Verlag, New York, 281--290. Dickh\u00f6fer, M. and Wilke, T. 1999. Timed alternating tree automata: the automata-theoretic solution to the TCTL model checking problem. In Proceedings of the International Colloquium on Automata, Language and Programming (ICALP'99). Lecture Notes in Computer Science, vol. 1644. Springer-Verlag, New York, 281--290."},{"key":"e_1_2_1_16_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the STACS'00","author":"Dima C.","unstructured":"Dima , C. 2000. Real-time automata and the Kleene algebra of sets of real numbers . In Proceedings of the STACS'00 . Lecture Notes in Computer Science , vol. 1170 . Springer-Verlag , New York , 279--289. Dima, C. 2000. Real-time automata and the Kleene algebra of sets of real numbers. In Proceedings of the STACS'00. Lecture Notes in Computer Science, vol. 1170. Springer-Verlag, New York, 279--289."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-2.1.326"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the CONCUR'04","volume":"3170","author":"Laroussinie F.","unstructured":"Laroussinie , F. , Markey , N. , and Schnoebelen , P . 2004. Model checking timed automata with one or two clocks . In Proceedings of the CONCUR'04 . Lecture Notes in Computer Science , vol. 3170 . Springer-Verlag, New York, 387--401. Laroussinie, F., Markey, N., and Schnoebelen, P. 2004. Model checking timed automata with one or two clocks. In Proceedings of the CONCUR'04. Lecture Notes in Computer Science, vol. 3170. Springer-Verlag, New York, 387--401."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021842"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.33"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(01)00337-4"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002360100067"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1342991.1342994","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1342991.1342994","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:39:03Z","timestamp":1750253943000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1342991.1342994"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,3]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2008,3]]}},"alternative-id":["10.1145\/1342991.1342994"],"URL":"https:\/\/doi.org\/10.1145\/1342991.1342994","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,3]]},"assertion":[{"value":"2005-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2006-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-04-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}