## Line Graphs: Property Verification Efficiency Across Datasets
### Overview
The image contains two line graphs comparing the efficiency of different computational methods in verifying properties across two datasets: CollisionDetection and ACAS. Both graphs plot "% of properties verified" against "Computation time (in s)" on a logarithmic scale. Four methods are compared: interval (blue), planetsym-feasible (orange), planet-feasible (green), and planet-opt (red).
---
### Components/Axes
- **Y-Axis**: "% of properties verified" (0–100% range, linear scale).
- **X-Axis**: "Computation time (in s)" (logarithmic scale: 10⁰ to 10³ seconds).
- **Legends**: Positioned at the bottom-right of each graph, with color-coded labels:
- Blue: interval
- Orange: planetsym-feasible
- Green: planet-feasible
- Red: planet-opt
- **Text Elements**:
- (a) CollisionDetection Dataset
- (b) ACAS Dataset
---
### Detailed Analysis
#### (a) CollisionDetection Dataset
- **Trends**:
- All methods (interval, planetsym-feasible, planet-feasible, planet-opt) rapidly reach ~100% verification within ~10⁰–10¹ seconds.
- After the initial spike, all lines plateau near 100%, indicating near-complete property verification with minimal computation time.
- **Key Data Points**:
- Interval (blue): Peaks at ~100% by 10⁰ seconds.
- Planetsym-feasible (orange): Peaks at ~100% by 10⁰ seconds.
- Planet-feasible (green): Peaks at ~100% by 10⁰ seconds.
- Planet-opt (red): Peaks at ~100% by 10⁰ seconds.
#### (b) ACAS Dataset
- **Trends**:
- **Interval (blue)**: Slow, gradual increase from ~0% to ~20% over 10³ seconds.
- **Planetsym-feasible (orange)**: Steeper rise, reaching ~40% by 10² seconds, plateauing near 50%.
- **Planet-feasible (green)**: Rapid ascent to ~50% by 10¹ seconds, plateauing near 50%.
- **Planet-opt (red)**: Sharp rise to ~60% by 10¹ seconds, plateauing near 60%.
- **Key Data Points**:
- Interval (blue): ~20% at 10³ seconds.
- Planetsym-feasible (orange): ~50% at 10³ seconds.
- Planet-feasible (green): ~50% at 10³ seconds.
- Planet-opt (red): ~60% at 10³ seconds.
---
### Key Observations
1. **CollisionDetection Dataset**:
- All methods achieve near-complete property verification almost instantaneously (<1 second).
- No significant differences between methods in efficiency.
2. **ACAS Dataset**:
- **Interval method** is orders of magnitude slower, achieving only ~20% verification after 1000 seconds.
- **Planet-opt** and **planet-feasible** methods outperform others, achieving ~60% and ~50% verification, respectively, within 10 seconds.
- **Planetsym-feasible** lags behind planet-opt but outperforms interval.
---
### Interpretation
- **CollisionDetection**: The dataset’s simplicity allows all methods to verify properties with minimal computation, suggesting it is a "easier" problem for automated verification.
- **ACAS**: The dataset’s complexity is evident in the interval method’s poor performance, which struggles to verify properties even after 1000 seconds. This highlights the need for optimized methods like planet-opt and planet-feasible in handling complex, real-world problems.
- **Method Comparison**: Planet-opt consistently outperforms other methods in both datasets, suggesting it is the most efficient approach for property verification. The interval method’s inefficiency in ACAS may stem from its reliance on conservative approximations, which become impractical for complex systems.
The data underscores the importance of method selection based on problem complexity, with planet-opt emerging as the most robust solution for high-stakes verification tasks.
