×

zbMATH — the first resource for mathematics

Synthesising strategy improvement and recursive algorithms for solving 2.5 player parity games. (English) Zbl 06687361
Bouajjani, Ahmed (ed.) et al., Verification, model checking, and abstract interpretation. 18th international conference, VMCAI 2017, Paris, France, January 15–17, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-52233-3/pbk; 978-3-319-52234-0/ebook). Lecture Notes in Computer Science 10145, 266-287 (2017).
Summary: 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.
For the entire collection see [Zbl 1355.68009].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. JACM 49(5), 672–713 (2002) · Zbl 1326.68181 · doi:10.1145/585265.585270
[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 · Zbl 1272.91025 · doi:10.1007/978-3-642-10631-6_13
[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 · Zbl 1136.68447 · doi:10.1007/11672142_43
[4] Björklund, H., Vorobyov, S.: A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games. DAM 155(2), 210–229 (2007) · Zbl 1176.68087
[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) · Zbl 0901.68118 · doi:10.1016/S0304-3975(96)00228-9
[6] Chatterjee, K.: The complexity of stochastic müller games. Inf. Comput. 211, 29–48 (2012) · Zbl 1238.91022 · doi:10.1016/j.ic.2011.11.004
[7] Chatterjee, K., de Alfaro, L., Henzinger, T.A.: The complexity of quantitative concurrent parity games. In: SODA, pp. 678–687. SIAM (2006) · Zbl 1192.68430 · doi:10.1145/1109557.1109631
[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) · Zbl 1269.91022 · doi:10.1016/j.jcss.2012.12.001
[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 · Zbl 1136.91322 · doi:10.1007/11672142_42
[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 · Zbl 1151.68474 · doi:10.1007/11817949_25
[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 · Zbl 05772670 · doi:10.1007/978-3-642-14295-6_57
[12] Chatterjee, K., Jurdziński, M., Henzinger, T.A.: Quantitative stochastic parity games. In: SODA 2004, pp. 121–130 (2004) · Zbl 1318.91027
[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 · Zbl 1381.68151 · doi:10.1007/978-3-642-36742-7_13
[14] Condon, A.: On algorithms for simple stochastic games. Adv. Comput. Complex. Theory 13, 51–73 (1993) · Zbl 0808.90141 · doi:10.1090/dimacs/013/04
[15] Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995) · Zbl 0885.68109 · doi:10.1145/210332.210339
[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) · Zbl 1323.68417
[18] de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. J. Comput. Syst. Sci. 68(2), 374–397 (2004) · Zbl 1093.91001 · doi:10.1016/j.jcss.2003.07.009
[19] Emerson, E.A., Jutla, C.S.: Tree automata, \[ \mu \] -calculus and determinacy. In: FOCS, pp. 368–377 (1991) · doi:10.1109/SFCS.1991.185392
[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 · Zbl 0973.68120 · doi:10.1007/3-540-56922-7_32
[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) · Zbl 1310.91040 · doi:10.1007/978-3-642-17511-4_13
[23] Friedmann, O.: An exponential lower bound for the parity game strategy improvement algorithm as we know it. In: LICS, pp. 145–156 (2009) · doi:10.1109/LICS.2009.27
[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) · Zbl 1377.68091 · doi:10.1137/1.9781611973082.19
[25] Friedmann, O., Lange, M.: Solving parity games in practice. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 182–196. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-04761-9_15 · Zbl 1258.68077 · doi:10.1007/978-3-642-04761-9_15
[26] Gimbert, H., Horn, F.: Solving simple stochastic games with few random vertices. LMCS 5(2:9), 1–17 (2009) · Zbl 1163.91318
[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) · Zbl 1374.68290
[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 · Zbl 06400680 · doi:10.1007/978-3-319-06410-9_22
[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 · Zbl 06687361
[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 · doi:10.1007/978-3-319-41540-6_16
[31] Jurdziński, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000). doi: 10.1007/3-540-46541-3_24 · Zbl 0962.68111 · doi:10.1007/3-540-46541-3_24
[32] Jurdziński, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. SIAM J. Comput. 38(4), 1519–1532 (2008) · Zbl 1173.91326 · doi:10.1137/070686652
[33] Kemeny, J.G., Snell, J.L., Knapp, A.W.: Denumerable Markov Chains. D. Van Nostrand Company, Princeton (1966) · Zbl 0149.13301
[34] Kozen, D.: Results on the propositional \[ \mu \] -calculus. TCS 27, 333–354 (1983) · Zbl 0553.03007 · doi:10.1016/0304-3975(82)90125-6
[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 · Zbl 05940745 · doi:10.1007/978-3-642-22110-1_47
[36] Ludwig, W.: A subexponential randomized algorithm for the simple stochastic game problem. Inf. Comput. 117(1), 151–155 (1995) · Zbl 0827.90141 · doi:10.1006/inco.1995.1035
[37] McNaughton, R.: Infinite games played on finite graphs. Ann. Pure Appl. Logic 65(2), 149–184 (1993) · Zbl 0798.90151 · doi:10.1016/0168-0072(93)90036-D
[38] Obdržálek, J.: Fast mu-calculus model checking when tree-width is bounded. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 80–92. Springer, Heidelberg (2003). doi: 10.1007/978-3-540-45069-6_7 · Zbl 1278.68188 · doi:10.1007/978-3-540-45069-6_7
[39] Piterman, N.: From nondeterministic Büchi, Streett automata to deterministic parity automata. J. Log. Methods Comput. Sci. 3(3:5), 1–21 (2007) · Zbl 1125.68067
[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 · Zbl 1156.68478 · doi:10.1007/978-3-540-87531-4_27
[42] Schewe, S.: Solving parity games in big steps. J. Comput. Syst. Sci. 84, 243–262 (2017) · Zbl 1353.68180 · doi:10.1016/j.jcss.2016.10.002
[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 · Zbl 1225.68124 · doi:10.1007/11874683_39
[44] Schewe, S., Finkbeiner, B.: Synthesis of asynchronous systems. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 127–142. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-71410-1_10 · Zbl 1196.68142 · doi:10.1007/978-3-540-71410-1_10
[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 · Zbl 1440.91005 · 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 · Zbl 0909.03019 · doi:10.1007/BFb0055090
[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 · Zbl 0974.68527 · doi:10.1007/10722167_18
[48] Wilke, T.: Alternating tree automata, parity games, and modal \[ \mu \] -calculus. Bull. Soc. Math. Belg. 8(2), 359 (2001) · Zbl 0994.68079
[49] Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. TCS 200(1–2), 135–183 (1998) · Zbl 0915.68120 · doi:10.1016/S0304-3975(98)00009-7
[50] Zielonka, W.: Perfect-information stochastic parity games. In: Walukiewicz, I. (ed.) FoSSaCS 2004. LNCS, vol. 2987, pp. 499–513. Springer, Heidelberg (2004). doi: 10.1007/978-3-540-24727-2_35 · Zbl 1126.68489 · doi:10.1007/978-3-540-24727-2_35
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.