Scenario-Based Compositional Statistical Model Checking for Safety Specifications

This project extends compositional statistical model checking for autonomous vehicles from Markovian to non-Markovian safety specifications, covering safety requirements for self-driving cars that the prior framework could not express. Published with UC Berkeley faculty at the International Conference on Runtime Verification 2026.

The core idea is to augment simulation states with DFA states that encode the temporal logic of the specification, then propagate the DFA distribution across primitive scenario traces. This makes it possible to verify safety properties that depend on the history of events (not just the current state) while preserving the compositional structure that keeps large-scale verification tractable.

By reusing simulation results across driving scenarios, the method runs up to 32.3× more test simulations in the same time budget and cuts estimation error from 0.275 to 0.014 in the hardest case. Evaluated on the MetaDrive driving simulator, with support from DARPA, NSF, Nissan, and California PATH.

Affiliation

UC Berkeley

Partners

Report

International Conference on Runtime Verification 2026

Keywords

Compositional Analysis
Statistical Model Checking
DFA
Automata Theory
Markov Chains
Python
VerifAI
MetaDrive
Scenic

Testing a self-driving car in every scenario without re-driving each one

To show an autonomous car merely matches the human fatality rate, a fleet of 100 cars would have to drive 275 million miles without a single fatality — about 12.5 years, around the clock. To show it is 20 % safer: 8.8 billion miles, roughly 400 years. So the field tests in simulation instead, across thousands of scenarios — each a specific arrangement of road, traffic, and events — and every scenario is run thousands of times.

Top: a road as a mileage bar from 0 to 400 million miles, with a marker at 275 million miles annotated 'a fleet of 100 cars, 24 h a day, no fatalities: about 12.5 years, just to match the human fatality rate (RAND, 2016); proving it 20 % safer: 8.8 billion miles, about 400 years'. Bottom: a grid of scenario tiles labelled S, X, O, C, annotated 'thousands of scenarios × thousands of runs each; every run is a trace, every trace costs simulator time'. A closing line reads: so the question becomes, how do you spend those simulator hours without repeating yourself? — Why simulation, and why it is still expensive. Road miles cannot deliver statistical confidence in any reasonable time (RAND, 2016), so confidence comes from simulated traces — and every trace costs simulator time.

The tool for turning those runs into a number you can trust is statistical model checking (SMC): treat the car as a black box, run it many times, and estimate the probability that it satisfies a safety property, with a confidence bound attached. This project makes SMC compositional — scenarios sharing structure share simulation work — and extends it to properties that depend on the history of a drive, not just its final state. It started as a class project in Berkeley’s EECS 219C (Formal Methods) and became a paper with Berkeley faculty at the International Conference on Runtime Verification (RV) 2026.

Published at RV 2026 — work supported by DARPA, NSF, Nissan, and California PATH.

Three annotated cards pointing at three vehicles: an autonomous car labelled core case, a launching spacecraft labelled co-safety, and a UAV labelled SMC, each describing how its mission decomposes into primitive phases checked against safety sub-specifications. — The same structure appears wherever a black-box controller is tested across phased missions — driving is the paper’s case, but spacecraft ascent and UAV mission planning decompose into primitive phases the same way.

The redundancy monolithic SMC can’t see

Scenarios are rarely atomic. A realistic one is a composite built from a small vocabulary of primitives — a straight road, an intersection, a roundabout, a curve — glued end to end. The same primitives recur constantly, and every combination is a scenario the car should be checked against.

Top: four primitive road pieces drawn as roads — S straight, X intersection, O roundabout, C curve — each with a marked entry and exit point. Bottom: the composite S → X → S → C drawn as one continuous road with a car at the start and cream dots at the seams where one primitive's exit becomes the next one's entry. — The four primitives (`S`, `X`, `O`, `C`), and a composite made by gluing them at their terminal states — exactly how a Scenic program writes it. The seams are where the interesting work happens.

Monolithic SMC treats each composite as its own sealed problem: a fresh batch of long simulations per scenario–specification pair. Swap an intersection for a roundabout and everything is thrown away and redone, even though most of the drive is identical to one already simulated. On a corpus of overlapping composites, that waste compounds.

Top row: four primitive tiles labelled S, X, O, C. Bottom row: three composition operators — sequential S then X, choice of S or X with probability one half each, and shuffle of S then X or X then S with probability one half each. — Three operators build composites: sequential (`S → X`), `choose` (pick a branch at random), and `shuffle` (random order). They mirror Scenic’s own composition clauses, so the decomposition is already in the source.

How it works

The idea is to shift the cost onto the primitives: simulate each one once into a shared trace pool, and answer any composite by composing statistics instead of running new simulations. Two things make that non-trivial.

Carrying history across primitives. The interesting properties are about the sequence — “never four consecutive slow steps” — and cannot be decided from a final state alone, which is what broke the earlier Markovian estimator. The framework writes each specification as an automaton and carries a distribution over its states, μ, from one primitive to the next. Each primitive’s traces say how often they move the automaton from state q to q′; propagate μ through S, then X, then S, and the satisfaction probability is whatever mass never reached the violating state. A non-Markovian property becomes a chain of Markovian updates.

