Academic Articles & Supplements

Synthesizing Controllers for Safety Games under Delayed Information

Mingshuai Chen

Author

Mingshuai Chen

Title

Synthesizing Controllers for Safety Games under Delayed Information

Description

The implementation declares either WINNING associated with a finite-memory winning strategy if the game is controllable, or LOSING otherwise with a delay under which the winning strategy vanishes.

DGame: solving delayed safety games

The tool DGame is dedicated to synthesizing controllers for safety games under delayed information. The key idea of the synthesis procedure is to compute a series of finite-memory winning strategies

while increasing delays from k = 0 to the finally interesting delay k = δ. The algorithm takes as input a delayed two-player safety game

and returns either WINNING associated with a winning strategy (α,

) for the controller if

is controllable, or LOSING otherwise with an integer m indicating that the winning strategy vanishes when lifting delay to m. Current version: v1.0Validated on platform: Mathematica 10, 64bit-Ubuntu-Desktop-14.10/17.04Latest modification: on Jan. 22, 2018, by Mingshuai Chen, SKLCS-ISCASCorresponding e-mail: chenms@ios.ac.cnList of contributors: Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter N. Mosaad, and Naijun ZhanComments and bug-reports are higly appreciated.© 2018 DGame, State Key Lab. of Computer Science, ISCAS. All rights reserved.

Source code

Demonstrative examples

Exmp. 1

(*gamegraph*)g1=Graph[{12,14,23,43,36,38,65,85,710,712,109,129,914,916,1411,1611,54,512,114,1112},EdgeWeight{a,b,u,u,a,b,u,u,b,a,u,u,b,a,u,u,b,a,a,b}];(*initialstate*)init1={1};(*unsafestates*)bad1={2,6,10,14};(*delay*)lag1=5;(*graphicalmode*)graphical1=1;

(*synthesizethestrategy*)main[g1,init1,bad1,lag1,graphical1]

Original graph:

Under delay = 0 :

Under delay = 1 :

Under delay = 2 :

Under delay = 3 :

Under delay = 4 :

Under delay = 5 :

(*Computationtimeisgotunderthetextmode,i.e.withgraphical1=0,asrenderingthegraphsneedsmuchmoreextratime,whichthoughfallsbeyondthealgorithm.*)

Computation time under increasing delays : {0.004,0.004,0.004,0.008,0.008,0.012}

Exmp. 2

g2=Graph[{12,14,23,43,36,38,65,85,710,712,109,129,914,916,1411,1611,54,512,114,1112,83,811},EdgeWeight{a,b,u,u,a,b,u,u,b,a,u,u,b,a,u,u,b,a,a,b,u,u}];init2={1};bad2={2,6,10,14};lag2=4;graphical2=0;

main[g2,init2,bad2,lag2,graphical2]

Under delay = 0 :

{1,{}}{b},{3,{}}{b},{5,{}}{b,a},{7,{}}{a},{9,{}}{a},{11,{}}{a,b}

Under delay = 1 :

{{2,{}}{},{4,{}}{b},{6,{}}{},{8,{}}{b},{10,{}}{},{12,{}}{a},{14,{}}{},{16,{}}{a,b}}

Under delay = 2 :

{{1,{{a}}}{},{1,{{b}}}{b},{3,{{a}}}{},{3,{{b}}}{b},{5,{{b}}}{b},{5,{{a}}}{a},{7,{{b}}}{},{7,{{a}}}{a},{9,{{b}}}{},{9,{{a}}}{a,b},{11,{{a}}}{b},{11,{{b}}}{a}}

Under delay = 3 :

{{2,{{a}}}{},{2,{{b}}}{},{4,{{a}}}{},{4,{{b}}}{},{6,{{b}}}{},{6,{{a}}}{},{8,{{a}}}{},{8,{{b}}}{}}

Not possible for sure-winning anymore under delay=3 with uncontrollable states {4,8,1}.

Computation time under increasing delays : {0.,0.004,0.004,0.008}

Escp. 4 x 4

main[g3,init3,bad3,lag3,graphical3]

Under delay = 0 :

Under delay = 1 :

