2882:
20:
1106:
661:
1101:{\displaystyle {\begin{aligned}Attr_{i}(U)^{0}&:=U\\Attr_{i}(U)^{j+1}&:=Attr_{i}(U)^{j}\cup \{v\in V_{i}\mid \exists (v,w)\in E:w\in Attr_{i}(U)^{j}\}\cup \{v\in V_{1-i}\mid \forall (v,w)\in E:w\in Attr_{i}(U)^{j}\}\\Attr_{i}(U)&:=\bigcup _{j=0}^{\infty }Attr_{i}(U)^{j}\end{aligned}}}
46:
The winner of a finite play is the player whose opponent is unable to move. The winner of an infinite play is determined by the priorities appearing in the play. Typically, player 0 wins an infinite play if the largest priority that occurs infinitely often in the play is even. Player 1 wins
39:. Two players, 0 and 1, move a (single, shared) token along the edges of the graph. The owner of the node that the token falls on selects the successor node (does the next move). The players keep moving the token, resulting in a (possibly infinite)
2846:
Parity is the special case where every vertex has a single color. Specifically, in the above bipartite graph scenario, the problem now is to determine if there is a choice function selecting a single out-going edge from each vertex of
96:
Moreover, parity games are history-free determined. This means that if a player has a winning strategy then that player has a winning strategy that depends only on the current board position, and not on the history of the play.
2798:
2706:
1280:
Zielonka's algorithm is based on a recursive descent on the number of priorities. If the maximal priority is 0, it is immediate to see that player 0 wins the whole game (with an arbitrary strategy). Otherwise, let
2446:
2020:
666:
2124:
482:
147:
Given that parity games are history-free determined, solving a given parity game is equivalent to solving the following simple looking graph-theoretic problem. Given a finite colored directed
23:
A parity game. Circular nodes belong to player 0, rectangular nodes belong to player 1. On the left side is the winning region of player 0, on the right side is the winning region of player 1.
2628:
1927:
316:
1968:
1564:
1372:
2063:
2889:
Despite its interesting complexity theoretic status, parity game solving can be seen as the algorithmic backend to problems in automated verification and controller synthesis. The
2556:
1483:
448:
2269:
2493:
124:
a parity game played on a finite graph means deciding, for a given starting position, which of the two players has a winning strategy. It has been shown that this problem is in
1171:
416:
199:
2318:
1275:
1223:
2368:
1319:
1842:
1802:
1740:
1600:
1427:
511:
1693:
653:
596:
2177:
1633:
1512:
543:
370:
343:
238:
2212:
1766:
1663:
3083:
3121:
115:
3196:
2973:
and C. S. Jutla: Tree
Automata, Mu-Calculus and Determinacy, IEEE Proc. Foundations of Computer Science, pp 368–377 (1991),
3105:
2713:
2897:
for instance is known to be equivalent to parity game solving. Also, decision problems like validity or satisfiability for
3066:
2632:
2372:
453:
3186:
3144:
2978:
251:
2815:, and thus every vertex is colored by a set of colors instead of a single color. Accordingly, we say a vertex
1324:
2873:
Note that as opposed to parity games, this game is no longer symmetric with respect to players 0 and 1.
2560:
2068:
1859:
240:, such that the resulting subgraph has the property that in each cycle the largest occurring color is even.
3191:
2855:
2500:
421:
2807:
A slight modification of the above game, and the related graph-theoretic problem, makes solving the game
2219:
1973:
1118:
375:
158:
90:
70:
1936:
2287:
1517:
1451:
1228:
1176:
2322:
1288:
2453:
2025:
1381:
490:
613:
556:
2141:
1811:
1771:
1709:
1569:
1605:
3001:"Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees"
1668:
1225:) with a single edge and all nodes belonging to player 1 that must reach the previous set (
516:
348:
321:
216:
137:
66:
3033:
2989:
A. Mostowski: Games with forbidden positions, University of Gdansk, Tech. Report 78 (1991)
8:
3151:
Infinite games on finitely coloured graphs with applications to automata on infinite tree
2191:
1745:
1642:
40:
2894:
1492:
35:, where each node has been colored by a priority – one of (usually) finitely many
3115:
2950:
2854:, such that the resulting subgraph has the property that in each cycle (and hence each
3064:
3052:
3017:
3000:
2919:: Borel determinacy, The Annals of Mathematics, Vol 102 No. 2 pp. 363–371 (1975)
3140:
3101:
2974:
78:
3048:
3012:
2942:
2916:
213:, is there a choice function selecting a single out-going edge from each vertex of
62:
3065:
Calude, Cristian S; Jain, Sanjay; Khoussainov, Bakhadyr; Li, Wei; Stephan, Frank,
2930:
2812:
148:
133:
125:
51:
36:
3093:
2890:
2881:
141:
32:
3166:
3180:
3085:
2970:
19:
1173:) one adds all nodes belonging to player 0 that can reach the previous set (
140:). It remains an open question whether this decision problem is solvable in
104:
3089:
2898:
86:
55:
2954:
2130:
2931:"Decidability of second-order theories and automata on infinite trees"
248:
Zielonka outlined a recursive algorithm that solves parity games. Let
3162:
Two state-of-the-art parity game solving toolsets are the following:
2946:
3171:
1970:. We again solve it by recursion and obtain a pair of winning sets
93:
leads to a relatively simple proof of determinacy of parity games.
2808:
487:
Zielonka's algorithm is based on the notation of attractors. Let
243:
2301:
1302:
129:
2802:
2831:. An infinite play is winning for player 0 if there exists
2876:
2835:
such that infinitely many vertices in the play have color
47:
otherwise. This explains the word "parity" in the title.
2793:{\displaystyle W_{i},W_{1-i}:=W_{i}'',W_{1-i}''\cup B}
61:
Games related to parity games were implicitly used in
3034:"Deciding the winner in parity games is in UP∩ co-UP"
2716:
2635:
2563:
2503:
2456:
2375:
2325:
2290:
2222:
2194:
2144:
2071:
2028:
1976:
1939:
1862:
1814:
1774:
1748:
1712:
1671:
1645:
1608:
1572:
1520:
1495:
1454:
1384:
1327:
1291:
1231:
1179:
1121:
664:
616:
559:
519:
493:
456:
424:
378:
372:
are the sets of nodes belonging to player 0 resp. 1,
351:
324:
254:
219:
161:
2701:{\displaystyle W_{0}'',W_{1}'':=solve(G\setminus B)}
106:
2792:
2700:
2622:
2550:
2487:
2441:{\displaystyle W_{0}',W_{1}':=solve(G\setminus A)}
2440:
2362:
2312:
2263:
2206:
2171:
2118:
2057:
2014:
1962:
1921:
1836:
1796:
1760:
1734:
1687:
1657:
1627:
1594:
1558:
1506:
1477:
1421:
1366:
1313:
1269:
1217:
1165:
1100:
647:
590:
537:
505:
476:
442:
410:
364:
337:
310:
232:
193:
3031:
2935:Transactions of the American Mathematical Society
477:{\displaystyle \Omega :V\rightarrow \mathbb {N} }
3178:
2885:Most common applications of parity game solving.
1856:-attractor). We therefore compute the attractor
1742:is not empty, we only know for sure that player
1321:be the player associated with the priority. Let
1111:In other words, one starts with the initial set
655:. It can be defined by a fix-point computation:
3067:"Deciding parity games in quasipolynomial time"
1514:by recursion and obtain a pair of winning sets
1489:are removed. We can now solve the smaller game
112:Can parity games be solved in polynomial time?
3135:E. Grädel, W. Thomas, T. Wilke (Eds.) :
3120:: CS1 maint: multiple names: authors list (
2545:
2542:
2482:
2479:
2258:
2255:
2133:, the algorithm might be expressed as this:
1361:
1334:
996:
900:
894:
804:
244:Recursive algorithm for solving parity games
116:(more unsolved problems in computer science)
16:Mathematical game played on a directed graph
1437:can now ensure that every play that visits
311:{\displaystyle G=(V,V_{0},V_{1},E,\Omega )}
50:Parity games lie in the third level of the
3016:
2803:Related games and their decision problems
1485:in which all nodes and affected edges of
1429:be the corresponding attractor of player
470:
3098:Finite model theory and its applications
2998:
2880:
1367:{\displaystyle U=\{v\mid \Omega (v)=p\}}
18:
2941:. American Mathematical Society: 1–35.
2901:can be reduced to parity game solving.
2877:Relation with logic and automata theory
2623:{\displaystyle B:=Attr_{1-i}(W_{1-i}')}
2119:{\displaystyle W_{1-i}=W''_{1-i}\cup B}
1699:which also results in a win for player
1277:) no matter which edge player 1 takes.
3179:
3096:, Yde Venema, Scott Weinstein (2007).
2858:) it is the case that there exists an
1922:{\displaystyle B=Attr_{1-i}(W'_{1-i})}
2928:
2551:{\displaystyle W_{i},W_{1-i}:=V,\{\}}
484:is the priority assignment function.
3137:Automata, Logics, and Infinite Games
2966:
2964:
443:{\displaystyle E\subseteq V\times V}
107:Unsolved problem in computer science
3084:Erich Grädel, Phokion G. Kolaitis,
2264:{\displaystyle W_{0},W_{1}:=V,\{\}}
13:
3129:
1441:infinitely often is won by player
1374:be the set of nodes with priority
1343:
1054:
928:
826:
457:
302:
14:
3208:
3157:
2992:
2961:
2689:
2429:
2015:{\displaystyle W''_{i},W''_{1-i}}
1954:
1469:
1166:{\displaystyle Attr_{i}(U)^{j+1}}
411:{\displaystyle V=V_{0}\cup V_{1}}
194:{\displaystyle V=V_{0}\cup V_{1}}
100:
3197:Quasi-polynomial time algorithms
1963:{\displaystyle G''=G\setminus B}
2866:, and no node with color 2
2839:, yet finitely many have color
2313:{\displaystyle i:=p{\bmod {2}}}
1665:can only decide to escape from
1559:{\displaystyle W'_{i},W'_{1-i}}
1478:{\displaystyle G'=G\setminus A}
1270:{\displaystyle Attr_{i}(U)^{j}}
1218:{\displaystyle Attr_{i}(U)^{j}}
450:is the total set of edges, and
3058:
3041:Information Processing Letters
3025:
2983:
2922:
2910:
2695:
2683:
2617:
2595:
2435:
2423:
2363:{\displaystyle A:=Attr_{i}(U)}
2357:
2351:
2166:
2160:
1916:
1894:
1416:
1410:
1352:
1346:
1314:{\displaystyle i=p{\bmod {2}}}
1258:
1251:
1206:
1199:
1148:
1141:
1085:
1078:
1028:
1022:
987:
980:
943:
931:
885:
878:
841:
829:
792:
785:
744:
737:
695:
688:
642:
636:
585:
579:
466:
305:
261:
89:of such games was proven. The
1:
3153:, TCS, 200(1-2):135-183, 1998
3139:, Springer LNCS 2500 (2003),
3053:10.1016/S0020-0190(98)00150-1
3018:10.1016/S0304-3975(98)00009-7
2904:
2488:{\displaystyle W_{1-i}'=\{\}}
2182: := maximal priority in
2058:{\displaystyle W_{i}=W''_{i}}
1422:{\displaystyle A=Attr_{i}(U)}
136:and co-UP, as well as in QP (
2862:and a node with color 2
2856:strongly connected component
2827:belongs to the color set of
2811:. The modified game has the
506:{\displaystyle U\subseteq V}
91:Knaster–Tarski theorem
7:
1933:to obtain the smaller game
1285:be the largest one and let
648:{\displaystyle Attr_{i}(U)}
591:{\displaystyle Attr_{i}(U)}
10:
3213:
3032:Marcin Jurdziński (1998),
2813:Rabin acceptance condition
553:is the least set of nodes
418:is the set of all nodes,
205:colored with colors from
3187:Game theory game classes
3047:(3), Elsevier: 119–124,
2172:{\displaystyle solve(G)}
1837:{\displaystyle W'_{1-i}}
1797:{\displaystyle W'_{1-i}}
1735:{\displaystyle W'_{1-i}}
1595:{\displaystyle W'_{1-i}}
318:be a parity game, where
1628:{\displaystyle W_{1-i}}
1115:. Then, for each step (
54:, and are consequently
31:is played on a colored
2886:
2794:
2702:
2624:
2552:
2489:
2442:
2364:
2314:
2265:
2208:
2173:
2120:
2059:
2016:
1964:
1923:
1838:
1798:
1762:
1736:
1689:
1688:{\displaystyle W_{i}'}
1659:
1629:
1596:
1560:
1508:
1479:
1423:
1368:
1315:
1271:
1219:
1167:
1102:
1058:
649:
592:
539:
513:be a set of nodes and
507:
478:
444:
412:
366:
339:
312:
234:
195:
24:
2929:Rabin, M. O. (1969).
2884:
2795:
2703:
2625:
2553:
2490:
2443:
2365:
2315:
2266:
2209:
2174:
2121:
2060:
2017:
1965:
1924:
1839:
1799:
1763:
1737:
1690:
1660:
1630:
1602:is empty, then so is
1597:
1561:
1509:
1480:
1424:
1369:
1316:
1272:
1220:
1168:
1103:
1038:
650:
606:can force a visit to
593:
540:
538:{\displaystyle i=0,1}
508:
479:
445:
413:
367:
365:{\displaystyle V_{1}}
340:
338:{\displaystyle V_{0}}
313:
235:
233:{\displaystyle V_{0}}
196:
22:
2999:Zielonka, W (1998).
2714:
2633:
2561:
2501:
2454:
2373:
2323:
2288:
2220:
2192:
2142:
2069:
2026:
1974:
1937:
1860:
1812:
1772:
1746:
1710:
1669:
1643:
1606:
1570:
1518:
1493:
1452:
1382:
1325:
1289:
1229:
1177:
1119:
662:
614:
557:
517:
491:
454:
422:
376:
349:
322:
252:
217:
159:
138:quasipolynomial time
71:monadic second-order
3192:Finite model theory
3167:PGSolver Collection
3149:W. Zielonka :
2783:
2761:
2664:
2648:
2616:
2475:
2404:
2388:
2207:{\displaystyle p=0}
2109:
2054:
2011:
1989:
1929:and remove it from
1915:
1833:
1808:cannot escape from
1793:
1761:{\displaystyle 1-i}
1731:
1684:
1658:{\displaystyle 1-i}
1591:
1555:
1533:
610:from every node in
3005:Theor. Comput. Sci
2887:
2870: + 1...
2790:
2765:
2749:
2698:
2652:
2636:
2620:
2598:
2548:
2485:
2457:
2438:
2392:
2376:
2360:
2310:
2277: := nodes in
2261:
2204:
2169:
2116:
2091:
2055:
2042:
2022:. It follows that
2012:
1993:
1977:
1960:
1919:
1897:
1834:
1815:
1794:
1775:
1758:
1732:
1713:
1685:
1672:
1655:
1625:
1592:
1573:
1556:
1537:
1521:
1507:{\displaystyle G'}
1504:
1475:
1448:Consider the game
1419:
1364:
1311:
1267:
1215:
1163:
1098:
1096:
645:
588:
535:
503:
474:
440:
408:
362:
335:
308:
230:
191:
25:
3107:978-3-540-00428-8
1639:, because player
545:be a player. The
132:, more precisely
43:, called a play.
3204:
3125:
3119:
3111:
3088:, Maarten Marx,
3077:
3076:
3071:
3062:
3056:
3055:
3038:
3029:
3023:
3022:
3020:
3011:(1–2): 135–183.
2996:
2990:
2987:
2981:
2968:
2959:
2958:
2926:
2920:
2914:
2895:modal μ-calculus
2893:problem for the
2799:
2797:
2796:
2791:
2779:
2757:
2745:
2744:
2726:
2725:
2707:
2705:
2704:
2699:
2660:
2644:
2629:
2627:
2626:
2621:
2612:
2594:
2593:
2557:
2555:
2554:
2549:
2532:
2531:
2513:
2512:
2494:
2492:
2491:
2486:
2471:
2447:
2445:
2444:
2439:
2400:
2384:
2369:
2367:
2366:
2361:
2350:
2349:
2319:
2317:
2316:
2311:
2309:
2308:
2284:
2280:
2276:
2270:
2268:
2267:
2262:
2245:
2244:
2232:
2231:
2213:
2211:
2210:
2205:
2185:
2181:
2178:
2176:
2175:
2170:
2125:
2123:
2122:
2117:
2105:
2087:
2086:
2064:
2062:
2061:
2056:
2050:
2038:
2037:
2021:
2019:
2018:
2013:
2007:
1985:
1969:
1967:
1966:
1961:
1947:
1932:
1928:
1926:
1925:
1920:
1911:
1893:
1892:
1855:
1851:
1847:
1843:
1841:
1840:
1835:
1829:
1807:
1803:
1801:
1800:
1795:
1789:
1767:
1765:
1764:
1759:
1741:
1739:
1738:
1733:
1727:
1702:
1698:
1694:
1692:
1691:
1686:
1680:
1664:
1662:
1661:
1656:
1638:
1634:
1632:
1631:
1626:
1624:
1623:
1601:
1599:
1598:
1593:
1587:
1565:
1563:
1562:
1557:
1551:
1529:
1513:
1511:
1510:
1505:
1503:
1488:
1484:
1482:
1481:
1476:
1462:
1444:
1440:
1436:
1432:
1428:
1426:
1425:
1420:
1409:
1408:
1377:
1373:
1371:
1370:
1365:
1320:
1318:
1317:
1312:
1310:
1309:
1284:
1276:
1274:
1273:
1268:
1266:
1265:
1250:
1249:
1224:
1222:
1221:
1216:
1214:
1213:
1198:
1197:
1172:
1170:
1169:
1164:
1162:
1161:
1140:
1139:
1114:
1107:
1105:
1104:
1099:
1097:
1093:
1092:
1077:
1076:
1057:
1052:
1021:
1020:
995:
994:
979:
978:
924:
923:
893:
892:
877:
876:
822:
821:
800:
799:
784:
783:
758:
757:
736:
735:
703:
702:
687:
686:
654:
652:
651:
646:
635:
634:
609:
605:
601:
597:
595:
594:
589:
578:
577:
552:
548:
544:
542:
541:
536:
512:
510:
509:
504:
483:
481:
480:
475:
473:
449:
447:
446:
441:
417:
415:
414:
409:
407:
406:
394:
393:
371:
369:
368:
363:
361:
360:
344:
342:
341:
336:
334:
333:
317:
315:
314:
309:
292:
291:
279:
278:
239:
237:
236:
231:
229:
228:
200:
198:
197:
192:
190:
189:
177:
176:
108:
3212:
3211:
3207:
3206:
3205:
3203:
3202:
3201:
3177:
3176:
3160:
3132:
3130:Further reading
3113:
3112:
3108:
3080:
3069:
3063:
3059:
3036:
3030:
3026:
2997:
2993:
2988:
2984:
2969:
2962:
2947:10.2307/1995086
2927:
2923:
2915:
2911:
2907:
2879:
2853:
2805:
2800:
2769:
2753:
2734:
2730:
2721:
2717:
2715:
2712:
2711:
2656:
2640:
2634:
2631:
2630:
2602:
2583:
2579:
2562:
2559:
2558:
2521:
2517:
2508:
2504:
2502:
2499:
2498:
2461:
2455:
2452:
2451:
2396:
2380:
2374:
2371:
2370:
2345:
2341:
2324:
2321:
2320:
2304:
2300:
2289:
2286:
2285:
2282:
2278:
2274:
2240:
2236:
2227:
2223:
2221:
2218:
2217:
2193:
2190:
2189:
2183:
2179:
2143:
2140:
2139:
2095:
2076:
2072:
2070:
2067:
2066:
2046:
2033:
2029:
2027:
2024:
2023:
1997:
1981:
1975:
1972:
1971:
1940:
1938:
1935:
1934:
1930:
1901:
1882:
1878:
1861:
1858:
1857:
1853:
1849:
1845:
1819:
1813:
1810:
1809:
1805:
1779:
1773:
1770:
1769:
1747:
1744:
1743:
1717:
1711:
1708:
1707:
1700:
1696:
1676:
1670:
1667:
1666:
1644:
1641:
1640:
1636:
1613:
1609:
1607:
1604:
1603:
1577:
1571:
1568:
1567:
1541:
1525:
1519:
1516:
1515:
1496:
1494:
1491:
1490:
1486:
1455:
1453:
1450:
1449:
1442:
1438:
1434:
1430:
1404:
1400:
1383:
1380:
1379:
1375:
1326:
1323:
1322:
1305:
1301:
1290:
1287:
1286:
1282:
1261:
1257:
1245:
1241:
1230:
1227:
1226:
1209:
1205:
1193:
1189:
1178:
1175:
1174:
1151:
1147:
1135:
1131:
1120:
1117:
1116:
1112:
1095:
1094:
1088:
1084:
1072:
1068:
1053:
1042:
1031:
1016:
1012:
1000:
999:
990:
986:
974:
970:
913:
909:
888:
884:
872:
868:
817:
813:
795:
791:
779:
775:
759:
747:
743:
731:
727:
715:
714:
704:
698:
694:
682:
678:
665:
663:
660:
659:
630:
626:
615:
612:
611:
607:
603:
599:
573:
569:
558:
555:
554:
550:
546:
518:
515:
514:
492:
489:
488:
469:
455:
452:
451:
423:
420:
419:
402:
398:
389:
385:
377:
374:
373:
356:
352:
350:
347:
346:
329:
325:
323:
320:
319:
287:
283:
274:
270:
253:
250:
249:
246:
224:
220:
218:
215:
214:
185:
181:
172:
168:
160:
157:
156:
149:bipartite graph
119:
118:
113:
110:
103:
52:Borel hierarchy
37:natural numbers
17:
12:
11:
5:
3210:
3200:
3199:
3194:
3189:
3175:
3174:
3169:
3159:
3158:External links
3156:
3155:
3154:
3147:
3131:
3128:
3127:
3126:
3106:
3094:Moshe Y. Vardi
3079:
3078:
3057:
3024:
2991:
2982:
2960:
2921:
2908:
2906:
2903:
2891:model-checking
2878:
2875:
2851:
2804:
2801:
2789:
2786:
2782:
2778:
2775:
2772:
2768:
2764:
2760:
2756:
2752:
2748:
2743:
2740:
2737:
2733:
2729:
2724:
2720:
2697:
2694:
2691:
2688:
2685:
2682:
2679:
2676:
2673:
2670:
2667:
2663:
2659:
2655:
2651:
2647:
2643:
2639:
2619:
2615:
2611:
2608:
2605:
2601:
2597:
2592:
2589:
2586:
2582:
2578:
2575:
2572:
2569:
2566:
2547:
2544:
2541:
2538:
2535:
2530:
2527:
2524:
2520:
2516:
2511:
2507:
2484:
2481:
2478:
2474:
2470:
2467:
2464:
2460:
2437:
2434:
2431:
2428:
2425:
2422:
2419:
2416:
2413:
2410:
2407:
2403:
2399:
2395:
2391:
2387:
2383:
2379:
2359:
2356:
2353:
2348:
2344:
2340:
2337:
2334:
2331:
2328:
2307:
2303:
2299:
2296:
2293:
2281:with priority
2260:
2257:
2254:
2251:
2248:
2243:
2239:
2235:
2230:
2226:
2203:
2200:
2197:
2168:
2165:
2162:
2159:
2156:
2153:
2150:
2147:
2135:
2115:
2112:
2108:
2104:
2101:
2098:
2094:
2090:
2085:
2082:
2079:
2075:
2053:
2049:
2045:
2041:
2036:
2032:
2010:
2006:
2003:
2000:
1996:
1992:
1988:
1984:
1980:
1959:
1956:
1953:
1950:
1946:
1943:
1918:
1914:
1910:
1907:
1904:
1900:
1896:
1891:
1888:
1885:
1881:
1877:
1874:
1871:
1868:
1865:
1832:
1828:
1825:
1822:
1818:
1792:
1788:
1785:
1782:
1778:
1757:
1754:
1751:
1730:
1726:
1723:
1720:
1716:
1706:Otherwise, if
1683:
1679:
1675:
1654:
1651:
1648:
1622:
1619:
1616:
1612:
1590:
1586:
1583:
1580:
1576:
1554:
1550:
1547:
1544:
1540:
1536:
1532:
1528:
1524:
1502:
1499:
1474:
1471:
1468:
1465:
1461:
1458:
1418:
1415:
1412:
1407:
1403:
1399:
1396:
1393:
1390:
1387:
1363:
1360:
1357:
1354:
1351:
1348:
1345:
1342:
1339:
1336:
1333:
1330:
1308:
1304:
1300:
1297:
1294:
1264:
1260:
1256:
1253:
1248:
1244:
1240:
1237:
1234:
1212:
1208:
1204:
1201:
1196:
1192:
1188:
1185:
1182:
1160:
1157:
1154:
1150:
1146:
1143:
1138:
1134:
1130:
1127:
1124:
1109:
1108:
1091:
1087:
1083:
1080:
1075:
1071:
1067:
1064:
1061:
1056:
1051:
1048:
1045:
1041:
1037:
1034:
1032:
1030:
1027:
1024:
1019:
1015:
1011:
1008:
1005:
1002:
1001:
998:
993:
989:
985:
982:
977:
973:
969:
966:
963:
960:
957:
954:
951:
948:
945:
942:
939:
936:
933:
930:
927:
922:
919:
916:
912:
908:
905:
902:
899:
896:
891:
887:
883:
880:
875:
871:
867:
864:
861:
858:
855:
852:
849:
846:
843:
840:
837:
834:
831:
828:
825:
820:
816:
812:
809:
806:
803:
798:
794:
790:
787:
782:
778:
774:
771:
768:
765:
762:
760:
756:
753:
750:
746:
742:
739:
734:
730:
726:
723:
720:
717:
716:
713:
710:
707:
705:
701:
697:
693:
690:
685:
681:
677:
674:
671:
668:
667:
644:
641:
638:
633:
629:
625:
622:
619:
587:
584:
581:
576:
572:
568:
565:
562:
549:-attractor of
534:
531:
528:
525:
522:
502:
499:
496:
472:
468:
465:
462:
459:
439:
436:
433:
430:
427:
405:
401:
397:
392:
388:
384:
381:
359:
355:
332:
328:
307:
304:
301:
298:
295:
290:
286:
282:
277:
273:
269:
266:
263:
260:
257:
245:
242:
227:
223:
188:
184:
180:
175:
171:
167:
164:
114:
111:
105:
102:
101:Solving a game
99:
33:directed graph
15:
9:
6:
4:
3:
2:
3209:
3198:
3195:
3193:
3190:
3188:
3185:
3184:
3182:
3173:
3170:
3168:
3165:
3164:
3163:
3152:
3148:
3146:
3145:3-540-00388-6
3142:
3138:
3134:
3133:
3123:
3117:
3109:
3103:
3099:
3095:
3091:
3087:
3086:Leonid Libkin
3082:
3081:
3075:
3068:
3061:
3054:
3050:
3046:
3042:
3035:
3028:
3019:
3014:
3010:
3006:
3002:
2995:
2986:
2980:
2979:0-8186-2445-0
2976:
2972:
2971:E. A. Emerson
2967:
2965:
2956:
2952:
2948:
2944:
2940:
2936:
2932:
2925:
2918:
2913:
2909:
2902:
2900:
2896:
2892:
2883:
2874:
2871:
2869:
2865:
2861:
2857:
2850:
2844:
2842:
2838:
2834:
2830:
2826:
2823:if the color
2822:
2818:
2814:
2810:
2787:
2784:
2780:
2776:
2773:
2770:
2766:
2762:
2758:
2754:
2750:
2746:
2741:
2738:
2735:
2731:
2727:
2722:
2718:
2710:
2692:
2686:
2680:
2677:
2674:
2671:
2668:
2665:
2661:
2657:
2653:
2649:
2645:
2641:
2637:
2613:
2609:
2606:
2603:
2599:
2590:
2587:
2584:
2580:
2576:
2573:
2570:
2567:
2564:
2539:
2536:
2533:
2528:
2525:
2522:
2518:
2514:
2509:
2505:
2497:
2476:
2472:
2468:
2465:
2462:
2458:
2450:
2432:
2426:
2420:
2417:
2414:
2411:
2408:
2405:
2401:
2397:
2393:
2389:
2385:
2381:
2377:
2354:
2346:
2342:
2338:
2335:
2332:
2329:
2326:
2305:
2297:
2294:
2291:
2273:
2252:
2249:
2246:
2241:
2237:
2233:
2228:
2224:
2216:
2201:
2198:
2195:
2188:
2163:
2157:
2154:
2151:
2148:
2145:
2138:
2134:
2132:
2127:
2113:
2110:
2106:
2102:
2099:
2096:
2092:
2088:
2083:
2080:
2077:
2073:
2051:
2047:
2043:
2039:
2034:
2030:
2008:
2004:
2001:
1998:
1994:
1990:
1986:
1982:
1978:
1957:
1951:
1948:
1944:
1941:
1912:
1908:
1905:
1902:
1898:
1889:
1886:
1883:
1879:
1875:
1872:
1869:
1866:
1863:
1830:
1826:
1823:
1820:
1816:
1790:
1786:
1783:
1780:
1776:
1755:
1752:
1749:
1728:
1724:
1721:
1718:
1714:
1704:
1681:
1677:
1673:
1652:
1649:
1646:
1635:for the game
1620:
1617:
1614:
1610:
1588:
1584:
1581:
1578:
1574:
1552:
1548:
1545:
1542:
1538:
1534:
1530:
1526:
1522:
1500:
1497:
1472:
1466:
1463:
1459:
1456:
1446:
1413:
1405:
1401:
1397:
1394:
1391:
1388:
1385:
1358:
1355:
1349:
1340:
1337:
1331:
1328:
1306:
1298:
1295:
1292:
1278:
1262:
1254:
1246:
1242:
1238:
1235:
1232:
1210:
1202:
1194:
1190:
1186:
1183:
1180:
1158:
1155:
1152:
1144:
1136:
1132:
1128:
1125:
1122:
1089:
1081:
1073:
1069:
1065:
1062:
1059:
1049:
1046:
1043:
1039:
1035:
1033:
1025:
1017:
1013:
1009:
1006:
1003:
991:
983:
975:
971:
967:
964:
961:
958:
955:
952:
949:
946:
940:
937:
934:
925:
920:
917:
914:
910:
906:
903:
897:
889:
881:
873:
869:
865:
862:
859:
856:
853:
850:
847:
844:
838:
835:
832:
823:
818:
814:
810:
807:
801:
796:
788:
780:
776:
772:
769:
766:
763:
761:
754:
751:
748:
740:
732:
728:
724:
721:
718:
711:
708:
706:
699:
691:
683:
679:
675:
672:
669:
658:
657:
656:
639:
631:
627:
623:
620:
617:
582:
574:
570:
566:
563:
560:
532:
529:
526:
523:
520:
500:
497:
494:
485:
463:
460:
437:
434:
431:
428:
425:
403:
399:
395:
390:
386:
382:
379:
357:
353:
330:
326:
299:
296:
293:
288:
284:
280:
275:
271:
267:
264:
258:
255:
241:
225:
221:
212:
208:
204:
186:
182:
178:
173:
169:
165:
162:
154:
150:
145:
143:
139:
135:
131:
127:
123:
117:
98:
94:
92:
88:
84:
80:
76:
72:
68:
64:
59:
57:
53:
48:
44:
42:
38:
34:
30:
21:
3161:
3150:
3136:
3100:. Springer.
3097:
3090:Joel Spencer
3073:
3060:
3044:
3040:
3027:
3008:
3004:
2994:
2985:
2938:
2934:
2924:
2917:D. A. Martin
2912:
2899:modal logics
2888:
2872:
2867:
2863:
2859:
2848:
2845:
2840:
2836:
2832:
2828:
2824:
2820:
2816:
2806:
2708:
2495:
2448:
2271:
2214:
2186:
2136:
2128:
1705:
1447:
1279:
1110:
486:
247:
210:
206:
202:
152:
146:
121:
120:
95:
85:= 2), where
82:
77:successors (
74:
67:decidability
65:'s proof of
60:
49:
45:
28:
26:
1768:can win on
598:containing
87:determinacy
29:parity game
3181:Categories
2905:References
2819:has color
2131:pseudocode
2129:In simple
1804:as player
602:such that
73:theory of
56:determined
3116:cite book
3074:Stoc 2017
2785:∪
2774:−
2739:−
2690:∖
2607:−
2588:−
2526:−
2466:−
2430:∖
2111:∪
2100:−
2081:−
2002:−
1955:∖
1906:−
1887:−
1824:−
1784:−
1753:−
1722:−
1650:−
1618:−
1582:−
1546:−
1470:∖
1433:. Player
1344:Ω
1341:∣
1055:∞
1040:⋃
959:∈
947:∈
929:∀
926:∣
918:−
907:∈
898:∪
857:∈
845:∈
827:∃
824:∣
811:∈
802:∪
498:⊆
467:→
458:Ω
435:×
429:⊆
396:∪
303:Ω
179:∪
155:vertices
2781:″
2759:″
2662:″
2646:″
2614:′
2473:′
2402:′
2386:′
2137:function
2107:″
2052:″
2009:″
1987:″
1945:″
1913:′
1831:′
1791:′
1729:′
1682:′
1589:′
1553:′
1531:′
1501:′
1460:′
1378:and let
2955:1995086
2809:NP-hard
1848:(since
122:Solving
69:of the
3143:
3104:
2977:
2953:
2709:return
2496:return
2215:return
1852:is an
345:resp.
201:, and
3070:(PDF)
3037:(PDF)
2951:JSTOR
1566:. If
151:with
142:PTime
130:co-NP
63:Rabin
3172:Oink
3141:ISBN
3122:link
3102:ISBN
2975:ISBN
2841:2i+1
2272:else
2065:and
128:and
81:for
41:path
3049:doi
3013:doi
3009:200
2943:doi
2939:141
2302:mod
1844:to
1695:to
1303:mod
209:to
79:S2S
3183::
3118:}}
3114:{{
3092:,
3072:,
3045:68
3043:,
3039:,
3007:.
3003:.
2963:^
2949:.
2937:.
2933:.
2843:.
2837:2i
2747::=
2666::=
2568::=
2534::=
2449:if
2406::=
2330::=
2295::=
2247::=
2187:if
2126:.
1703:.
1445:.
1036::=
764::=
709::=
144:.
134:UP
126:NP
58:.
27:A
3124:)
3110:.
3051::
3021:.
3015::
2957:.
2945::
2868:i
2864:i
2860:i
2852:0
2849:V
2833:i
2829:v
2825:j
2821:j
2817:v
2788:B
2777:i
2771:1
2767:W
2763:,
2755:i
2751:W
2742:i
2736:1
2732:W
2728:,
2723:i
2719:W
2696:)
2693:B
2687:G
2684:(
2681:e
2678:v
2675:l
2672:o
2669:s
2658:1
2654:W
2650:,
2642:0
2638:W
2618:)
2610:i
2604:1
2600:W
2596:(
2591:i
2585:1
2581:r
2577:t
2574:t
2571:A
2565:B
2546:}
2543:{
2540:,
2537:V
2529:i
2523:1
2519:W
2515:,
2510:i
2506:W
2483:}
2480:{
2477:=
2469:i
2463:1
2459:W
2436:)
2433:A
2427:G
2424:(
2421:e
2418:v
2415:l
2412:o
2409:s
2398:1
2394:W
2390:,
2382:0
2378:W
2358:)
2355:U
2352:(
2347:i
2343:r
2339:t
2336:t
2333:A
2327:A
2306:2
2298:p
2292:i
2283:p
2279:G
2275:U
2259:}
2256:{
2253:,
2250:V
2242:1
2238:W
2234:,
2229:0
2225:W
2202:0
2199:=
2196:p
2184:G
2180:p
2167:)
2164:G
2161:(
2158:e
2155:v
2152:l
2149:o
2146:s
2114:B
2103:i
2097:1
2093:W
2089:=
2084:i
2078:1
2074:W
2048:i
2044:W
2040:=
2035:i
2031:W
2005:i
1999:1
1995:W
1991:,
1983:i
1979:W
1958:B
1952:G
1949:=
1942:G
1931:G
1917:)
1909:i
1903:1
1899:W
1895:(
1890:i
1884:1
1880:r
1876:t
1873:t
1870:A
1867:=
1864:B
1854:i
1850:A
1846:A
1827:i
1821:1
1817:W
1806:i
1787:i
1781:1
1777:W
1756:i
1750:1
1725:i
1719:1
1715:W
1701:i
1697:A
1678:i
1674:W
1653:i
1647:1
1637:G
1621:i
1615:1
1611:W
1585:i
1579:1
1575:W
1549:i
1543:1
1539:W
1535:,
1527:i
1523:W
1498:G
1487:A
1473:A
1467:G
1464:=
1457:G
1443:i
1439:A
1435:i
1431:i
1417:)
1414:U
1411:(
1406:i
1402:r
1398:t
1395:t
1392:A
1389:=
1386:A
1376:p
1362:}
1359:p
1356:=
1353:)
1350:v
1347:(
1338:v
1335:{
1332:=
1329:U
1307:2
1299:p
1296:=
1293:i
1283:p
1263:j
1259:)
1255:U
1252:(
1247:i
1243:r
1239:t
1236:t
1233:A
1211:j
1207:)
1203:U
1200:(
1195:i
1191:r
1187:t
1184:t
1181:A
1159:1
1156:+
1153:j
1149:)
1145:U
1142:(
1137:i
1133:r
1129:t
1126:t
1123:A
1113:U
1090:j
1086:)
1082:U
1079:(
1074:i
1070:r
1066:t
1063:t
1060:A
1050:0
1047:=
1044:j
1029:)
1026:U
1023:(
1018:i
1014:r
1010:t
1007:t
1004:A
997:}
992:j
988:)
984:U
981:(
976:i
972:r
968:t
965:t
962:A
956:w
953::
950:E
944:)
941:w
938:,
935:v
932:(
921:i
915:1
911:V
904:v
901:{
895:}
890:j
886:)
882:U
879:(
874:i
870:r
866:t
863:t
860:A
854:w
851::
848:E
842:)
839:w
836:,
833:v
830:(
819:i
815:V
808:v
805:{
797:j
793:)
789:U
786:(
781:i
777:r
773:t
770:t
767:A
755:1
752:+
749:j
745:)
741:U
738:(
733:i
729:r
725:t
722:t
719:A
712:U
700:0
696:)
692:U
689:(
684:i
680:r
676:t
673:t
670:A
643:)
640:U
637:(
632:i
628:r
624:t
621:t
618:A
608:U
604:i
600:U
586:)
583:U
580:(
575:i
571:r
567:t
564:t
561:A
551:U
547:i
533:1
530:,
527:0
524:=
521:i
501:V
495:U
471:N
464:V
461::
438:V
432:V
426:E
404:1
400:V
391:0
387:V
383:=
380:V
358:1
354:V
331:0
327:V
306:)
300:,
297:E
294:,
289:1
285:V
281:,
276:0
272:V
268:,
265:V
262:(
259:=
256:G
226:0
222:V
211:m
207:1
203:V
187:1
183:V
174:0
170:V
166:=
163:V
153:n
109::
83:n
75:n
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
