Scaling Up Logico-Numerical Strategy Iteration

Tested max-strategy improvement algorithms:
  • GS'07: for each boolean state and each template row: test non-visited strategies
  • GM'11: for each boolean state and each template row: test all non-visited strategies at once
  • n: for each template row: test strategies for all boolean states at once by naive model enumeration
  • g: for each template row: test strategies for all boolean states at once by model generalisation
  • m: for each template row: test strategies for all boolean states at once by two-layered model enumeration generalisation
  • s: test strategies for all boolean states and all template rows at once by model enumeration
  • n: for each template row: test strategies for all boolean states at once by model enumeration and retesting successful models

    Comparison between Max-Strategy Iteration and Widening-Based Techniques

    Examples
    state varsinput varsCFGmax-strategy iterationstd.analysisabs.accel.
    templatebool.num.bool.num.locsarcsGS'07GM'11gs(wid.delay=2,desc.=2)(wid.delay=2,desc.=2)
    Traffic 1BOX660018612.1602.1042.3282.1641.2240.428
    Traffic 2ZONE680018151121.756114.387108.04796.9783.4922.856
    Traffic 3ZONE881050619674.062640.220356.93328.9322.07719.170
    Thermostat 1BOX43026150.3600.3200.2840.2640.8200.852
    Thermostat 2BOX65041814516.80115.1093.4403.22826.62630.398
    Thermostat 3BOX8706661357720.205715.35366.52061.880674.182907.889
    Window 1OCT955021120109.283102.31870.74073.4334.5684.696
    Window 2OCT1156045452393.901371.511189.096286.31818.57323.493
    Window 3OCT135708113881412.4441220.348241.669697.36870.17693.510
    Drugpump 1INT41041623192.60290.3186.0524.553209.963119.655
    Drugpump 2INT712813411201o.o.mem.o.o.mem.149.46395.457>1800>1800
    Drugpump 3INT101481146112561o.o.mem.o.o.mem.1019.348o.o.mem.>1800>1800

    Comparison between Various Variants of the Max-Strategy-Improvement Algorithm

    Examples
    state varsinput varsCFGoctagonal templatesbox templates
    bool.num.bool.num.locsarcsGS'07GM'11ngmstGS'07GM'11ngmst
    simple loop 13200490.1640.1280.1120.1160.1480.1080.1200.1000.1040.0880.0800.0920.0800.092
    simple loop 242106240.3680.2800.1160.1040.1360.1360.1240.2040.1960.0840.0720.0920.0720.088
    simple loop 3522010721.0440.7760.1440.1400.1760.1440.1760.5880.4560.1120.0880.1080.1120.132
    simple loop 46230182403.4562.5600.2320.1120.1600.2360.2602.0641.4520.2440.0800.1160.2200.244
    simple loop 572403486413.3779.3530.5960.1200.1840.5520.6287.9525.6320.7760.0960.1520.6360.680
    simple loop 6825066326449.83536.6422.3280.1120.2481.7281.98832.83021.5853.4560.0880.1962.1602.536
    simple loop 7926013012672222.642177.51511.1610.1240.3766.8727.904143.901101.27819.1050.0800.3168.04110.925
    simple loop 81027025849920>300>30071.6760.1320.67227.19432.134>300>300135.0360.1000.62037.41849.831
    simple loop 911280??>300>300>3000.1240.712>300>300>300>300>3000.0921.436>300>300
    simple loop 1012290??>300>300>3000.1324.448>300>300>300>300>3000.1004.048>300>300
    simple loop 11132100??>300>300>3000.14015.153>300>300>300>300>3000.11612.297>300>300
    simple loop 12142110??>300>300>3000.16063.560>300>300>300>300>3000.15249.615>300>300
    simple loop 13152120??>300>300>3000.208>300>300>300>300>300>3000.212259.248>300>300
    simple loop 14162130??>300>300>3000.308>300>300>300>300>300>3000.360>300>300>300
    simple loop 15172140??>300>300>3000.568>300>300>300>300>300>3000.788>300>300>300
    simple loop 16182150??>300>300>3001.204>300>300>300>300>300>3002.416>300>300>300
    nested loop 1 143005211.8121.3440.9080.9361.3080.9680.9520.4320.3200.1800.1560.2160.1640.172
    nested loop 1 253108524.4083.4840.9760.9521.3121.0281.0001.0840.7320.1800.1640.2160.1760.180
    nested loop 1 363201414412.6339.6251.1840.9561.3641.2521.1843.0682.0720.2360.1800.2240.2280.228
    nested loop 1 473302644839.16630.9701.8680.9601.4041.8641.8249.9696.7960.4120.1760.2440.3840.400
    nested loop 1 58340501536133.004107.5394.7080.9641.5003.7883.82034.91024.1261.0800.1720.2720.9160.996
    nested loop 1 69350985632>300>30018.1890.9521.73211.00511.581139.845100.0224.1480.1800.3563.0723.256
    nested loop 1 71036019421504>300>300105.1750.9722.22841.49143.471>300>30018.7010.1840.51211.50112.901
    nested loop 1 81137038682560>300>300>3000.9843.436165.058186.376>300>300109.1870.1840.86849.50756.464
    nested loop 1 912380??>300>300>3000.9926.896>300>300>300>300>3000.1961.944>300>300
    nested loop 1 1013390??>300>300>3000.98817.233>300>300>300>300>3000.2165.116>300>300
    nested loop 1 11143100??>300>300>3001.02052.719>300>300>300>300>3000.23615.757>300>300
    nested loop 1 12153110??>300>300>3001.056223.750>300>300>300>300>3000.26464.388>300>300
    nested loop 1 13163120??>300>300>3001.148>300>300>300>300>300>3000.344>300>300>300
    nested loop 1 14173130??>300>300>3001.364>300>300>300>300>300>3000.560>300>300>300
    nested loop 1 15183140??>300>300>3001.888>300>300>300>300>300>3001.028>300>300>300
    nested loop 1 16193150??>300>300>3004.116>300>300>300>300>300>3002.748>300>300>300
    nested loop 2 1440064313.93311.8418.1098.64510.6538.5538.2012.0121.4840.3600.3520.4960.3440.364
    nested loop 2 254101010034.13030.1948.5098.50110.6138.9938.4494.7203.5960.3760.3640.4880.3800.400
    nested loop 2 364201825691.42680.1499.4458.46110.7379.7779.04912.8419.8370.4840.3920.4960.4760.488
    nested loop 2 4743034736>300249.81611.8338.53710.81711.77310.75338.37429.4780.8160.3640.5320.7680.824
    nested loop 2 58440662368>300>30021.9378.41711.21318.18116.673127.716103.6622.1800.3750.6161.8361.952
    nested loop 2 694501308320>300>30070.0528.53311.78940.67538.322>300>3008.0890.3760.7125.9166.280
    nested loop 2 71046025830976>300>300>3008.46113.081129.668128.584>300>30038.6540.4040.98422.40924.626
    nested loop 2 811470514115328>300>300>3008.54516.105>300>300>300>300258.0960.3961.62897.883108.387
    nested loop 2 912480??>300>300>3008.54524.650>300>300>300>300>3000.4123.348>300>300
    nested loop 2 1013490??>300>300>3008.60549.371>300>300>300>300>3000.4209.101>300>300
    nested loop 2 11144100??>300>300>3008.629135.972>300>300>300>300>3000.44427.014>300>300
    nested loop 2 12154110??>300>300>3008.709>300>300>300>300>300>3000.492108.011>300>300
    nested loop 2 13164120??>300>300>3008.765>300>300>300>300>300>3000.616>300>300>300
    nested loop 2 14174130??>300>300>3009.129>300>300>300>300>300>3000.888>300>300>300
    nested loop 2 15184140??>300>300>3009.885>300>300>300>300>300>3001.596>300>300>300
    nested loop 2 16194150??>300>300>30012.721>300>300>300>300>300>3003.972>300>300>300