{{84,{}}{b,e,f,g,h,i},{28,{}}{c,d,i},{50,{}}{g,i},{162,{}}{},{22,{}}{c,d},{134,{}}{a,b},{78,{}}{b,i},{54,{}}{c,g,i},{166,{}}{},{26,{}}{c,d},{138,{}}{a,b},{82,{}}{b,i},{98,{}}{},{70,{}}{e,f,g,h,i},{42,{}}{g},{112,{}}{f},{56,{}}{g,i},{104,{}}{f},{76,{}}{b},{48,{}}{i},{210,{}}{},{182,{}}{f},{154,{}}{e},{224,{}}{},{196,{}}{f},{168,{}}{e},{216,{}}{},{188,{}}{},{160,{}}{},{14,{}}{c,d,i},{20,{}}{},{126,{}}{a,b,i},{140,{}}{a,b,i},{132,{}}{},{108,{}}{f,i},{80,{}}{b},{52,{}}{c,i},{220,{}}{},{192,{}}{},{164,{}}{a},{24,{}}{},{136,{}}{},{148,{}}{e,g,h,i},{92,{}}{},{106,{}}{},{36,{}}{},{8,{}}{c,d},{120,{}}{a,b,c,i},{64,{}}{d,g,h,i},{110,{}}{f,i},{46,{}}{c,i},{158,{}}{},{102,{}}{f,i},{18,{}}{},{130,{}}{},{74,{}}{},{204,{}}{e,f},{218,{}}{},{176,{}}{a,b,f,i},{190,{}}{},{222,{}}{},{194,{}}{},{214,{}}{},{186,{}}{},{90,{}}{h},{202,{}}{e,f,i},{62,{}}{d},{174,{}}{a,b,i},{146,{}}{c,d,g,h,i},{34,{}}{},{6,{}}{},{118,{}}{c},{96,{}}{i},{68,{}}{},{40,{}}{c},{100,{}}{f,i},{72,{}}{b},{44,{}}{c,i},{208,{}}{},{180,{}}{},{152,{}}{a},{212,{}}{},{184,{}}{},{156,{}}{a},{12,{}}{},{16,{}}{},{124,{}}{},{128,{}}{},{32,{}}{},{144,{}}{a,i},{88,{}}{h,i},{200,{}}{e,f},{4,{}}{},{116,{}}{},{60,{}}{},{172,{}}{a,b},{38,{}}{c,i},{150,{}}{a,i},{94,{}}{f,h,i},{10,{}}{},{122,{}}{},{66,{}}{},{206,{}}{e,f},{178,{}}{a,b},{86,{}}{h,i},{58,{}}{d},{30,{}}{c},{198,{}}{e,f,i},{170,{}}{a,b,i},{142,{}}{a,c,d,g,h,i},{2,{}}{},{114,{}}{c}}

Under delay = 2 :

Under delay = 3 :

{{84,{{b}}}{},{84,{{d}}}{},{84,{{e,f}}}{},{84,{{g,h}}}{},{84,{{i}}}{},{28,{{i}}}{},{28,{{c,d}}}{},{50,{{c}}}{},{50,{{g}}}{},{50,{{i}}}{},{162,{{a}}}{},{162,{{e}}}{},{162,{{c,d}}}{},{162,{{g,h}}}{},{162,{{i}}}{},{22,{{c,d}}}{},{22,{{i}}}{},{134,{{a,b}}}{},{134,{{c}}}{},{134,{{i}}}{},{78,{{i}}}{},{78,{{b}}}{},{78,{{d}}}{},{78,{{e,f}}}{},{78,{{g,h}}}{}}

Not possible for sure-winning anymore under delay=3 with uncontrollable states {162,166,210,216,188,20,132,220,24,136,92,106,36,158,18,130,74,218,190,222,194,214,186,6,208,180,212,184,12,16,124,32,4,116,60,10,122,66,84,50,28,22,134,78,27}.

Computation time under increasing delays : {0.084,0.132,0.216,0.248}

Escp. 4 x 5

main[g4,init4,bad4,lag4,graphical4]

Under delay = 0 :

