Tight Game Abstractions of Probabilistic Automata
We present a new game-based abstraction technique for probabilistic automata (PA). The key idea is to use distribution-based abstraction – preserving novel distribution-based (alternating) simulation relations – rather than classical state-based abstraction. These abstractions yield (simple) probabilistic game automata (PGA), turn-based 2 player stochastic games in which moves of both players – as opposed to classical stochastic games – yield distributions over states. As distribution-based (alternating) simulation relations are pre-congruences for composite PGA, abstraction can be done compositionally. Our abstraction yields tighter upper and lower bounds on (extremal) reachability probabilities than state-based abstraction. This shows the potential superiority over state-based abstraction of PA and Markov decision processes.
KeywordsAbstract Model Markov Decision Process Stochastic Game Concrete State Simulation Relation
Unable to display preview. Download preview PDF.
- 1.Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)Google Scholar
- 10.Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266–277. IEEE CS Press (1991)Google Scholar
- 12.Ash, R.B., Doléans-Dade, C.A.: Probability & Measure Theory, 2nd edn. Academic Press (2000)Google Scholar
- 16.Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342–351. IEEE CS Press (2010)Google Scholar
- 19.Kattenbelt, M.: Automated Quantitative Software Verification. PhD thesis, University of Oxford (2010)Google Scholar