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:
Bringing LTL Model Checking to Biologists Read chapter Read first chapter

2017 | OriginalPaper | Chapter

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

Authors : Ernst Moritz Hahn, Sven Schewe, Andrea Turrini, Lijun Zhang

Published in: Verification, Model Checking, and Abstract Interpretation

Publisher: Springer International Publishing

Log in

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

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.

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 Dynamic Reductions for Model Checking Concurrent Software
next chapter Counterexample Validation and Interpolation-Based Refinement for Forest Automata
Footnotes
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)\).
 
Literature
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.
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.
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.
Metadata
Title
Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
Authors
Ernst Moritz Hahn
Sven Schewe
Andrea Turrini
Lijun Zhang
Copyright Year
2017
Book
Verification, Model Checking, and Abstract Interpretation

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

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

Copyright Year: 2017

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

Premium Partner

    Image Credits