{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,20]],"date-time":"2026-09-20T04:10:19Z","timestamp":1789877419365,"version":"4.0.1"},"reference-count":19,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["GR\/S52759\/01"],"award-info":[{"award-number":["GR\/S52759\/01"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2011,1]]},"abstract":"<jats:p>A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. Safety one-way alternating automata with one register on infinite data words are considered, their nonemptiness is shown to be ExpSpace-complete, and their inclusion decidable but not primitive recursive. The same complexity bounds are obtained for satisfiability and refinement, respectively, for the safety fragment of linear temporal logic with freeze quantification. Dropping the safety restriction, adding past temporal operators, or adding one more register, each causes undecidability.<\/jats:p>","DOI":"10.1145\/1877714.1877716","type":"journal-article","created":{"date-parts":[[2011,1,25]],"date-time":"2011-01-25T19:12:52Z","timestamp":1295982772000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Safety alternating automata on data words"],"prefix":"10.1145","volume":"12","author":[{"given":"Ranko","family":"Lazi\u0107","sequence":"first","affiliation":[{"name":"University of Warwick, Coventry, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2011,1,27]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01782772"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/2391495.2391506"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1142351.1142354"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.51"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science (STACS). IBFI","author":"Bouyer P.","unstructured":"Bouyer , P. , Markey , N. , Ouaknine , J. , Schnoebelen , P. , and Worrell , J . 2008. On termination for faulty channel machines . In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science (STACS). IBFI , Schloss Dagstuhl, Germany, 121--132. Bouyer, P., Markey, N., Ouaknine, J., Schnoebelen, P., and Worrell, J. 2008. On termination for faulty channel machines. In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science (STACS). IBFI, Schloss Dagstuhl, Germany, 121--132."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90069-9"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1507244.1507246"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.2307\/2370405"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.11"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90242-9"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11944836_35"},{"key":"e_1_2_1_13_1","volume-title":"The reachability problem requires exponential space. Tech. rep. 62","author":"Lipton R. J.","unstructured":"Lipton , R. J. 1976. The reachability problem requires exponential space. Tech. rep. 62 , Yale University . Lipton, R. J. 1976. The reachability problem requires exponential space. Tech. rep. 62, Yale University."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/647318.723471"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/16046.16075"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1013560.1013562"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_27"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00105-X"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_3"},{"key":"e_1_2_1_20_1","series-title":"Lecture Notes in Computer Science","volume-title":"Banff Higher Order Works","author":"Vardi M. Y.","unstructured":"Vardi , M. Y. 1996. An automata-theoretic approach to linear temporal logic . In Banff Higher Order Works . Lecture Notes in Computer Science , vol. 1043 , Springer , 238--266. Vardi, M. Y. 1996. An automata-theoretic approach to linear temporal logic. In Banff Higher Order Works. Lecture Notes in Computer Science, vol. 1043, Springer, 238--266."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1877714.1877716","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1877714.1877716","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:17:36Z","timestamp":1750249056000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1877714.1877716"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1]]},"references-count":19,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["10.1145\/1877714.1877716"],"URL":"https:\/\/doi.org\/10.1145\/1877714.1877716","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,1]]},"assertion":[{"value":"2008-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-01-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}