A road S → X → S with a car at the start. Above each seam is a small bar chart of the automaton state distribution μ over the Tollgate states moving, slow-1, slow-2, slow-3 and violated: μ-zero has all mass on moving, and with each primitive mass spreads into the slow states and accumulates in the orange violated bar. Below, the propagation chain μ-zero → μ-S → μ-S→X → μ-S→X→S, the one-step update rule, and the note that the satisfaction probability is the mass left outside violated. — Propagating the automaton state distribution. For the **Tollgate** property, μ starts with all mass on `moving`; each primitive redistributes it using that primitive’s own traces, and the mass that ends in `violated` is the failure probability.

The Tollgate specification automaton. States moving, slow-1, slow-2, slow-3 in a row, and an absorbing rejecting state violated. A slow step advances the counter, a fast step from any slow state returns to moving, and a fourth consecutive slow step goes to violated. — The **Tollgate** automaton itself. Co-safety properties — “eventually complete a fast–slow–fast profile” — are handled by checking the complemented safety property and subtracting from one.

Correcting the seams. When S and X are each simulated alone, the states S ends in do not match the states X was started from, so stitching their traces together gives a biased answer. The fix is self-normalized importance sampling: fit a Gaussian kernel density estimate to the boundary features (position, speed, heading) on each side, and reweight X’s traces by how likely their starting state is under S’s exit distribution. The propagation rule stays the same — one extra weight per trace.

Top: the seam between S and X, with a green dot for S's exit states and an orange dot for X's entry states marked not-equal. Below left: two overlapping density curves over a boundary feature, green for where S actually ends and orange for where X's traces started, with X's stored traces drawn as dots sized by their importance weight. Right: the propagation formula with the importance weight o-S over iota-X highlighted, and a note that if the densities barely overlap a few traces get huge weights and the estimate gets noisy, which is why primitives are simulated over diverse geometries and entry speeds. — The seam correction. Traces that start where S actually ends count more; traces that start where S never ends count less. The correction is only as good as the overlap, which is why primitives are simulated across diverse geometries and entry conditions.

Choice and shuffle fall out as algebra on the per-branch estimates: a choose is a mixture, a shuffle is the average over orderings, and both cost nothing on top of the shared pool.

A left-to-right pipeline: a Scenic program with a scenario and a Tollgate requirement; four primitives S, X, O, C each simulated once into 1000 stored traces; per-primitive statistics giving transition fractions between automaton states plus KDEs of entry and exit states; a compose step that propagates μ with reweighting at seams, mixes over choose, and averages over shuffle; and an estimate ρ̂ with a Hoeffding bound. Below, one trace pool fans out to all seven composite scenarios, with the note that an eighth composite would need zero new simulations. — The full pipeline. One pool of primitive traces serves every composite built from them; adding a new composite is a composition step, not a simulation campaign.

Results

Built as a prototype inside VerifAI, Berkeley’s toolkit for analysing AI-based systems, with MetaDrive as simulator and Scenic as scenario language. The system under test is MetaDrive’s built-in expert policy — a placeholder, so the comparison measures the verifier, not the driver. Seven composites (five sequential, one choose, one shuffle) against four specifications — two safety (2-Stop, Tollgate), two co-safety (V-Shaped, Sustained) — for 28 pairs, under both a matched trace budget and a matched time budget.

Accuracy holds. At a matched trace budget — 1000 composite traces for the baseline versus 1000 per primitive reused everywhere — the compositional estimates track the monolithic ground truth across nearly all pairs.

Composite	Monolithic ρ̂	Compositional ρ̂	Δ
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
S → shuffle(C, X, O)	0.9150	0.8941	−0.0209

Estimated satisfaction probabilities for the Tollgate specification under the fixed-trace-budget regime. The one place the gap grows is the Sustained co-safety property on S → shuffle(C, X, O) (Δ = +0.1162), where the mismatch between primitives’ initial-state distributions is largest — exactly the overlap the seam correction depends on.

Efficiency is where it pays off. Given the same 15-minute wall-clock budget, the compositional method generates 14,871 primitive traces against 753 monolithic — 14.6× more on average, up to 32.3× — and converges closer to the reference: mean deviation 0.029 versus 0.039.

Two horizontal-bar comparisons. Top: traces generated in a 15-minute budget — monolithic 753, compositional 14,871. Bottom: estimation error on the hardest pair, V-Shaped on S shuffle C X O — monolithic 0.275, compositional 0.014; even at a 60-minute budget the monolithic error is still 0.188. — On the hardest pair, ⟨V-Shaped, `S → shuffle(C, X, O)`⟩, the error is **0.014** against the baseline’s **0.275** — a gap the baseline cannot close even with four times the budget.

A line chart of satisfaction probability versus time budget on a log scale for V-Shaped on C → S → X → S. Two nearly overlapping curves, compositional in green and monolithic in red, both settle around 0.44, with the compositional curve reaching it from a far smaller budget. — Both methods converge to the same answer; the compositional estimate gets there from a far smaller wall-clock budget because that budget buys vastly more reusable traces.

Why it works. A compute-matched ablation makes the mechanism explicit: give the compositional method the same total budget split across the four primitives, and the two methods tie (0.038 versus 0.039). Strip away the extra trace count and the advantage disappears — the win comes from one place, sample reuse.

What I took away

Less about model checking than about the shape of the redundancy. The moment a verification target is built from reusable parts, re-verifying the whole from scratch each time is the real waste. The engineering is in composing the pieces back together at the seams without letting the statistics drift — and the seams are where the method’s one weak spot lives too.