(*hidden for the sake of space*)

Under delay = 1 :

(*hidden for the sake of space*)

Under delay = 2 :

(*hidden for the sake of space*)

Under delay = 3 :

(*hidden for the sake of space*)

Not possible for sure-winning anymore under delay=3 with uncontrollable states {162,170,360,350,314,242,356,320,248,100,88,268,106,286,96,276,24,204,352,340,348,312,30,210,90,152,80,270,260,44,98,288,278,346,130,310,238,22,202,78,6,14,194,20,302,308,40,112,4,184,120,12,192,64,70,244,144,250,28,34,208,214,136,142,134,62,342,36,26,206,35}.

Computation time under increasing delays : {0.18,0.272,0.456,0.628}

Escp. 5 x 5

main[g5,init5,bad5,lag5,graphical5]

Under delay = 0 :

(*hidden for the sake of space*)

Under delay = 1 :

(*hidden for the sake of space*)

Under delay = 2 :

(*hidden for the sake of space*)

Under delay = 3 :

(*hidden for the sake of space*)

Not possible for sure-winning anymore under delay=3 with uncontrollable states {110,340,202,358,118,348,210,302,308,588,450,578,440,596,550,458,584,538,446,492,400,546,408,120,108,338,126,356,116,438,346,392,24,254,30,260,580,568,586,540,576,530,494,484,594,502,582,536,490,100,192,54,298,22,252,160,390,482,500,98,6,14,20,244,474,480,50,4,142,12,242,150,212,82,312,218,90,320,166,172,74,80,72,28,34,26,402,266,274,264,396,258,256,36,174,44,182,184,304,310,46,164,45}.

Computation time under increasing delays : {0.456,0.68,1.164,1.708}

Escp. 5 x 6

main[g6,init6,bad6,lag6,graphical6]

Under delay = 0 :

(*hidden for the sake of space*)

Under delay = 1 :

(*hidden for the sake of space*)

Under delay = 2 :

(*hidden for the sake of space*)

Under delay = 3 :

(*hidden for the sake of space*)

Not possible for sure-winning anymore under delay=3 with uncontrollable states {602,612,134,144,152,488,828,816,824,768,712,834,722,292,124,314,300,244,132,650,482,636,468,322,672,658,490,310,254,142,646,590,478,422,332,668,318,654,598,542,430,840,826,814,836,780,822,766,710,552,776,720,290,312,130,466,298,648,802,634,320,670,656,140,476,308,812,644,756,588,28,364,700,532,820,764,36,372,708,288,232,120,624,64,306,642,194,530,418,26,362,698,118,6,16,352,24,688,696,60,172,4,182,14,350,88,96,424,266,210,546,434,432,276,220,556,444,32,40,368,376,200,208,198,258,202,90,98,108,256,100,436,110,446,426,264,86,594,538,760,704,536,534,34,42,52,30,378,388,44,54,380,390,212,222,224,56,544,370,366,55}.

Computation time under increasing delays : {1.,1.42,2.404,4.304}

Escp. 6 x 6

main[g7,init7,bad7,lag7,graphical7]

Under delay = 0 :

(*hidden for the sake of space*)

Under delay = 1 :

(*hidden for the sake of space*)

Under delay = 2 :

(*hidden for the sake of space*)

Under delay = 3 :

(*hidden for the sake of space*)

Not possible for sure-winning anymore under delay=3 with uncontrollable states {578,586,1008,994,722,1018,1004,936,732,946,158,372,168,780,802,380,176,788,584,1200,1188,1210,1142,1196,1128,992,1060,924,856,1220,1206,1138,1070,866,876,148,352,374,156,564,360,292,382,166,574,370,302,782,804,790,506,710,514,922,718,854,650,932,660,1212,1198,1222,1154,1208,1140,1072,1058,1150,1082,864,1068,874,1078,350,358,154,368,164,640,1048,28,436,844,1056,36,444,852,1066,144,280,76,502,26,434,230,638,842,6,16,24,424,72,4,208,14,422,218,304,170,316,178,326,102,110,510,518,306,314,312,188,336,596,734,744,120,528,324,236,244,100,108,98,712,982,778,986,918,714,644,1120,1052,916,914,32,40,30,652,450,460,926,724,656,858,666,868,676,654,664,448,440,438,34,42,442,238,246,52,256,248,112,258,122,268,132,508,532,542,520,530,124,134,516,540,44,54,64,452,462,56,464,260,66,474,270,272,68,472,234,67}.

