Abstract
Probabilistic Büchi Automata (PBA) are randomized, finite state automata that process input strings of infinite length. Based on the threshold chosen for the acceptance probability, different classes of languages can be defined. In this paper, we present a number of results that clarify the power of such machines and properties of the languages they define. The broad themes we focus on are as follows. We precisely characterize the complexity of the emptiness, universality, and language containment problems for such machines, answering canonical questions central to the use of these models in formal verification. Next, we characterize the languages recognized by PBAs topologically, demonstrating that though general PBAs can recognize languages that are not regular, topologically the languages are as simple as ω-regular languages. Finally, we introduce Hierarchical PBAs, which are syntactically restricted forms of PBAs that are tractable and capture exactly the class of ω-regular languages.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alpern, B., Schneider, F.: Defining liveness. Information Processing Letters 21, 181–185 (1985)
Baier, C., Bertrand, N., Größer, M.: On decision problems for probabilistic büchi automata. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 287–301. Springer, Heidelberg (2008)
Baier, C., Größer, M.: Recognizing ω-regular languages with probabilistic automata. In: Proceedings of the IEEE Symposium on Logic in Computer Science, pp. 137–146 (2005)
Chadha, R., Sistla, A.P., Viswanathan, M.: On the expressiveness and complexity of randomization in finite state monitors. In: LICS 2008- 23rd Annual IEEE Symposium on Logic in Computer Science, pp. 18–29. IEEE Computer Society, Los Alamitos (2008)
Chadha, R., Sistla, A.P., Viswanathan, M.: On the expressiveness and complexity of randomization in finite state monitors. Journal of the ACM (to appear), http://www.cs.uiuc.edu/homes/rch/TechReports/MonitoringTechReport.pdf
Condon, A., Lipton, R.J.: On the complexity of space bounded interactive proofs (extended abstract). In: 30th Annual Symposium on Foundations of Computer Science, pp. 462–467 (1989)
Groesser, M.: Reduction Methods for Probabilistic Model Checking. PhD thesis, TU Dresden (2008)
Holzmann, G.J., Peled, D.: The state of spin. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996)
Kemeny, J., Snell, J.: Denumerable Markov Chains. Springer, Heidelberg (1976)
Kurshan, R.P.: Computer Aided Verification of the Coordinated Processes: The Automata Theoretic Approach. Princeton University Press, Princeton (1994)
Lamport, L.: Logical foundation, distributed systems- methods and tools for specification, vol. 190. Springer, Heidelberg (1985)
Paz, A.: Introduction to Probabilistic Automata. Academic Press, London (1971)
Perrin, D., Pin, J.-E.: Infinite Words: Automata, Semigroups, Logic and Games. Elsevier, Amsterdam (2004)
Rabin, M.O.: Probabilitic automata. Information and Control 6(3), 230–245 (1963)
Rutten, J.M., Kwiatkowska, M., Norman, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. AMS (2004)
Salomaa, A.: Formal Languages. Academic Press, London (1973)
Sistla, A.P.: Theoretical Issues in the Design and Verification of Distributed Systems. PhD thesis, Harvard University (1983)
Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, vol. B, pp. 133–192 (1990)
Vardi, M.: Automatic verification of probabilistic concurrent systems. In: 26th annual Symposium on Foundations of Computer Science, pp. 327–338. IEEE Computer Society Press, Los Alamitos (1985)
Vardi, M., Wolper, P.: An automata theoretic approach to automatic program verification. In: Proceedings of the first IEEE Symposium on Logic in Computer Science (1986)
Vardi, M., Wolper, P., Sistla, A.P.: Reasoning about infinite computation paths. In: Proceedings of the 24th IEEE Symposium on Foundations of Computer Science (1983)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chadha, R., Sistla, A.P., Viswanathan, M. (2009). Power of Randomization in Automata on Infinite Strings. In: Bravetti, M., Zavattaro, G. (eds) CONCUR 2009 - Concurrency Theory. CONCUR 2009. Lecture Notes in Computer Science, vol 5710. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04081-8_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-04081-8_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04080-1
Online ISBN: 978-3-642-04081-8
eBook Packages: Computer ScienceComputer Science (R0)