\n
## Line Charts: Performance Comparison on Two Datasets
### Overview
The image contains two side-by-side line charts comparing the performance of four different methods (`interval`, `planetsym-feasible`, `planet-feasible`, `planet-opt`) on two distinct datasets. The charts plot the percentage of properties verified against computation time on a logarithmic scale. The overall visual suggests a performance benchmark in a formal verification or property checking context.
### Components/Axes
**Common Elements (Both Charts):**
* **Y-axis:** Label: `% of properties verified`. Scale: Linear, from 0 to 100 with major ticks at 0, 20, 40, 60, 80, 100. A dashed horizontal line is present at the 100% mark.
* **X-axis:** Label: `Computation time (in s)`. Scale: Logarithmic (base 10). Major ticks are labeled at `10^0` (1 second), `10^1` (10 seconds), `10^2` (100 seconds), and `10^3` (1000 seconds).
* **Legend:** Positioned in the top-right corner of each plot area. Contains four entries with corresponding colored lines:
* Blue line: `interval`
* Orange line: `planetsym-feasible`
* Green line: `planet-feasible`
* Red line: `planet-opt`
**Chart-Specific Elements:**
* **Chart (a) - Left:**
* **Title/Label (below chart):** `(a) CollisionDetection Dataset`
* **Chart (b) - Right:**
* **Title/Label (below chart):** `(b) ACAS Dataset`
### Detailed Analysis
**Chart (a): CollisionDetection Dataset**
* **Trend Verification:**
* `planet-opt` (Red): Exhibits an extremely steep, near-vertical ascent starting just before `10^0` seconds, reaching a plateau very close to 100% verification. The line is essentially flat after `10^0`.
* `planet-feasible` (Green) & `planetsym-feasible` (Orange): Both show a similarly steep ascent starting at approximately `10^0` seconds. They plateau at a high level, visually estimated between 85% and 90%. The green line (`planet-feasible`) appears to plateau at a marginally higher percentage than the orange line.
* `interval` (Blue): Remains flat at or very near 0% across the entire time range shown (up to `10^3` seconds).
* **Key Data Points (Approximate):**
* At `10^0` seconds: `planet-opt` is already near 100%. `planet-feasible` and `planetsym-feasible` are in their steep rise phase, passing through ~50-70%. `interval` is at 0%.
* From `10^0` to `10^3` seconds: `planet-opt` holds at ~100%. `planet-feasible` holds at ~90%. `planetsym-feasible` holds at ~88%. `interval` remains at 0%.
**Chart (b): ACAS Dataset**
* **Trend Verification:**
* `planet-feasible` (Green): Shows a rapid initial rise starting between `10^0` and `10^1` seconds, reaching a plateau around 45% by `10^1` seconds. It remains flat thereafter.
* `planet-opt` (Red): Follows a similar trajectory to `planet-feasible` but with a slightly delayed start and a slightly lower plateau, estimated around 42-44%.
* `planetsym-feasible` (Orange): Begins its ascent later, around `10^1` seconds. It rises more gradually than the green and red lines, showing a steady, concave-down increase. It approaches the plateau level of the green/red lines (~45%) by the end of the chart (`10^3` seconds).
* `interval` (Blue): Remains near 0% for most of the timeline. It shows a very slight, gradual increase starting around `10^2` seconds, reaching an estimated 15-20% by `10^3` seconds.
* **Key Data Points (Approximate):**
* At `10^1` seconds: `planet-feasible` is near its plateau (~45%). `planet-opt` is at ~35%. `planetsym-feasible` is just beginning to rise (~5%). `interval` is at 0%.
* At `10^2` seconds: `planet-feasible` and `planet-opt` are stable at ~45% and ~43% respectively. `planetsym-feasible` has risen to ~30%. `interval` is still near 0%.
* At `10^3` seconds: `planet-feasible` and `planet-opt` are stable. `planetsym-feasible` is at ~45%. `interval` has risen to ~18%.
### Key Observations
1. **Dataset-Dependent Performance:** The relative effectiveness of the methods changes dramatically between the two datasets. `planet-opt` is the clear, near-perfect performer on CollisionDetection but is only marginally better than `planet-feasible` on ACAS.
2. **Plateau Behavior:** All methods except `interval` on ACAS reach a performance plateau, indicating a maximum verifiable property percentage within the given time constraints for each method/dataset combination.
3. **The `interval` Method:** It is largely ineffective on CollisionDetection (0%) and shows only modest, late gains on ACAS (~18% at 1000s).
4. **Convergence on ACAS:** The `planetsym-feasible` method, while slower to start, eventually converges to the same performance level as the leading methods (`planet-feasible`, `planet-opt`) on the ACAS dataset given enough time (~1000 seconds).
### Interpretation
This data demonstrates a classic trade-off analysis in algorithm or tool selection for property verification. The `planet-opt` method appears to be the most optimized, achieving maximum results fastest on the simpler CollisionDetection task. However, on the presumably more complex ACAS dataset, the performance gap between `planet-opt` and the more basic `planet-feasible` narrows significantly, suggesting diminishing returns from optimization on harder problems.
The stark failure of the `interval` method on CollisionDetection and its poor performance on ACAS indicates it is likely a baseline or less sophisticated approach unsuited for these specific verification tasks. The behavior of `planetsym-feasible` on ACAS is particularly interesting; its slower but steady climb suggests it may be using a more exhaustive or less guided search strategy that is time-intensive but ultimately effective.
The charts effectively argue that method choice is highly context-dependent (dataset-dependent). There is no single "best" method across all scenarios. For quick, high-confidence results on CollisionDetection, `planet-opt` is superior. For the ACAS problem, if computation time is limited (e.g., <100 seconds), `planet-feasible` is the best choice. If ample time (>1000 seconds) is available, `planetsym-feasible` becomes a competitive alternative. This analysis would guide a user to select a tool based on their specific problem domain and time budget.