Computation time under increasing delays : {2.064,2.904,5.116,10.304}

Escp. 7 x 7

main[g8,init8,bad8,lag8,graphical8]

Under delay = 0 :

(*hidden for the sake of space*)

Under delay = 1 :

(*hidden for the sake of space*)

Under delay = 2 :

(*hidden for the sake of space*)

Under delay = 3 :

(*hidden for the sake of space*)

Not possible for sure-winning anymore under delay=3 with uncontrollable states {1568,1580,1942,308,966,590,992,320,978,884,602,894,1650,1274,1260,1678,1662,1286,1552,1270,1176,1564,1470,1188,1482,2336,1960,2320,1944,2348,2254,1972,2332,2238,1956,1862,1846,2250,2156,1874,2140,1858,2046,1764,2152,2058,1776,322,306,964,212,332,990,600,318,976,224,1648,1676,1660,1750,1374,1386,2322,2306,2334,2240,2318,2224,2346,2330,2236,2142,2048,2126,2032,2060,2138,2044,294,200,576,304,210,868,586,492,880,504,786,1162,796,1454,1172,1078,1466,1090,1372,2030,1748,1384,2042,1760,292,302,208,32,690,42,700,1358,2016,2028,196,478,102,782,30,688,406,1064,6,18,28,676,98,4,380,16,674,392,626,330,1284,922,988,250,896,908,612,1646,1312,1296,1970,1592,1954,1674,1658,2304,1554,1928,2316,2222,1578,1940,1848,1474,1754,2128,2034,1472,1484,1378,1752,1966,2344,2328,1872,2234,358,342,640,624,344,1016,1000,1298,920,1216,1282,1002,638,248,906,610,328,1268,986,262,530,234,1634,1926,1644,1458,2210,1930,1556,1836,2116,1834,1832,1550,1364,2022,1740,1738,1082,1362,370,354,652,636,356,1028,1012,1310,1294,1014,1686,1670,1968,1952,1672,340,998,1938,1656,1576,1200,1590,1562,2292,2132,1742,1850,1180,1460,1756,2130,2302,2208,2114,2038,1366,2036,2020,2314,2220,2340,1964,2342,2246,1870,2248,2326,2232,962,316,974,222,598,1632,1258,1164,1538,1256,506,226,604,240,898,614,252,910,510,520,228,238,236,264,532,132,142,790,800,508,518,516,544,276,934,1190,1202,154,812,412,422,130,140,128,1542,1448,1166,1070,1822,1728,1446,1444,36,46,34,1080,1178,1084,1462,706,718,1096,1368,1380,1486,1392,1376,1108,1766,1498,1404,1390,1094,704,694,692,38,48,696,414,424,60,436,416,426,134,144,438,156,450,168,788,804,816,1192,828,1204,802,814,146,158,522,534,170,546,536,548,560,1194,1206,1218,798,840,826,182,558,40,50,62,74,708,720,52,64,710,722,428,440,76,734,452,442,160,454,172,466,184,66,78,90,1086,1098,1110,1100,818,1112,830,174,832,186,844,1124,842,724,736,80,738,456,470,94,92,750,468,748,732,88,746,464,1122,410,93}.

Computation time under increasing delays : {7.712,10.672,19.044,52.468}

Escp. 7 x 8

main[g9,init9,bad9,lag9,graphical9]

Under delay = 0 :

(*hidden for the sake of space*)

Under delay = 1 :

(*hidden for the sake of space*)

Under delay = 2 :

(*hidden for the sake of space*)

Under delay = 3 :

(*hidden for the sake of space*)

