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.
Figures & tables
((a))
((b))
((c))
((d))
Scenario
Monolithic SMC (baseline)
Compositional SMC (ours)
Δ
S → X
0.6750
0.7074
+0.0324
S → X → S
0.6520
0.6898
+0.0378
S → O → C
0.4310
0.4740
+0.0430
C → S → X → S
0.5670
0.6206
+0.0536
C → X → S → X → C
0.3820
0.3819
−0.0001
S → choose ( C , X , O )
0.9800
0.9584
−0.0216
Table 1 : Estimated satisfaction probabilities for the Tollgate specification under the fixed-trace-budget regime.
Figure 2 : Fixed-time-budget convergence for the V-Shaped specification on the C → S → X → S scenario. 753 monolithic and 14871 compositional traces generated within the 15-minute budget.
Appendix figures & tables41 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 3 : Safety and co-safety specifications used in the experiments. Here v is the vehicle speed (m/s) and δ the steering angle; doubly circled states are accepting, q0 is the initial state, and ∗ marks a self-loop on any symbol.
Scenario
Monolithic
Compositional
Δ
2-Stop (safety)
S → X
0.6650
0.6712
+0.0062
S → X → S
0.6000
0.6700
+0.0700
S → O → C
0.3890
0.4511
+0.0621
C → S → X → S
0.5380
0.6156
+0.0776
C → X → S → X → C
0.3550
0.3849
+0.0299
Appendix
Table 2 : Estimated satisfaction probabilities for the monolithic baseline and our compositional method under the fixed-budget regime described in Section 4.1 . Δ denotes the compositional estimate minus the monolithic estimate.
Monolithic
Compositional
Scenario
N
ρ
N
ρ
Δ
Two-stop (safety)
S → X
2347
0.6412
12262
0.6558
+0.0146
S → X → S
1618
0.6057
12262
0.6533
+0.0476
S → O → C
788
0.3820
12335
0.4410
+0.0590
C → S → X → S
753
0.5618
14871
0.5892
+0.0275
Appendix
Table 3 : 15-minute time-budget results. ρ is the satisfaction probability estimate; N is the number of traces generated; Δ denotes the compositional estimate minus the monolithic estimate.
((a))
((b))
((c))
((d))
((e))
((f))
((g))
((a))
((b))
((c))
((d))
((e))
((f))
((g))
((a))
((b))
((c))
((d))
((e))
((f))
((g))
((a))
((b))
((c))
((d))
((e))
((f))
((g))
Monolithic
Compositional
Scenario
N
ρ
N
ρ
Δ
Two-stop (safety)
S → choose ( C , X , O )
188
0.9734
1161
0.9503
−0.0231
S → shuffle ( C , X , O )
76
0.9211
1161
0.8795
−0.0415
Tollgate (safety)
S → choose ( C , X , O )
188
0.9787
1161
0.9568
−0.0219
Appendix
Table 4 : 60-minute time-budget results on the choose / shuffle scenarios. ρ is the satisfaction probability estimate; N is the number of traces generated; Δ denotes the compositional estimate minus the monolithic estimate.
((a))
((b))
((c))
((d))
((e))
((f))
((g))
((h))
Monolithic
Compositional (matched)
Scenario
N
ρ
N
ρ
Δ
Two-stop (safety)
S → X
2347
0.6412
3064
0.6482
+0.0070
S → X → S
1618
0.6057
3064
0.6459
+0.0402
S → O → C
788
0.3820
3082
0.4617
+0.0797
C → S → X → S
753
0.5618
3716
0.5781
+0.0163
Appendix
Table 5 : Compute-matched ablation. ρ is the satisfaction probability estimate; N is the number of traces generated; Δ denotes the compositional estimate minus the monolithic estimate.