Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Information Flow for Timed Automata Read chapter Read first chapter

2017 | OriginalPaper | Chapter

Modal Stochastic Games

Abstraction-Refinement of Probabilistic Automata

Authors : Joost-Pieter Katoen, Falak Sher

Published in: Models, Algorithms, Logics and Tools

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

This paper presents an abstraction-refinement framework for Segala’s probabilistic automata (PA), a slight variant of Markov decision processes. We use Condon and Ladner’s two-player probabilistic game automata extended with possible and required transitions—as in Larsen and Thomsen’s modal transition systems—as abstract models. The key idea is to refine player-one and player-two states separately resulting in a nested abstract-refine loop. We show the adequacy of this approach for obtaining tight bounds on extremal reachability probabilities.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Admissible Strategies in Timed Games
next chapter A Coinductive Equational Characterisation of Trace Inclusion for Regular Processes
Footnotes
1
As this paper does not cover parallel composition all PGAs are closed. For modeling PGAs in a compositonal manner though, the distinction between internal and other actions is important, see [7].
 
2
For example, let \(x=\max \) in \( \mathrm {Pr}^x(T^{\prime })\) then \(\mathbf {1}=\max \) and \(\mathbf {2}=\min \) (player-one maximizes whereas the player-two minimizes the probability) or vice versa.
 
3
This may converge slower than allowing for coarser splittings (as in [5]), but yields smaller state spaces.
 
Literature
1.
Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nordic J. Comput. 2(2), 250–273 (1995)MathSciNetMATH
2.
Norman, G.: Analysing randomized distributed algorithms. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 384–418. Springer, Heidelberg (2004). doi:10.​1007/​978-3-540-24611-4_​11 CrossRef
3.
4.
Delahaye, B., Katoen, J.P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wasowski, A.: Abstract probabilistic automata. Inf. Comput. 232, 66–116 (2013)MathSciNetCrossRefMATH
5.
Kattenbelt, M., Kwiatkowska, M.Z., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. Formal Methods Syst. Des. 36(3), 246–280 (2010)CrossRefMATH
6.
Vira, F.S., Katoen, J.-P.: Tight game abstractions of probabilistic automata. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 576–591. Springer, Heidelberg (2014). doi:10.​1007/​978-3-662-44584-6_​39
7.
Sher, F., Katoen, J.-P.: Compositional abstraction techniques for probabilistic automata. In: Baeten, J.C.M., Ball, T., Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 325–341. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-33475-7_​23 CrossRef
8.
9.
Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: 20 years of modal and mixed specifications. Bull. EATCS 95, 94–129 (2008)MathSciNetMATH
10.
Huth, M., Jagadeesan, R., Schmidt, D.: 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). doi:10.​1007/​3-540-45309-1_​11 CrossRef
11.
12.
Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH
13.
14.
15.
Baier, C., Engelen, B., Majster-Cederbaum, M.E.: Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci. 60(1), 187–231 (2000)MathSciNetCrossRefMATH
16.
Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266–277. IEEE Computer Society (1991)
17.
Larsen, K.G., Thomsen, B.: Compositional proofs by partial specification of processes. In: Chytil, M.P., Koubek, V., Janiga, L. (eds.) MFCS 1988. LNCS, vol. 324, pp. 414–423. Springer, Heidelberg (1988). doi:10.​1007/​BFb0017164 CrossRef
18.
Sher, F.: Abstraction and refinement of probabilistic automata using modal stochastic games. Ph.D. thesis, RWTH Aachen University Aachener Informatik-Berichte AIB-2015-10 (2015)
19.
D’Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reachability analysis of probabilistic systems by successive refinements. In: Alfaro, L., Gilmore, S. (eds.) PAPM-PROBMIV 2001. LNCS, vol. 2165, pp. 39–56. Springer, Heidelberg (2001). doi:10.​1007/​3-540-44804-7_​3 CrossRef
20.
Katoen, J.P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for probabilistic systems. J. Log. Algebr. Program. 81(4), 356–389 (2012)MathSciNetCrossRefMATH
21.
22.
Dehnert, C., Gebler, D., Volpato, M., Jansen, D.N.: On abstraction of probabilistic systems. In: Remke, A., Stoelinga, M. (eds.) Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems. LNCS, vol. 8453, pp. 87–116. Springer, Heidelberg (2014). doi:10.​1007/​978-3-662-45489-3_​4 CrossRef
23.
de Alfaro, L., Godefroid, P., Jagadeesan, R.: Three-valued abstractions of games: uncertainty, but with precision. In: LICS, pp. 170–179. IEEE Computer Society (2004)
24.
25.
26.
Hermanns, H., Krčál, J., Křetínský, J.: Probabilistic bisimulation: naturally on distributions. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 249–265. Springer, Heidelberg (2014). doi:10.​1007/​978-3-662-44584-6_​18
27.
28.
Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203–210. IEEE Computer Society (1988)
29.
Caillaud, B., Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wasowski, A.: Constraint Markov chains. Theoret. Comput. Sci. 412(34), 4373–4404 (2011)MathSciNetCrossRefMATH
30.
Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Uppaal in 1995. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 431–434. Springer, Heidelberg (1996). doi:10.​1007/​3-540-61042-1_​66 CrossRef
31.
D’Argenio, P.R., Katoen, J.-P., Ruys, T.C., Tretmans, J.: The bounded retransmission protocol must be on time!. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 416–431. Springer, Heidelberg (1997). doi:10.​1007/​BFb0035403 CrossRef
Metadata
Title
Modal Stochastic Games
Authors
Joost-Pieter Katoen
Falak Sher
Copyright Year
2017
Book
Models, Algorithms, Logics and Tools

Print ISBN: 978-3-319-63120-2

Electronic ISBN: 978-3-319-63121-9

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-3-319-63121-9_21

Premium Partner

    Image Credits