Not possible for sure-winning anymore under delay=3 with uncontrollable states {1570,1584,2466,2448,2016,2480,2462,2354,2030,2368,354,368,380,1244,2108,3008,2990,2972,3004,2896,2986,2878,2446,2892,2784,2676,2690,772,340,802,784,676,352,1666,1234,1216,814,1696,1678,1246,798,690,366,1554,1230,1122,1566,1458,1134,2560,2128,2542,2110,2592,2574,2142,2556,2124,1998,1472,2336,2012,1904,2350,2242,1918,3024,3006,2988,3020,2912,3002,2894,2908,2800,2782,2674,2256,2796,2688,770,800,350,782,242,1664,812,1694,1676,364,796,256,688,2558,2540,2590,2572,2554,1794,2766,2658,2226,1808,2780,2672,660,336,228,672,348,564,240,1104,578,1442,1118,1010,1454,1346,1022,1886,1360,2224,1900,1792,2656,2238,1806,2670,238,36,900,48,912,1776,2640,2654,548,224,116,466,1330,1006,34,898,6,20,884,32,112,436,4,450,18,882,1662,412,394,1276,1258,828,2140,1616,1598,2122,1692,810,286,1136,1150,718,702,734,378,1674,1582,1166,1242,2526,2538,2000,2430,2106,2154,3018,2476,2588,2136,3000,2570,1272,1164,2028,1612,1504,2044,1596,1580,2552,2444,1906,1920,1798,2770,2662,2230,2228,2970,2984,2876,2340,2232,2338,1908,2768,2660,1228,2092,1660,842,426,408,1290,824,410,392,1274,1256,826,1706,1688,2138,1614,2478,2460,2120,1690,376,1240,808,716,608,284,268,300,732,748,1148,700,2104,1672,1564,1350,2322,2214,1890,1782,1780,2956,2524,2968,2536,2860,2428,2754,2752,1462,2434,2326,2002,1892,2864,2756,2324,2862,2432,2004,2320,2646,2644,1784,2648,2216,2218,2212,856,838,424,406,1288,1270,840,1720,2152,1702,2134,1704,2584,3016,2586,2566,2998,2568,730,390,422,1286,1594,1254,822,2150,3014,2458,2118,1686,2010,2982,2550,2874,2042,2906,2474,2026,2890,2366,2442,2580,2472,3012,2996,2364,2904,2888,768,780,1644,1212,2508,794,686,362,1658,1550,1226,254,2522,2414,2090,1984,1446,2418,2310,1986,1996,1876,1888,2848,2740,2308,2306,1552,1444,1982,148,160,1012,594,486,1026,1024,500,1364,1040,40,52,904,916,472,484,470,582,474,150,162,176,580,272,706,720,598,612,1476,1138,1152,164,1028,596,626,1182,2032,2046,1490,178,1042,610,258,260,274,288,692,694,276,1140,290,1154,262,1126,704,304,1168,584,270,302,318,1014,592,192,1056,624,640,316,1180,1474,1488,146,586,1124,152,1016,1338,1768,1336,1334,2632,2200,2198,2202,1878,1558,1450,1988,1880,1448,1874,42,54,68,38,918,932,56,70,920,934,488,502,84,948,516,490,504,166,180,518,194,532,208,58,72,86,100,1348,1368,2018,1910,1382,2246,1922,1352,1366,1396,2260,1936,1812,1380,1354,1030,1044,1058,168,182,1032,1046,600,614,196,1060,628,616,630,644,210,1074,642,1460,1480,1494,1508,1924,1478,1492,1938,1506,1072,1894,1896,1464,922,936,950,60,74,924,938,492,506,88,952,520,508,184,522,198,536,212,76,90,104,102,966,534,964,1786,1800,1814,1788,1802,1356,1370,1816,1384,1372,1048,1386,1062,200,1064,214,1078,1400,1076,940,954,92,956,524,540,108,106,970,538,968,1830,1398,1796,1828,2244,906,44,908,476,478,154,46,902,107}.

Computation time under increasing delays : {13.44,18.248,32.688,108.596}

Cite this as: Mingshuai Chen, "Synthesizing Controllers for Safety Games under Delayed Information" from the Notebook Archive (2021), https://notebookarchive.org/2021-08-5lc88f4