<< back

Logico-Numerical Max-Strategy Iteration

Experimental Evaluation

Benchmarks
Templates: octagonal constraints
enumerated numerical max-strategy iterationlogico-numerical max-strategy iterationstandard octagons
vars locsarcstimeprovedlocsarcstimeprovedkeptworselostprovedworse2
LCM Quest 0a-1 7/2/0 7 130.37 y 5 90.24 y 100% 0% 0% y 0%
LCM Quest 0a-2 7/3/0 6 132.40 ? 4 61.29 ? 93% 7% 0% ? 80%
Gate 1 4/4/2 7 2310.1 ? 5 125.52 ? 92% 8% 0% ? 0%
Traffic 1 4/6/0 18 61142 y 16 5824.6 y 100% 0% 0% y 0%
Traffic 2 4/8/0 18 1511753 y 16 73137 y 100% 0% 0% ? 10%
LCM Quest 0b-110/3/0 19 456.31 y 12 252.08 y 100% 0% 0% y 7%
LCM Quest 0b-210/4/0 17 5459.9 ? 11 2614.0 ? 88% 6% 6% ? 34%
LCM Quest 0c-115/4/0 28 75101 y 16 3710.0 y 100% 0% 0% y 4%
LCM Quest 0c-215/5/0 25 89> ? 14 37136 ? ? 25%
LCM Quest 1b-116/5/0 55 360900 y 29 12324.4 y 100% 0% 0% ? 10%
LCM Quest 1b-216/5/0 45 306> ? 23 95663 ? ? 11%
LCM Quest 1-1 16/5/0 114 4931774 y 42 235167 y 100% 0% 0% y 53%
LCM Quest 1-2 16/6/0 100 644> ? 34 227> ?
LCM Quest 2-1 17/6/0 2472648> ? 82 580424 y y 58%
LCM Quest 2-2 17/7/0 1982302> ? 62 443> ?
LCM Quest 3-1 25/5/0 4832136> ? 58 3451130 y y 19%
LCM Quest 3d-126/6/0 2811416> ? 81 4022731 y y 11%
LCM Quest 3e-127/7/0 6384656> ? 140 970> ?
Legend:
  • vars...Boolean state variables / numerical state variables / Boolean inputs
  • locs...number of locations of the CFG
  • arcs...number of arcs of the CFG
  • times in seconds, >...timed out after 3600s
  • y...property proved, ?...property not proved
  • kept, worse, lost...percentage of bounds kept, worsened and lost in logico-numerical max-strategy iteration w.r.t. enumerated numerical max-strategy iteration
  • worse2...percentage of worse bounds in standard logico-numerical octagon analysis w.r.t. logico-numerical max-strategy iteration on the same control flow graph
<< back