Abstract
We present aggressive abstraction techniques for probabilistic automata (PA), a state-based model involving discrete probabilistic and nondeterministic branching. Our abstractions yield abstract PA in which transitions are typed “possible” or “required”—as in modal transition systems—and have constraint functions as target. The key idea is to focus on identifying common combined-transitions from concrete states and putting them as required ones in the abstract state. We prove the correctness of our abstraction techniques, study their relationship, and show that they are compositional w.r.t. parallel composition. We also show the preservation of probabilistic and expected reachability properties for PA.
This research is supported by the EU FP7 MoVeS Project (Modeling, Verification and Control of Complex Systems) and the German-Dutch bilateral project ROCKS.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
de Alfaro, L.: Computing Minimum and Maximum Reachability Times in Probabilistic Systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 66–81. Springer, Heidelberg (1999)
Ash, R.B., Doléans-Dade, C.A.: Probabilty & Measure Theory, 2nd edn. Academic Press (2000)
Baier, C., Kwiatkowska, M.: Model checking for a probabilistic branching time logic with fairness. Distributed Computing 11, 125–155 (1998)
Bertsekas, D.P., Tsitsiklis, J.N.: An analysis of stochastic shortest path problems. Mathematics of Operations Research 16, 580–595 (1991)
Caillaud, B., Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wasowski, A.: Constraint Markov chains. Theor. Comput. Sci. 412, 4373–4404 (2011)
de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, Stanford, CA, USA (1998)
Delahaye, B., Katoen, J.-P., Larsen, K., Legay, A., Pedersen, M., Sher, F., Wasowski, A.: New results on abstract probabilistic automata. In: 2011 11th International Conference on Application of Concurrency to System Design (ACSD), pp. 118–127. IEEE CS Press (2011)
Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wąsowski, A.: Abstract Probabilistic Automata. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 324–339. Springer, Heidelberg (2011)
Huth, M., Jagadeesan, R., Schmidt, D.A.: Modal Transition Systems: A Foundation for Three-Valued Program Analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 155–169. Springer, Heidelberg (2001)
Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: Logic in Computer Science, pp. 266–277. IEEE CS Press (1991)
Katoen, J.-P., Klink, D., Neuhäußer, M.R.: Compositional Abstraction for Stochastic Systems. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 195–211. Springer, Heidelberg (2009)
Kattenbelt, M., Kwiatkowska, M.Z., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. Formal Methods in System Design 36, 246–280 (2010)
Lynch, N.A., Segala, R., Vaandrager, F.W.: Observing branching structure through probabilistic contexts. SIAM J. Comput. 37, 977–1013 (2007)
Milner, R.: Communication and Concurrency. Prentice-Hall, Inc. (1989)
Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)
Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nordic J. of Computing 2, 250–273 (1995)
Swaminathan, M., Katoen, J.-P., Olderog, E.-R.: Layered reasoning for randomized distributed algorithms. Formal Aspects of Computing (to appear, 2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 IFIP International Federation for Information Processing
About this paper
Cite this paper
Sher, F., Katoen, JP. (2012). Compositional Abstraction Techniques for Probabilistic Automata. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds) Theoretical Computer Science. TCS 2012. Lecture Notes in Computer Science, vol 7604. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33475-7_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-33475-7_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33474-0
Online ISBN: 978-3-642-33475-7
eBook Packages: Computer ScienceComputer Science (R0)