research-article

Probabilistic ω-automata

Authors:

Christel Baier,

Marcus Grösser,

Nathalie BertrandAuthors Info & Claims

Journal of the ACM (JACM), Volume 59, Issue 1

Article No.: 1, Pages 1 - 52

https://doi.org/10.1145/2108242.2108243

Published: 02 March 2012 Publication History

Abstract

Probabilistic ω-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 ω-automata, such as Büchi, Rabin or Streett conditions. The accepted language of a probabilistic ω-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 ω-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 λ ∈ ]0,1[ that specifies a lower probability bound for the acceptance probability. We provide a comparison of probabilistic ω-automata under these three semantics and nondeterministic ω-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.

References

[1]

Alur, R., Courcoubetis, C., and Yannakakis, M. 1995. Distinguishing tests for nondeterministic and probabilistic machines. In Proceedings of the 27th ACM Symposium on Theory of Computing (STOC'95). ACM, 363--372.

Digital Library

[2]

Ambainis, A. 1996. The complexity of probabilistic versus deterministic finite automata. In Proceedings of the 7th International Symposium on Algorithms and Computation (ISAAC'96). Lecture Notes in Computer Science, vol. 1178, Springer, 233--238.

Digital Library

[3]

Andrés, M. E., Palamidessi, C., van Rossum, P., and Sokolova, A. 2010. Information hiding in probabilistic concurrent systems. In Proceedings of the 7th International Conference on Quantitative Evaluation of Systems (QEST'10). IEEE Computer Society, 17--26.

Digital Library

[4]

Baier, C., Bertrand, N., and Grösser, M. 2008. On decision problems for probabilistic Büchi automata. In Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'08). Lecture Notes in Computer Science, vol. 4962, Springer, 287--301.

Digital Library

[5]

Baier, C. and Grösser, M. 2005. Recognizing ω-regular languages with probabilistic automata. In Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS'05). IEEE Computer Society, 137--146.

Digital Library

[6]

Bertrand, N., Genest, B., and Gimbert, H. 2009. Qualitative determinacy and decidability of stochastic games with signals. In Proceedings of the 24th IEEE Symposium on Logic in Computer Science (LICS'09). IEEE Computer Society, 319--328.

Digital Library

[7]

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.

Digital Library

[8]

Blondel, V. and Canterini, V. 2003. Undecidable problems for probabilistic finite automata. Theory Comput. Syst. 36, 231--245.

[9]

Burago, D., de Rougemont, M., and Slissenko, A. 1996. On the complexity of partially observed Markov decision processes. Theoret. Comput. Sci. 157, 2, 161--183.

Digital Library

[10]

Chadha, R., Sistla, A. P., and Viswanathan, M. 2009a. On the expressiveness and complexity of randomization in finite state monitors. J. ACM 56, 5.

Digital Library

[11]

Chadha, R., Sistla, A. P., and Viswanathan, M. 2009b. Power of randomization in automata on infinite strings. In Proceedings of the 20th International Conference on Concurrency Theory (CONCUR'09). Lecture Notes in Computer Science, vol. 5710, Springer, 229--243.

Digital Library

[12]

Chadha, R., Sistla, A. P., and Viswanathan, M. 2011. Probabilistic Büchi automata with non-extremal acceptance thresholds. In Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 6538, Springer, 103--117.

Digital Library

[13]

Chatterjee, K., Doyen, L., and Henzinger, T. 2009. Power of randomization in automata on infinite strings. In Proceedings of the 20th International Conference on Concurrency Theory (CONCUR'09). Lecture Notes in Computer Science, vol. 5710, Springer, 244--258.

Digital Library

[14]

Chatterjee, K., Doyen, L., and Henzinger, T. A. 2010. Qualitative analysis of partially-observable markov decision processes. In Proceedings of the 35th International Symposium on Mathematical Foundations of Computer Science (MFCS'10). Lecture Notes in Computer Science, vol. 6281, Springer, 258--269.

Digital Library

[15]

Chatterjee, K., Doyen, L., Henzinger, T. A., and Raskin, J.-F. 2006. Algorithms for omega-regular games with imperfect information. In Proceedings of the 20th International Workshop on Computer Science Logic (CSL'06). Lecture Notes in Computer Science, vol. 4207, Springer, 287--302.

Digital Library

[16]

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.

[17]

Chatterjee, K. and Henzinger, T. A. 2010. Probabilistic automata on infinite words: Decidability and undecidability results. In Proceedings of the 8th International Symposium on Automated Technology for Verification and Analysis (ATVA'10). Lecture Notes in Computer Science, vol. 6252, Springer, 1--16.

Digital Library

[18]

Chatzikokolakis, K. and Palamidessi, C. 2010. Making random choices invisible to the scheduler. Inf. Comput. 208, 6, 694--715.

Digital Library

[19]

Cheung, L., Lynch, N. A., Segala, R., and Vaandrager, F. W. 2006. Switched PIOA: Parallel composition via distributed scheduling. Theoret. Comput. Sci. 365, 1-2, 83--108.

Digital Library

[20]

Condon, A. 2001. Bounded error probabilistic finite state automata. In Handbook of Randomized Computing. Vol. II, Springer, 509--532.

[21]

Courcoubetis, C. and Yannakakis, M. 1995. The complexity of probabilistic verification. J. ACM 42, 4, 857--907.

Digital Library

[22]

de Alfaro, L. 1997. Formal verification of probabilistic systems. Ph.D. dissertation, Stanford University, Department of Computer Science.

[23]

de Alfaro, L. 1998. Stochastic transition systems. In Proceedings of the 9th International Conference on Concurrency Theory (CONCUR'98). Lecture Notes in Computer Science, vol. 1466, Springer, 423--438.

Digital Library

[24]

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.

[25]

Dwork, C. and Stockmeyer, L. 1990. A time-complexity gap for two-way probabilistic finite state automata. SIAM J. Comput. 19, 1011--1023.

Digital Library

[26]

Feller, W. 1950. An Introduction to Probability Theory and Its Applications. Wiley, New York.

[27]

Freivalds, R. 1981. Probabilistic two-way machines. In Proceedings of the 10th International Symposium on Mathematical Foundations of Computer Science (MFCS'81). Lecture Notes in Computer Science, vol. 118, Springer, 33--45.

Digital Library

[28]

Gimbert, H. and Oualhadj, Y. 2010. Probabilistic automata on finite words: Decidable and undecidable problems. In Proceedings of the 37th International Colloquium on Automata, Languages and Programming (ICALP'10). Lecture Notes in Computer Science, vol. 6199, Springer, 527--538.

Digital Library

[29]

Giro, S. and D'Argenio, P. 2007. Quantitative model checking revisited: neither decidable nor approximable. In Proceedings of the 5th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'07). Lecture Notes in Computer Science, vol. 4763, Springer, 179--194.

Digital Library

[30]

Grädel, 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.

[31]

Gripon, V. and Serre, O. 2009. Qualitative concurrent stochastic games with imperfect information. In Proceedings of the 36th International Colloquium on Automata, Languages and Programming (ICALP'09). Lecture Notes in Computer Science, vol. 5556, Springer, 200--211.

Digital Library

[32]

Grösser, M. 2008. Reduction methods for probabilistic model checking. Ph.D. thesis, Technische Universität Dresden.

[33]

Hart, S., Sharir, M., and Pnueli, A. 1983. Termination of probabilistic concurrent programs. ACM Trans. Prog. Lang. Syst. 5, 3, 356--380.

Digital Library

[34]

Kaelbling, L., Littman, M., and Cassandra, A. 1995. Partially observable markov decision processes for artificial intelligence. In Lecture Notes in Computer Science, vol. 981, Springer, 1--17.

Digital Library

[35]

Littman, M. 1996. Algorithms for sequential decision making. Ph.D. thesis, Brown University, Department of Computer Science.

Digital Library

[36]

Lovejoy, W. 1991. A survey of algorithmic methods for partially observable Markov decision processes. Ann. Oper. Res. 28, 1, 47--65.

Digital Library

[37]

Madani, O., Hanks, S., and Condon, A. 2003. On the undecidability of probabilistic planning and related stochastic optimization problems. Artif. Intell. 147, 1-2, 5--34.

Digital Library

[38]

Monahan, G. 1982. A survey of partially observable Markov decision processes: Theory, models, and algorithms. Manag. Sci. 28, 1, 1--16.

Digital Library

[39]

Papadimitriou, C. and Tsitsiklis, J. 1987. The complexity of Markov decision processes. Math. Oper. Res. 12, 3, 441--450.

Digital Library

[40]

Paz, A. 1966. Some aspects of probabilistic automata. Inf. Comput. 9, 1, 26--60.

[41]

Paz, A. 1971. Introduction to Probabilistic Automata. Academic Press.

Digital Library

[42]

Perrin, D. and Pin, J.-E. 2004. Infinite Words: Automata, Semigroups, Logic and Games. Pure and Applied Mathematics, vol. 141, Elsevier.

[43]

Pnueli, A. and Zuck, L. D. 1993. Probabilistic verification. Inf. Comput. 103, 1, 1--29.

Digital Library

[44]

Rabin, M. O. 1963. Probabilistic automata. Information and Control 6, 3, 230--245.

[45]

Reif, J. H. 1984. The complexity of two-player games of incomplete information. J. Comput. Syst. Sci. 29, 2, 274--301.

[46]

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.

[47]

Reisz, R. D. 1999b. Decomposition theorems for probabilistic automata over infinite objects. Informatica, Lithuanian Acad. Sci. 10, 4, 427--440.

[48]

Rosier, L. E. and Yen, H.-C. 1986. On the complexity of deciding fair termination of probabilistic concurrent finite-state programs. In Proceedings of the 13th International Colloquium on Automata, Languages and Programming (ICALP'86). Lecture Notes in Computer Science, vol. 226, Springer, 334--343.

Digital Library

[49]

Safra, S. 1988. On the complexity of ω-automata. In Proceedings of the 29th Symposium on Foundations of Computer Science (FOCS'88). IEEE Computer Society, 319--327.

Digital Library

[50]

Safra, S. and Vardi, M. Y. 1989. On ω-automata and temporal logic. In Proceedings of the 21st ACM Symposium on Theory of Computing (STOC'89). ACM, 127--137.

Digital Library

[51]

Segala, R. 1995. Modeling and verification of randomized distributed real-time systems. Ph.D. thesis, Massachusetts Institute of Technology.

Digital Library

[52]

Sondik, E. J. 1971. The optimal control of partially observable Markov processes. Ph.D. thesis, Stanford University.

[53]

Thomas, W. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science. Vol. B: Formal Models and Semantics. Elsevier Science, 133--191.

Digital Library

[54]

Thomas, W. 1997. Languages, automata, and logic. In Handbook of Formal Languages. Vol. 3: Beyond Words. Springer, 389--455.

Digital Library

[55]

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.

[56]

Vardi, M. Y. 1985. Automatic verification of probabilistic concurrent finite-state programs. In Proceedings of the 26th Symposium on Foundations of Computer Science (FOCS'85). IEEE Computer Society, 327--338.

Digital Library

[57]

Vardi, M. Y. 1994. Nontraditional applications of automata theory. In Proceedings of International Conference on Theoretical Aspects of Computer Software (TACS'94). Lecture Notes in Computer Science, vol. 789, Springer, 575--597.

Digital Library

[58]

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.

Cited By

Wang QYing M(2024)Quantum Büchi automataTheoretical Computer Science10.1016/j.tcs.2024.1147401012:COnline publication date: 12-Oct-2024
https://dl.acm.org/doi/10.1016/j.tcs.2024.114740
Hammi BZeadally SNebhen J(2023)Security Threats, Countermeasures, and Challenges of Digital Supply ChainsACM Computing Surveys10.1145/358899955:14s(1-40)Online publication date: 22-Mar-2023
https://dl.acm.org/doi/10.1145/3588999
Doyen L(2023)Stochastic Games with Synchronization ObjectivesJournal of the ACM10.1145/358886670:3(1-35)Online publication date: 23-May-2023
https://dl.acm.org/doi/10.1145/3588866
Show More Cited By

Index Terms

Probabilistic ω-automata

Recommendations

On the Size of Unary Probabilistic and Nondeterministic Automata
Non-Classical Models of Automata and Applications II

We investigate and compare the descriptional power of unary probabilistic and nondeterministic automata (pfa's and nfa's, respectively). We show the existence of a family of languages hard for pfa's in the following sense: For any positive integer d, ...
A power-set construction for reducing Büchi automata to non-determinism degree two

Buchi automata are finite automata that accept languages of infinitely long strings, so-called @w-languages. It is well known that, unlike in the finite-string case, deterministic and non-deterministic Buchi automata accept different @w-language classes,...
Deciding the Value 1 Problem for Probabilistic Leaktight Automata
LICS '12: Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science

The value 1 problem is a decision problem for probabilistic automata over finite words: given a probabilistic automaton, are there words accepted with probability arbitrarily close to 1? This problem was proved undecidable recently. We sharpen this ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of the ACM

Journal of the ACM Volume 59, Issue 1

February 2012

166 pages

ISSN:0004-5411

EISSN:1557-735X

DOI:10.1145/2108242

Issue’s Table of Contents

Copyright © 2012 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 March 2012

Accepted: 01 November 2011

Revised: 01 October 2011

Received: 01 February 2011

Published in JACM Volume 59, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

49
Total Citations
View Citations
807
Total Downloads

Downloads (Last 12 months)40
Downloads (Last 6 weeks)6

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wang QYing M(2024)Quantum Büchi automataTheoretical Computer Science10.1016/j.tcs.2024.1147401012:COnline publication date: 12-Oct-2024
https://dl.acm.org/doi/10.1016/j.tcs.2024.114740
Hammi BZeadally SNebhen J(2023)Security Threats, Countermeasures, and Challenges of Digital Supply ChainsACM Computing Surveys10.1145/358899955:14s(1-40)Online publication date: 22-Mar-2023
https://dl.acm.org/doi/10.1145/3588999
Doyen L(2023)Stochastic Games with Synchronization ObjectivesJournal of the ACM10.1145/358886670:3(1-35)Online publication date: 23-May-2023
https://dl.acm.org/doi/10.1145/3588866
Liu CYu H(2023)AI-Empowered Persuasive Video Generation: A SurveyACM Computing Surveys10.1145/358876455:13s(1-31)Online publication date: 13-Jul-2023
https://dl.acm.org/doi/10.1145/3588764
Jessurun NDizon-Paradis OHarrison JGhosh STehranipoor MWoodard DAsadizanjani N(2023)FPIC: A Novel Semantic Dataset for Optical PCB AssuranceACM Journal on Emerging Technologies in Computing Systems10.1145/358803219:2(1-21)Online publication date: 18-May-2023
https://dl.acm.org/doi/10.1145/3588032
Das DNishimura YVivek RTakeda NFish SPlötz TChernova S(2023)Explainable Activity Recognition for Smart Home SystemsACM Transactions on Interactive Intelligent Systems10.1145/356153313:2(1-39)Online publication date: 5-May-2023
https://dl.acm.org/doi/10.1145/3561533
van der Vegt MJansen NJunges S(2023)Robust Almost-Sure Reachability in Multi-Environment MDPsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-30823-9_26(508-526)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30823-9_26
Carr SJansen NTopcu U(2022)Task-Aware Verifiable RNN-Based Policies for Partially Observable Markov Decision ProcessesJournal of Artificial Intelligence Research10.1613/jair.1.1296372(819-847)Online publication date: 4-Jan-2022
https://dl.acm.org/doi/10.1613/jair.1.12963
Chatterjee KSaona RZiliotto B(2022)Finite-Memory Strategies in POMDPs with Long-Run Average ObjectivesMathematics of Operations Research10.1287/moor.2020.111647:1(100-119)Online publication date: 1-Feb-2022
https://dl.acm.org/doi/10.1287/moor.2020.1116
Doyen L(2022)Stochastic Games with Synchronizing ObjectivesProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3532439(1-12)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3532439
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents