PaperlayerView exact revision on arXiv

Source-linked AI summary

Scenario-Based Compositional Statistical Model Checking for Safety Specifications

Abhinav Pomalapally, Arya Raeesi, Kevin Kai-Chun Chang, Beyazit Yalcinkaya, Sanjit A. Seshia

arXiv:2610.05571v1cs.LOcs.AIcs.ROcs.SEcs.SYeess.SY

TL;DR

Simulation-based verification of opaque AI systems faces costly repeated simulations, especially when each composite scenario is analyzed independently. This paper decomposes scenarios and specifications for compositional SMC, and reports accurate estimates for unseen composites with lower simulation cost through parallelization and trace reuse.

  • Problem

    SMC often requires many expensive simulations and must be repeated when scenario conditions change, creating redundant computation across structurally related composite scenarios.

    Source: §2 · p. 4

  • Method

    The framework independently verifies primitive scenarios against specification sub-parts, then composes estimates using importance sampling and kernel density estimation.

    Source: §1 · p. 2, §5 · pp. 9–10

  • Results

    The framework accurately estimates queries for previously unseen composite scenarios while reducing simulation cost; under a 15-minute budget, it generated 14.6× more traces on average than the monolithic baseline.

    Source: §4.2 · p. 8, §5 · p. 10

  • Takeaways & Limitations

    Parallelization and trace reuse reduce simulation cost, a property the authors identify as valuable for rapid feedback in early-stage development.

    Source: §5 · p. 10

    Sequential composition assumes overlap between the output and input MDP state distributions; KDE may suffer from the curse of dimensionality in high dimensions.

    Source: §3.1 · p. 6

Abstract

from arXiv · show

In safety-critical domains such as autonomous driving, systems must be evaluated across a large number of environment conditions, often represented as composite scenarios built from primitive scenarios. Existing statistical model checking (SMC) approaches analyze each composite scenario independently, requiring many expensive simulations and resulting in substantial redundant computation when scenarios share common structure. This work introduces a scenario-based compositional SMC framework for safety and co-safety specifications, enabling efficient analysis of composite scenarios. Our approach decomposes scenarios into primitives and specifications into sub-specifications, verifies each primitive independently, and composes the resulting statistical estimates using importance sampling and kernel density estimation. Our empirical evaluation shows that the proposed framework can accurately answer verification queries for previously unseen composite scenarios while reducing simulation cost through parallelization and trace reuse.

1 Introduction

Simulation-based statistical model checking (SMC) addresses verification when AI systems lack tractable explicit models, but repeated, costly simulations limit scalability. This paper introduces black-box compositional SMC that decomposes scenarios and specifications, enabling primitive-level verification and reuse of traces across composite scenarios.

1 Introduction

  • Repeated, computationally expensive simulations make high-confidence SMC results difficult to scale, and changing scenarios typically require rerunning SMC.Traditional formal verification is also often inapplicable to opaque AI systems because it requires an explicit, tractable system model.Source: §1 · pp. 1–2
  • The framework decomposes composite scenarios into primitives and specifications into sub-specifications, then verifies primitives independently and composes their statistical estimates.Primitive verification tasks can run in parallel with shorter simulations; traces can also be reused across composite scenarios to reduce redundant effort.Source: §1 · p. 2
  • The paper implements the framework in VerifAI and reports improved verification efficiency while maintaining accuracy.Simulation-based analysis treats systems as black boxes and is used when exhaustive real-world testing is infeasible.Source: §1 · pp. 1–2
  • The framework extends compositional SMC to non-Markovian safety and co-safety specifications, beyond prior work restricted to memoryless specifications.It decomposes environmental scenarios and specifications rather than internal system architectures or neural-network layers.Source: Related Work · p. 3
  • Earlier scenario-decomposition approaches relied on white-box access, offline probabilistic abstractions, or falsification rather than black-box compositional SMC for safety and co-safety properties.Related work also includes spatial or temporal decomposition of environments and specifications.Source: Related Work · p. 3

2 Motivating Example

Composite driving scenarios are built from primitive road segments and can be arranged through sequential, choice, or shuffle composition. Because monolithic SMC repeats expensive simulations for each scenario and specification pair, the motivating example shifts computation to primitives and reuses their traces to estimate results for composite scenarios.

2 Motivating Example

  • The example's primitive scenarios are a straight road (S), intersection (X), roundabout (O), and curved road (C), composed sequentially, by choice, or by shuffle.Sequential composition fixes order, while choice randomly selects an alternative and shuffle randomly permutes a collection.Source: §2 · p. 3, Figure 1 · p. 3
  • Monolithic SMC runs many simulations for each new scenario–specification pair, repeating costly long simulations that share substantial structure.The motivating example frames this as increasingly expensive as composite scenarios grow in complexity.Source: §2 · pp. 3–4
  • The approach runs the system on each primitive, stores traces, evaluates them against relevant sub-specifications, and composes results to estimate satisfaction probability.Importance sampling and kernel density estimation account for behavior-distribution mismatch, allowing estimates for previously unseen composites without running the system in those scenarios.Source: §2 · p. 4

3 Method

The method propagates automaton-state distributions across decomposed scenarios to compose SMC queries. For sequential composition, importance sampling and KDE account for a boundary-state distribution mismatch.

3 Method

  • Under a Markovian controller in an MDP, traces estimate automaton-state distributions, enabling updates for non-Markovian properties and composition across scenario operators.The empirical propagation rule supports sequential, choose, and shuffle compositions.Source: §3 · pp. 4–5
  • Co-safety queries are handled by checking the complement safety specification and subtracting its satisfaction probability from one.Source: §3 · p. 5

3.1 Sequential Composition

  • Sequential composition reuses primitive traces by importance-sampling for boundary-state mismatch, assuming adjacent scenario distributions overlap and using KDE for their estimation.The authors note KDE may suffer from the curse of dimensionality in high-dimensional spaces, and expect moderate-sized semantic feature spaces.Source: §3.1 · pp. 5–6

3.2 Choose Composition

  • Choose composition marginalizes over its selected branch; the satisfaction probability is the branch-probability-weighted mixture of constituent probabilities.Source: §3.2 · p. 6

3.3 Shuffle Composition

  • Shuffle composition averages satisfaction probabilities across sequential orders; its extension to n scenarios entails factorial growth in permutation count.The authors expect the number of shuffled scenarios to remain relatively small.Source: §3.3 · pp. 6–7

4 Empirical Evaluation

Across 28 scenario–specification pairs, compositional SMC closely tracks monolithic estimates and converges faster under a fixed time budget. Its compute-matched results are nearly tied, with trace reuse identified as the primary benefit.

4 Empirical Evaluation

  • The evaluation covers seven composite scenarios and four safety or co-safety specifications, yielding 28 pairs tested in fixed-trace- and fixed-time-budget experiments.Both approaches’ estimates are compared with fixed-trace-budget references; the prototype uses VerifAI, MetaDrive, Scenic, and MetaDrive’s built-in expert policy.Source: §4 · p. 7, §4.1 · p. 7

4.1 Evaluating Accuracy

  • Compositional estimates closely track the monolithic baseline for nearly all evaluated pairs, with a +0.1162 difference for Sustained on S →shuffle (C, X, O).The authors attribute this exception to mismatched MDP state distributions at scenario interfaces; estimate quality depends on their overlap.Source: §4.1 · p. 8

4.2 Evaluating Efficiency

  • 0.029 versus 0.039 mean deviation: under a 15-minute budget, compositional SMC converges faster toward its fixed-trace-budget references than the monolithic baseline.The compositional method generates 14.6× more traces on average, ranging from 5.2× to 32.3× more.Source: §4.2 · p. 8
  • 14,871 compositional primitive traces versus 753 monolithic traces were generated within 15 minutes for the V-Shaped C →S →X →S scenario.Figure 2 shows fixed-time-budget convergence for this representative scenario–specification pair.Source: Figure 2 · p. 9, §4.2 · p. 9
  • 0.275 versus 0.014 error: for V-Shaped with S →shuffle (C, X, O), the 15-minute monolithic estimate is less accurate than the compositional estimate.Even at 60 minutes, the monolithic error is 0.188, higher than the compositional error achieved with 15 minutes.Source: §4.2 · p. 9
  • 0.038 versus 0.039 mean deviations: with sample-count advantage removed, compositional and monolithic methods are essentially tied across 28 scenario–specification pairs.The authors identify reuse of one primitive-trace pool across composite scenarios as the primary benefit; the monolithic baseline regenerates traces per scenario.Source: §4.2 · p. 9

5 Conclusion

The framework decomposes composite scenarios and specifications, then composes primitive verification results to answer queries about unseen composites. The reported evaluation finds accurate estimates with lower simulation cost through parallelization and trace reuse.

5 Conclusion

  • Composite scenarios are decomposed into primitives and specifications into sub-specifications, whose independent verification results are composed using importance sampling and kernel density estimation.The resulting estimates answer SMC queries about previously unseen composite scenarios.Source: §5 · pp. 9–10
  • The framework supports sequential, choose, and shuffle compositions.Source: §5 · p. 10
  • The empirical evaluation reports accurate estimates with reduced simulation cost through parallelization and trace reuse, which is valuable when rapid early-stage feedback is essential.Source: §5 · p. 10

A Formal Specifications

Figure 3 presents the four specifications used in the experiments as automata over vehicle speed and steering angle.

A Formal Specifications

B Full Accuracy Results

The full accuracy results are presented for the monolithic baseline and compositional method under the fixed-budget regime described in Section 4.1.

B Full Accuracy Results

  • The section presents the full experimental results corresponding to Section 4.1.Source: B Full Accuracy Results · p. 13
  • Table 2 reports estimated satisfaction probabilities for the monolithic baseline and compositional method under the fixed-budget regime.Source: Table 2 · p. 13
  • Δ denotes the compositional estimate minus the monolithic estimate.Source: Table 2 · p. 13

C Full Efficiency Results

Under a 15-minute budget, compositional estimates deviate less from their fixed-trace references than monolithic estimates; at 60 minutes, the monolithic method remains roughly twice as far from reference. The gap is concentrated in choose/shuffle scenarios, where monolithic trace generation is costly.

C.1 15-Minute Time-Budget Experiments

  • Table 3 covers all 28 specification–scenario cells, while Figures 4–7 show estimate convergence as the 15-minute budget grows.Figure 4 is 2-Stop, Figure 5 Tollgate, Figure 6 V-Shaped, and Figure 7 Sustained; Nm and Nc count monolithic and compositional primitive traces.Source: §C.1 · p. 14, Table 3 · p. 14, Figure 4 · p. 16
  • Under a 15-minute monolithic budget (as few as 20 traces), deviation from each method’s own fixed-trace-budget reference was 0.039 for monolithic versus 0.029 for compositional estimates, making compositional deviation lower.For choose and shuffle scenarios, deviations were 0.089 vs. 0.059.Source: §C.1 · p. 20

C.2 60-Minute Time-Budget Experiments

  • 0.063 vs. 0.029 mean deviation at 60 minutes leaves the monolithic estimate roughly twice as far from reference as the compositional estimate.The monolithic deviation falls from 0.089 at 15 minutes, while the compositional deviation falls from 0.059; the comparison covers eight choose/shuffle scenario–specification pairs.Source: Table 4 · p. 20, §C.2 · p. 22, Figure 8 · p. 22
  • 0.188 vs. 0.039 is the 60-minute monolithic and compositional distance from reference, respectively, for V-Shaped shuffle.The corresponding Sustained shuffle distances are 0.203 and 0.060, respectively; the monolithic run generated 76 traces.Source: §C.2 · pp. 21–22, Figure 8 · p. 22

C.3 Compute-Matched Ablation

The compute-matched ablation truncates each primitive trace pool to match the monolithic simulation budget. With four primitives, the compositional method retains essentially the same accuracy while losing its raw sample-count advantage.

C.3 Compute-Matched Ablation

  • Splitting the budget across k = 4 primitive pools removes the compositional method’s raw sample-count advantage, yet its accuracy remains essentially unchanged.Each pool is truncated to the prefix corresponding to its equal share of the total budget, leaving the estimator unchanged.Source: §C.3 · pp. 22–24
  • 0.038 and 0.039 are the compositional and monolithic mean deviations, respectively, across 28 pairs against their 1,000-trace references.The comparison gives the compositional method the same total simulation budget as one monolithic scenario, split evenly across four primitive pools at 225 seconds each.Source: §C.3 · pp. 23–24, Table 5 · p. 23
  • A single truncated primitive pool can be reused across composite scenarios, whereas the monolithic baseline must regenerate traces for each scenario.The compositional and monolithic methods achieve nearly identical mean deviations in this compute-matched comparison.Source: §C.3 · p. 24
Loading 2610.05571v1…