{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T14:40:51Z","timestamp":1770734451597,"version":"3.49.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2012,2,1]],"date-time":"2012-02-01T00:00:00Z","timestamp":1328054400000},"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":["J. ACM"],"published-print":{"date-parts":[[2012,2]]},"abstract":"<jats:p>Probabilistic \u03c9-automata are variants of nondeterministic automata over infinite words where all choices are resolved by probabilistic distributions. Acceptance of a run for an infinite input word can be defined using traditional acceptance criteria for \u03c9-automata, such as B\u00fcchi, Rabin or Streett conditions. The accepted language of a probabilistic \u03c9-automata is then defined by imposing a constraint on the probability measure of the accepting runs. In this paper, we study a series of fundamental properties of probabilistic \u03c9-automata with three different language-semantics: (1) the probable semantics that requires positive acceptance probability, (2) the almost-sure semantics that requires acceptance with probability 1, and (3) the threshold semantics that relies on an additional parameter \u03bb \u2208 ]0,1[ that specifies a lower probability bound for the acceptance probability. We provide a comparison of probabilistic \u03c9-automata under these three semantics and nondeterministic \u03c9-automata concerning expressiveness and efficiency. Furthermore, we address closure properties under the Boolean operators union, intersection and complementation and algorithmic aspects, such as checking emptiness or language containment.<\/jats:p>","DOI":"10.1145\/2108242.2108243","type":"journal-article","created":{"date-parts":[[2012,2,28]],"date-time":"2012-02-28T12:58:35Z","timestamp":1330433915000},"page":"1-52","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":45,"title":["Probabilistic \u03c9-automata"],"prefix":"10.1145","volume":"59","author":[{"given":"Christel","family":"Baier","sequence":"first","affiliation":[{"name":"Technische Universit\u00e4t Dresden, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcus","family":"Gr\u00f6sser","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Dresden, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nathalie","family":"Bertrand","sequence":"additional","affiliation":[{"name":"INRIA Rennes Bretagne Atlantique, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,3,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/225058.225161"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/646339.686404"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2010.11"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792803.1792824"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.41"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.31"},{"key":"e_1_2_1_7_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 15th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'95)","author":"Bianco A.","unstructured":"Bianco , A. and de Alfaro , L. 1995. Model checking of probabilistic and non-deterministic systems . In Proceedings of the 15th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'95) . Lecture Notes in Computer Science , vol. 1026 , Springer , 499--513. Bianco, A. and de Alfaro, L. 1995. Model checking of probabilistic and non-deterministic systems. In Proceedings of the 15th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'95). Lecture Notes in Computer Science, vol. 1026, Springer, 499--513."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-003-1061-2"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00158-1"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1552285.1552287"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_16"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946284.1946293"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_16"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1885577.1885601"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_19"},{"key":"e_1_2_1_16_1","first-page":"3","article-title":"Algorithms for omega-regular games with imperfect information","volume":"3","author":"Chatterjee K.","year":"2007","unstructured":"Chatterjee , K. , Doyen , L. , Henzinger , T. A. , and Raskin , J.-F. 2007 . Algorithms for omega-regular games with imperfect information . Log. Meth. Comput. Sci. 3 , 3 . Chatterjee, K., Doyen, L., Henzinger, T. A., and Raskin, J.-F. 2007. Algorithms for omega-regular games with imperfect information. Log. Meth. Comput. Sci. 3, 3.","journal-title":"Log. Meth. Comput. Sci."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1927331.1927333"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.06.006"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.07.033"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-0013-1_13"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/210332.210339"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/646733.701309"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 2nd International Workshop on Probabilistic Methods in Verification (ProbMiV'99)","author":"de Alfaro L.","year":"1999","unstructured":"de Alfaro , L. 1999 . The verification of probabilistic systems under memoryless partial-information policies is hard . In Proceedings of the 2nd International Workshop on Probabilistic Methods in Verification (ProbMiV'99) . 19--32. de Alfaro, L. 1999. The verification of probabilistic systems under memoryless partial-information policies is hard. In Proceedings of the 2nd International Workshop on Probabilistic Methods in Verification (ProbMiV'99). 19--32."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1137\/0219069"},{"key":"e_1_2_1_26_1","volume-title":"An Introduction to Probability Theory and Its Applications","author":"Feller W.","unstructured":"Feller , W. 1950. An Introduction to Probability Theory and Its Applications . Wiley , New York . Feller, W. 1950. An Introduction to Probability Theory and Its Applications. Wiley, New York."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/645715.665145"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1880999.1881057"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1779879.1779893"},{"key":"e_1_2_1_30_1","volume-title":"Eds","author":"Gr\u00e4del E.","year":"2002","unstructured":"Gr\u00e4del , E. , Thomas , W. , and Wilke , T. , Eds . 2002 . Automata, Logics , and Infinite Games: A Guide to Current Research. Lecture Notes in Computer Science, vol. 2500 , Springer . Gr\u00e4del, E., Thomas, W., and Wilke, T., Eds. 2002. Automata, Logics, and Infinite Games: A Guide to Current Research. Lecture Notes in Computer Science, vol. 2500, Springer."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02930-1_17"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2166.357214"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/647615.731417"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02055574"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(02)00378-8"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1287\/mnsc.28.1.1"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1287\/moor.12.3.441"},{"key":"e_1_2_1_40_1","first-page":"26","article-title":"Some aspects of probabilistic automata","volume":"9","author":"Paz A.","year":"1966","unstructured":"Paz , A. 1966 . Some aspects of probabilistic automata . Inf. Comput. 9 , 1, 26 -- 60 . Paz, A. 1966. Some aspects of probabilistic automata. Inf. Comput. 9, 1, 26--60.","journal-title":"Inf. Comput."},{"key":"e_1_2_1_41_1","volume-title":"Introduction to Probabilistic Automata","author":"Paz A.","unstructured":"Paz , A. 1971. Introduction to Probabilistic Automata . Academic Press . Paz, A. 1971. Introduction to Probabilistic Automata. Academic Press."},{"key":"e_1_2_1_42_1","volume-title":"-E","author":"Perrin D.","year":"2004","unstructured":"Perrin , D. and Pin , J . -E . 2004 . Infinite Words : Automata, Semigroups, Logic and Games. Pure and Applied Mathematics, vol. 141 , Elsevier . Perrin, D. and Pin, J.-E. 2004. Infinite Words: Automata, Semigroups, Logic and Games. Pure and Applied Mathematics, vol. 141, Elsevier."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1012"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(63)90290-0"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90034-5"},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of the Symposium on 50 Years Jubilee of Mathematics Faculty, Timisoara. Analele Universitatii din Timisoara, seria Matematica-Informatica","volume":"37","author":"Reisz R. D.","year":"1999","unstructured":"Reisz , R. D. 1999 a. A characterization theorem for probabilistic automata over infinite words . In Proceedings of the Symposium on 50 Years Jubilee of Mathematics Faculty, Timisoara. Analele Universitatii din Timisoara, seria Matematica-Informatica , vol. 37 , 156--168. Reisz, R. D. 1999a. A characterization theorem for probabilistic automata over infinite words. In Proceedings of the Symposium on 50 Years Jubilee of Mathematics Faculty, Timisoara. Analele Universitatii din Timisoara, seria Matematica-Informatica, vol. 37, 156--168."},{"key":"e_1_2_1_47_1","first-page":"427","article-title":"Decomposition theorems for probabilistic automata over infinite objects","volume":"10","author":"Reisz R. D.","year":"1999","unstructured":"Reisz , R. D. 1999 b. Decomposition theorems for probabilistic automata over infinite objects . Informatica, Lithuanian Acad. Sci. 10 , 4, 427 -- 440 . Reisz, R. D. 1999b. Decomposition theorems for probabilistic automata over infinite objects. Informatica, Lithuanian Acad. Sci. 10, 4, 427--440.","journal-title":"Informatica, Lithuanian Acad. Sci."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/16046.16081"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1988.21948"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/73007.73019"},{"key":"e_1_2_1_53_1","volume-title":"Handbook of Theoretical Computer Science.","author":"Thomas W.","unstructured":"Thomas , W. 1990. Automata on infinite objects . In Handbook of Theoretical Computer Science. Vol. B: Formal Models and Semantics. Elsevier Science, 133-- 191 . Thomas, W. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science. Vol. B: Formal Models and Semantics. Elsevier Science, 133--191."},{"key":"e_1_2_1_54_1","series-title":"Handbook of Formal Languages.","volume-title":"Beyond Words","author":"Thomas W.","unstructured":"Thomas , W. 1997. Languages , automata, and logic . In Handbook of Formal Languages. Vol. 3 : Beyond Words . Springer , 389--455. Thomas, W. 1997. Languages, automata, and logic. In Handbook of Formal Languages. Vol. 3: Beyond Words. Springer, 389--455."},{"key":"e_1_2_1_55_1","volume-title":"Proceedings of the 5th IEEE Symposium on Logic in Computer Science (LICS'90)","author":"van Glabbeek R.","unstructured":"van Glabbeek , R. , Smolka , S. , Steffen , B. , and Tofts , C . 1990. Reactive, generative, and stratified models of probabilistic processes . In Proceedings of the 5th IEEE Symposium on Logic in Computer Science (LICS'90) . IEEE Computer Society, 130--141. van Glabbeek, R., Smolka, S., Steffen, B., and Tofts, C. 1990. Reactive, generative, and stratified models of probabilistic processes. In Proceedings of the 5th IEEE Symposium on Logic in Computer Science (LICS'90). IEEE Computer Society, 130--141."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1985.12"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/645868.668514"},{"key":"e_1_2_1_58_1","volume-title":"Proceedings of the 1st IEEE Symposium on Logic in Computer Science (LICS'86)","author":"Vardi M. Y.","unstructured":"Vardi , M. Y. and Wolper , P . 1986. An automata-theoretic approach to automatic program verification . In Proceedings of the 1st IEEE Symposium on Logic in Computer Science (LICS'86) . IEEE Computer Society, 332--345. Vardi, M. Y. and Wolper, P. 1986. An automata-theoretic approach to automatic program verification. In Proceedings of the 1st IEEE Symposium on Logic in Computer Science (LICS'86). IEEE Computer Society, 332--345."}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2108242.2108243","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2108242.2108243","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:06:08Z","timestamp":1750241168000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2108242.2108243"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,2]]},"references-count":53,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,2]]}},"alternative-id":["10.1145\/2108242.2108243"],"URL":"https:\/\/doi.org\/10.1145\/2108242.2108243","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,2]]},"assertion":[{"value":"2011-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-03-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}