Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Bringing LTL Model Checking to Biologists Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games

verfasst von : Ernst Moritz Hahn, Sven Schewe, Andrea Turrini, Lijun Zhang

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

2.5 player parity games combine the challenges posed by 2.5 player reachability games and the qualitative analysis of parity games. These two types of problems are best approached with different types of algorithms: strategy improvement algorithms for 2.5 player reachability games and recursive algorithms for the qualitative analysis of parity games. We present a method that—in contrast to existing techniques—tackles both aspects with the best suited approach and works exclusively on the 2.5 player game itself. The resulting technique is powerful enough to handle games with several million states.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Dynamic Reductions for Model Checking Concurrent Software
Nächstes Kapitel Counterexample Validation and Interpolation-Based Refinement for Forest Automata
Fußnoten
1
In classic strategy improvement algorithms, the restriction to implementing a change once is made to keep it easy to identify the improvements. Such changes will also lead to an improvement when applied repeatedly.
 
2
In the notation of [7, 9], \(\pi = \mathsf {Tr}_{\text {almost}}(\overline{\pi }_Q)\).
 
Literatur
1.
2.
Andersson, D., Miltersen, P.B.: The complexity of solving stochastic games on graphs. In: Dong, Y., Du, D.-Z., Ibarra, O. (eds.) ISAAC 2009. LNCS, vol. 5878, pp. 112–121. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-10631-6_​13 CrossRef
3.
Berwanger, D., Dawar, A., Hunter, P., Kreutzer, S.: DAG-width and parity games. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol. 3884, pp. 524–536. Springer, Heidelberg (2006). doi:10.​1007/​11672142_​43 CrossRef
4.
Björklund, H., Vorobyov, S.: A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games. DAM 155(2), 210–229 (2007)MathSciNetMATH
5.
Browne, A., Clarke, E.M., Jha, S., Long, D.E., Marrero, W.R.: An improved algorithm for the evaluation of fixpoint expressions. TCS 178(1–2), 237–255 (1997)MathSciNetCrossRefMATH
6.
7.
Chatterjee, K., de Alfaro, L., Henzinger, T.A.: The complexity of quantitative concurrent parity games. In: SODA, pp. 678–687. SIAM (2006)
8.
Chatterjee, K., de Alfaro, L., Henzinger, T.A.: Strategy improvement for concurrent reachability and turn-based stochastic safety games. J. Comput. Syst. Sci. 79(5), 640–657 (2013)MathSciNetCrossRefMATH
9.
Chatterjee, K., Henzinger, T.A.: Strategy improvement and randomized subexponential algorithms for stochastic parity games. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol. 3884, pp. 512–523. Springer, Heidelberg (2006). doi:10.​1007/​11672142_​42 CrossRef
10.
Chatterjee, K., Henzinger, T.A.: Strategy improvement for stochastic rabin and streett games. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 375–389. Springer, Heidelberg (2006). doi:10.​1007/​11817949_​25 CrossRef
11.
Chatterjee, K., Henzinger, T.A., Jobstmann, B., Radhakrishna, A.: Gist: a solver for probabilistic games. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 665–669. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-14295-6_​57 CrossRef
12.
Chatterjee, K., Jurdziński, M., Henzinger, T.A.: Quantitative stochastic parity games. In: SODA 2004, pp. 121–130 (2004)
13.
Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: PRISM-games: a model checker for stochastic multi-player games. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 185–191. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-36742-7_​13 CrossRef
14.
Condon, A.: On algorithms for simple stochastic games. Adv. Comput. Complex. Theory 13, 51–73 (1993)MathSciNetMATH
15.
16.
de Alfaro, L., Henzinger, T.A., Majumdar, R.: From verification to control: dynamic programs for omega-regular objectives. In: LICS, pp. 279–290 (2001)
17.
de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. In: Vitter, J.S., Spirakis, P.G., Yannakakis, M. (eds.) Proceedings on 33rd Annual ACM Symposium on Theory of Computing, 6–8 July 2001, Heraklion, Crete, Greece, pp. 675–683. ACM (2001)
18.
19.
Emerson, E.A., Jutla, C.S.: Tree automata, \(\mu \)-calculus and determinacy. In: FOCS, pp. 368–377 (1991)
20.
Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model-checking for fragments of \(\mu \)-calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 385–396. Springer, Heidelberg (1993). doi:10.​1007/​3-540-56922-7_​32 CrossRef
21.
Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional \(\mu \)-calculus. In: LICS, pp. 267–278 (1986)
22.
Fearnley, J.: Non-oblivious strategy improvement. In: LPAR, pp. 212–230 (2010)
23.
Friedmann, O.: An exponential lower bound for the parity game strategy improvement algorithm as we know it. In: LICS, pp. 145–156 (2009)
24.
Friedmann, O., Hansen, T.D., Zwick, U.: A subexponential lower bound for the random facet algorithm for parity games. In: SODA, pp. 202–216 (2011)
25.
26.
Gimbert, H., Horn, F.: Solving simple stochastic games with few random vertices. LMCS 5(2:9), 1–17 (2009)MathSciNetMATH
27.
Hahn, E.M. Li, G., Schewe, S., Turrini, A., Zhang, L.: Lazy probabilistic model checking without determinisation. In: CONCUR. LIPIcs, vol. 42, pp. 354–367 (2015)
28.
Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312–317. Springer, Heidelberg (2014). doi:10.​1007/​978-3-319-06410-9_​22 CrossRef
29.
Hahn, E.M., Schewe, S., Turrini, A., Zhang, L.: Synthesising strategy improvement, recursive algorithms for solving 2.5 player parity games. arXiv:​1607.​01474
30.
Hahn, E.M., Schewe, S., Turrini, A., Zhang, L.: A simple algorithm for solving qualitative probabilistic parity games. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 291–311. Springer, Heidelberg (2016). doi:10.​1007/​978-3-319-41540-6_​16 CrossRef
31.
32.
Jurdziński, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. SIAM J. Comput. 38(4), 1519–1532 (2008)MathSciNetCrossRefMATH
33.
Kemeny, J.G., Snell, J.L., Knapp, A.W.: Denumerable Markov Chains. D. Van Nostrand Company, Princeton (1966)MATH
34.
35.
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22110-1_​47 CrossRef
36.
Ludwig, W.: A subexponential randomized algorithm for the simple stochastic game problem. Inf. Comput. 117(1), 151–155 (1995)MathSciNetCrossRefMATH
37.
38.
39.
Piterman, N.: From nondeterministic Büchi, Streett automata to deterministic parity automata. J. Log. Methods Comput. Sci. 3(3:5), 1–21 (2007)MathSciNetMATH
40.
Puri, A.: Theory of hybrid systems and discrete event systems. Ph.D. thesis, Computer Science Department, University of California, Berkeley (1995)
41.
Schewe, S.: An optimal strategy improvement algorithm for solving parity and payoff games. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 369–384. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-87531-4_​27 CrossRef
42.
43.
Schewe, S., Finkbeiner, B.: Satisfiability and finite model property for the alternating-time \(\mu \)-calculus. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 591–605. Springer, Heidelberg (2006). doi:10.​1007/​11874683_​39 CrossRef
44.
45.
Schewe, S., Trivedi, A., Varghese, T.: Symmetric strategy improvement. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 388–400. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-47666-6_​31
46.
Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 628–641. Springer, Heidelberg (1998). doi:10.​1007/​BFb0055090 CrossRef
47.
Vöge, J., Jurdziński, M.: A discrete strategy improvement algorithm for solving parity games (Extended abstract). In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 202–215. Springer, Heidelberg (2000). doi:10.​1007/​10722167_​18 CrossRef
48.
Wilke, T.: Alternating tree automata, parity games, and modal \(\mu \)-calculus. Bull. Soc. Math. Belg. 8(2), 359 (2001)MathSciNetMATH
49.
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. TCS 200(1–2), 135–183 (1998)MathSciNetCrossRefMATH
50.
Metadaten
Titel
Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
verfasst von
Ernst Moritz Hahn
Sven Schewe
Andrea Turrini
Lijun Zhang
Copyright-Jahr
2017
Buch
Verification, Model Checking, and Abstract Interpretation

Print ISBN: 978-3-319-52233-3

Electronic ISBN: 978-3-319-52234-0

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-52234-0_15

Premium Partner

    Bildnachweise