Abstract
We consider finite-state Hierarchical Probabilistic Automata (HPA) to model failure-prone open systems. In an HPA, its states are stratified into a fixed number of levels. A k-HPA is an HPA with \(k+1\) levels and it can be used to model open systems where up to k failures can occur. In this paper, we present a new forward algorithm that checks universality of a 1-HPA. This algorithm runs much faster than an earlier backward algorithm. We present the implementation and experimental results for verifying abstracted failure-prone web applications. We also prove a theoretical result showing that the problem of checking emptiness and universality for 2-HPA is undecidable answering an open question.
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 subscriptionsNotes
- 1.
A rational number s has size r iff \(s=\frac{m}{n}\) where m, n are integers, and the binary representation of m and n has at most r bits.
- 2.
HPA tool website: https://github.com/benyue/HPA.
References
Baier, C., Größer, M.: Recognizing \(\omega \)-regular languages with probabilistic automata. In: 20th IEEE Symposium on Logic in Computer Science, pp. 137–146 (2005)
Baier, C., Größer, M., Bertrand, N.: Probabilistic \(\omega \)-automata. J. ACM 59(1), 1–52 (2012)
Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time markov decision processes. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 61–76. Springer, Heidelberg (2004)
Chadha, R., Sistla, A.P., Viswanathan, M.: Probabilistic Büchi automata with non-extremal acceptance thresholds. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 103–117. Springer, Heidelberg (2011)
Chadha, R., Sistla, A.P., Viswanathan, M.: Power of randomization in automata on infinite strings. Log. Methods Comput. Sci. 7(3), 1–22 (2011)
Chadha, R., Sistla, A.P., Viswanathan, M., Ben, Y.: Decidable and expressive classes of probabilistic automata. In: Pitts, A. (ed.) FOSSACS 2015. LNCS, vol. 9034, pp. 200–214. Springer, Heidelberg (2015)
Gimbert, H., Oualhadj, Y.: Probabilistic automata on finite words: decidable and undecidable problems. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 527–538. Springer, Heidelberg (2010)
Größer, M.: Reduction Methods for Probabilistic Model Checking. Ph.D. thesis, TU Dresden (2008)
Paz, A.: Introduction to Probabilistic Automata. Academic Press, Orlando (1971)
PRISM – Probabilistic Symbolic Model Checker. http://www.prismmodelchecker.org
Rabin, M.O.: Probabilistic automata. Inf. Control 6(3), 230–245 (1963)
Acknowledgements
This research is supported by the NSF grants CCF-1319754, CNS-1314485 and CNS-1035914.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Ben, Y., Sistla, A.P. (2015). Model Checking Failure-Prone Open Systems Using Probabilistic Automata. In: Finkbeiner, B., Pu, G., Zhang, L. (eds) Automated Technology for Verification and Analysis. ATVA 2015. Lecture Notes in Computer Science(), vol 9364. Springer, Cham. https://doi.org/10.1007/978-3-319-24953-7_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-24953-7_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24952-0
Online ISBN: 978-3-319-24953-7
eBook Packages: Computer ScienceComputer Science (R0)