Compositional Analysis for Safety Specifications

Introduction

This project extends VerifAI’s compositional statistical model checking (SMC) from Markovian to non-Markovian safety specifications, and adds a Scenic frontend so that composite driving scenarios written in standard Scenic source can be analyzed end-to-end. Compositional analysis decomposes a long simulation into short primitive scenarios whose traces are generated in parallel and stitched together via importance sampling at handoff boundaries; the contribution here is representing each safety property as a deterministic finite automaton (DFA) and propagating a distribution over DFA states across those handoffs so that history-dependent properties, “stop at most once at a tollgate,” “once the vehicle exceeds 15 m/s it must never drop below 6.5 m/s”, fall inside the compositional framework. On the MetaDrive simulator and on a Scenic intersection benchmark, the framework recovers monolithic estimates to within statistical error while achieving a 4–7× wall-clock speedup.

This was a joint course project for EECS 219C (Formal Methods: Specification, Verification, and Synthesis) at UC Berkeley, Spring 2026, with Abhi Pomalapally. Abhi led the VerifAI backend (DFA-augmented state-distribution propagation, the rejection-conditioning fix in check_with_dfa, and the MetaDrive evaluation); I led the Scenic frontend (the recursive DAG parser over containers, composition statements, and weighted invocations, and the linearization that feeds the backend); Abhi also handled the end-to-end Scenic → MetaDrive integration.

Problem Definition

Primitive and composite scenarios. Let $\mathcal{S}$ denote a finite set of primitive scenarios. Each primitive $s \in \mathcal{S}$ induces a Markov decision process $M_s = (X, A, P_s, x_0^s)$ with shared state space $X$, action space $A$, transition kernel $P_s$, and initial state $x_0^s$. Under the system policy, $M_s$ yields traces $\tau = (x_0, x_1, \dots, x_T)$ distributed according to some trace distribution $\mathcal{D}_s$. A composite scenario $c$ is built from primitives via three composition operators, mirroring Scenic’s do, do choose, and do shuffle clauses:

• sequential composition $c_1 ; c_2$, which runs $c_1$ to its terminal state and then $c_2$ from that state;
• probabilistic choice $\textsf{choose}\{(c_1, w_1), \dots, (c_k, w_k)\}$, which executes $c_i$ with probability $w_i / \sum_j w_j$;
• shuffle $\textsf{shuffle}\{c_1, \dots, c_k\}$, which executes the $c_i$‘s in a uniformly random order.

Specifications and satisfaction probability. A specification $\varphi$ is given by a deterministic finite automaton $\mathcal{A}_\varphi = (Q, \Sigma, \delta, q_0, F)$ together with a labeling function $L : X \to \Sigma$. A trace $\tau = (x_0, \dots, x_T)$ satisfies $\varphi$, written $\tau \models \varphi$, iff the run $q_0, q_1, \dots, q_T$ given by $q_{t+1} = \delta(q_t, L(x_{t+1}))$ ends in an accepting state, $q_T \in F$. The quantity of interest is

$$\rho(c, \varphi) \;=\; \Pr_{\tau \sim \mathcal{D}_c}[\tau \models \varphi].$$

We call $\varphi$ Markovian if $\tau \models \varphi$ depends only on the terminal state $x_T$, and non-Markovian otherwise.

The compositional non-Markovian analysis problem. Given a composite scenario $c$ over primitives $\mathcal{S}$, a non-Markovian specification $\varphi$ given by $(\mathcal{A}_\varphi, L)$, and a per-primitive simulation budget of $N$ traces, produce an estimate $\hat{\rho}(c, \varphi)$ of $\rho(c, \varphi)$ with a confidence half-width $\hat{\varepsilon}$ at level $\delta$ (so that $|\hat{\rho}, \rho| \leq \hat{\varepsilon}$ holds with probability at least $1, \delta$), using only the primitive trace sets $\{\tau_i^s\}_{i=1}^N \sim \mathcal{D}_s$ for $s \in \mathcal{S}$.

Why the problem is hard. The restriction to primitive traces is what makes the problem useful, primitives are short, can be simulated in parallel, and need not be re-run when $c$ changes, and also what makes it technically nontrivial. First, since $\varphi$ may be non-Markovian, $\rho(c, \varphi)$ depends on the full trace rather than its terminal state, which rules out the Markovian compositional estimator of Yalcinkaya et al. (RV 2023). Second, in $c_1 ; c_2$, the state distribution at the end of $c_1$ generally differs from the initial-state distribution of $c_2$ when $c_2$ is simulated as a primitive, so naively concatenating primitive traces yields a biased estimate of $\rho(c_1 ; c_2, \varphi)$ unless this mismatch is explicitly corrected.

Approach

Given a composite Scenic program $c$ and a non-Markovian specification $\varphi = (\mathcal{A}_\varphi, L)$, the framework returns $(\hat{\rho}(c, \varphi), \hat{\varepsilon})$ in four stages: (i) recursively parse the Scenic source into a composition graph over primitives $\mathcal{S}$; (ii) simulate $N$ traces per primitive in parallel; (iii) walk the graph, propagating a distribution over DFA states and correcting trace-distribution mismatch with kernel-density importance sampling; (iv) aggregate sibling branches by operator (product for sequential, weighted mixture for choose, permutation average for shuffle).

Scenic Frontend

Scenic’s composition vocabulary (do, do choose, do shuffle, and nested scenario blocks) maps directly onto the sequential, probabilistic-choice, and shuffle operators above, so a Scenic program already carries the compositional decomposition the analysis needs. The challenge is that composition in Scenic nests arbitrarily: a compose block can invoke another scenario whose body has further choose or shuffle clauses, and nested choose weights combine multiplicatively along invocation paths. For example, $\textsf{choose}\{A{:}0.5, M{:}0.5\}$ with $M = \textsf{choose}\{B{:}0.6, C{:}0.4\}$ is the three-way distribution $(A{:}0.5, B{:}0.3, C{:}0.2)$, not the two-way $(A{:}0.5, M{:}0.5)$ obtained by reading the outer choose in isolation. A flat parse loses this structure; recovering $\mathcal{D}_c$ requires a recursive traversal of the Scenic abstract syntax tree (AST) that preserves operator semantics and propagates weights across invocation boundaries.

The composite scenario is represented as a directed acyclic graph $G = (V, E)$ with $V = V_C \cup V_S \cup V_I$ partitioned into three node kinds. $V_C$ contains one container node per scenario or behavior definition; $V_S$ contains one statement node per do, do choose, or do shuffle clause, each carrying its operator label; $V_I$ contains one invocation node per call site, each carrying a target identifier and (under choose) a positive weight. Edges fall into three kinds: contains (a container to each of its statements), invokes (a statement to its invocations and each invocation to its target), and next (between sibling statements inside a container, encoding sequential order).

The DAG is then linearized into a list of CompositionStep values, where

$$\textsf{CompositionStep} \;=\; \mathcal{S} \;\cup\; \Bigl\{ f : \mathcal{S} \to [0, 1] \;\Big|\; \textstyle\sum_{s \in \mathcal{S}} f(s) = 1 \Bigr\}.$$

Sequential statements concatenate their children’s step lists; choose produces a single step that flattens the child step lists into a distribution by multiplying weights along the invocation path; shuffle over $k$ children yields the $k!$ permutation step lists with uniform weight $1/k!$.

VerifAI Backend

The backend extends VerifAI’s compositional analysis engine from the Markovian estimator of Yalcinkaya et al. to DFA safety specifications. A new automaton_specification class in VerifAI wraps the dfa library to represent a safety property as $\mathcal{A}_\varphi = (Q, \Sigma, \delta, q_0, F)$ with labeling $L : X \to \Sigma$, and extends the engine to consume it. It takes the linearized composition $C = (c_1, \dots, c_N)$ from the frontend, where each $c_i$ is either a primitive name (sequential step) or a weighted dictionary $\{s^{(j)} : p_j\}_j$ (random choice), along with the per-primitive trace pools $\mathcal{T}_s$ and entry/exit features $\phi_{\text{src}}, \phi_{\text{tgt}}$ (e.g., position, speed), and returns $(\hat{\rho}, \hat{\varepsilon})$ estimating $\Pr[\hat{\delta}(q_0, L(\tau)) \in F]$ over the composite distribution.

Three challenges shape the algorithm.

Non-Markovian satisfaction. The Markovian estimator labels each trace by $\mathbf{1}[L(x_T)]$; DFA satisfaction instead depends on the full labeled sequence and on the entry state. We maintain a distribution $q_{\text{dist}}^{(i)} \in \Delta(Q)$ over DFA entry states, conditioned across primitives on acceptance, and label each trace by

$$\ell_i(\tau) \;=\; \sum_{q \in Q} q_{\text{dist}}^{(i)}(q)\, \mathbf{1}\!\bigl[\hat{\delta}(q, L(\tau)) \in F\bigr].$$

The accept-conditioning is essential: advancing $q_{\text{dist}}^{(i)}$ over all step-$i$ traces (including ones already in absorbing rejecting states) deflates both $\hat{\rho}_i$ and $\hat{\rho}_{i+1}$, so $\prod_i \hat{\rho}_i$ underestimates the truth. We therefore compute the full sequence $\{q_{\text{dist}}^{(i)}\}_{i=1}^N$ in a forward pass over $C$ before the main estimation loop, so each step uses the correct pre-step distribution.

Handoff distribution mismatch. Each primitive is simulated standalone, so its entry distribution over $X$ differs from its predecessor’s exit distribution; naive concatenation is biased. We correct with self-normalized importance sampling: fit a Gaussian KDE $p_{\text{src}}^{(i)}$ to step $i{-}1$‘s accepting-exit features $\phi_{\text{tgt}}$ and $p_{\text{tgt}}^{(i)}$ to step $i$‘s entry features $\phi_{\text{src}}$, with

$$\tilde{w}_i(\tau) \;=\; \frac{p_{\text{src}}^{(i)}(\phi_{\text{src}}(\tau))}{p_{\text{tgt}}^{(i)}(\phi_{\text{src}}(\tau))}, \qquad w_i(\tau) \;=\; \tilde{w}_i(\tau) \,/\, {\textstyle\sum_{\tau'}} \tilde{w}_i(\tau').$$

The per-step estimate is the self-normalized IS-weighted mean $\hat{\rho}_i = \sum_\tau \tilde{w}_i(\tau)\, \ell_i(\tau) / \sum_\tau \tilde{w}_i(\tau)$. Near-disjoint supports collapse the weights, which we mitigate by prewarming primitives so successive supports overlap, and by monitoring effective sample size.

Random-choice composition. A step $c_i = \{s^{(j)} : p_j\}_j$ branches all three machinery components:

$$\hat{\rho}_i \;=\; \sum_j p_j\, \hat{\rho}_{i,j}, \qquad q_{\text{dist}}^{(i+1)} \;=\; \sum_j p_j\, \tilde{q}_{\text{dist}}^{(i+1), j},$$

where $\hat{\rho}_{i,j}$ is the per-branch IS estimate from a shared $q_{\text{dist}}^{(i)}$ and $\tilde{q}_{\text{dist}}^{(i+1), j}$ is its accept-conditioned successor. When step $i{+}1$ fits its source KDE, accepting-exit features are pooled across branches with weights $\propto p_j$, so the mixture mass is faithful rather than implicitly uniform.

Aggregation

The chain rule

$$\Pr\Bigl[\bigwedge_{i=1}^N \text{accept}_i\Bigr] \;=\; \prod_{i=1}^N \Pr[\text{accept}_i \mid \text{accept}_{<i}]$$

justifies multiplying per-step estimates into the composite estimate, with per-step Hoeffding bounds $\hat{\varepsilon}_i$ (using the effective sample size $N_{\text{eff}}$ of the importance weights) propagated as

$$\hat{\rho} \;=\; \prod_{i=1}^N \hat{\rho}_i, \qquad \hat{\varepsilon} \;=\; \hat{\rho}\sqrt{{\textstyle\sum_{i=1}^N} (\hat{\varepsilon}_i / \hat{\rho}_i)^2}, \qquad \hat{\varepsilon}_i^2 \;=\; {\textstyle\sum_j} p_j^2\, \hat{\varepsilon}_{i,j}^2.$$

A union bound over the $N$ per-step events with $\delta_i = \delta / N$ ensures the composite estimate holds at overall confidence $1, \delta$.

Results

We evaluate accuracy and efficiency against the monolithic SMC baseline (which simulates each composite as a single chained Scenic scenario) on three sets of scenarios in MetaDrive.

Accuracy at matched trace budget

Set A consists of five sequential composites $\{\text{SX}, \text{SXS}, \text{SC}, \text{SCS}, \text{SCX}\}$ over the primitives Straight, Intersection, Curve, evaluated under two DFAs: $\varphi_{\text{toll}}$ (rejects after the third near-stop) and $\varphi_{\text{stop}}$ (at most one near-stop). At a matched trace budget, the two estimators agree within Hoeffding intervals on every $(c, \varphi)$ pair.

Composite	$\hat{\rho}_{\text{mono}}$ ($\varphi_{\text{toll}}$)	$\hat{\rho}_{\text{comp}}$ ($\varphi_{\text{toll}}$)	$\hat{\rho}_{\text{mono}}$ ($\varphi_{\text{stop}}$)	$\hat{\rho}_{\text{comp}}$ ($\varphi_{\text{stop}}$)
SX	$0.702 \pm 0.061$	$0.727 \pm 0.092$	$0.650 \pm 0.061$	$0.692 \pm 0.097$
SXS	$0.664 \pm 0.061$	$0.713 \pm 0.108$	$0.600 \pm 0.061$	$0.687 \pm 0.114$
SC	$0.860 \pm 0.061$	$0.895 \pm 0.098$	$0.874 \pm 0.061$	$0.904 \pm 0.105$
SCS	$0.862 \pm 0.061$	$0.892 \pm 0.123$	$0.866 \pm 0.061$	$0.897 \pm 0.129$
SCX	$0.620 \pm 0.061$	$0.652 \pm 0.101$	$0.584 \pm 0.061$	$0.633 \pm 0.104$

Set B is the five-step wander composite $\textsf{Main} = 5 \times \textsf{choose}\{\textsf{GoStraight}, \textsf{TurnLeft}, \textsf{TurnRight}, \textsf{Brake}\}$, yielding $4^5 = 1024$ distinct execution paths over four leaf primitives. Under $\varphi_{\text{brake}}$ (rejects after the second hard brake), the compositional estimate $\hat{\rho}_{\text{comp}} = 0.868 \pm 0.051$ agrees with $\hat{\rho}_{\text{mono}} = 0.896 \pm 0.043$, with $|\Delta\hat{\rho}| = 0.028$ well inside both Hoeffding intervals. The same Set B primitive trace pool was additionally evaluated against seven further DFAs (including non-Markovian properties like rise_then_fall, k_consec_slow, at_most_one_brake) at ~1 s of post-hoc Python each, illustrating that compositional analysis decouples specifications from simulation.

Compositional point estimates land slightly above the monolithic baseline on Set A across all five composites, but the gap is within Hoeffding error in every row and shows no trend with composite length. This is evidence that the accept-conditioning fix in the backend is removing the dominant source of compositional drift, since residual multiplicative bias from un-conditioned rejection mass would grow with the number of primitives.

Efficiency at matched wall-clock budget

Set C is the two-step approach-then-turn composite $\textsf{Sub}_1 ; \textsf{choose}\{\textsf{Sub}_2^L, \textsf{Sub}_2^R, \textsf{Sub}_2^S\}$, evaluated under the Markovian safe_under_max spec to isolate the wall-clock comparison. Each method runs one continuous simulation up to $T_{\max} = 1800\,\text{s}$ and records per-primitive trace counts every $\Delta T = 30\,\text{s}$.

Reading the wall-clock ratio $T_{\text{mono}} / T_{\text{comp}}$ at fixed target precision off the left panel yields ≈ 4× at $\hat{\varepsilon}^\ast = 0.20$ and ≈ 7× at $\hat{\varepsilon}^\ast = 0.15$. Two structural advantages drive this. First, the compositional pipeline spawns one parallel worker per primitive ($\textsf{Sub}_1$ together with the three turning branches, four workers in total), while the monolithic pipeline runs a single worker on the chained behavior. Second, each primitive trace covers only one composition step and is therefore a factor of two shorter than a chained composite trace under matched horizons. A third structural advantage, trace-pool reuse across composites sharing the same primitives, is not exercised in this single-composite sweep but would compound the gap on a corpus of composites built from overlapping primitive sets.

Future Work

The framework as it stands handles flat safety DFAs, automata with an absorbing rejecting state where, once acceptance is lost, it cannot be recovered. The natural next step is bounded liveness via complementation: on finite traces of length $T$, a bounded-liveness property such as “the vehicle must exceed $v_{\max}$ at some point” equals $1, \rho(\neg\varphi)$, where $\neg\varphi$ is the flat safety property “the vehicle never exceeds $v_{\max}$ within the trace.” Appendix B of the report validates this empirically on a 4-way intersection composite ($\hat{\rho}_{\text{live}} = 0.586 \pm 0.060$ vs monolithic $0.607 \pm 0.078$), confirming the trick is sound when the negation is itself a flat safety DFA. This works because the DFA has only two states and bad is absorbing, so $\varphi_{\text{safe}}$ collapses to Markovian on the raw simulation state.

The trick does not generalize beyond the bounded-reachability fragment. Bounded-response (“within $k$ steps of $A$, observe $B$”), bounded-sequenced-reachability, bounded-persistence, and bounded-recurrence all negate to formulas with nested temporal operators rather than flat safety DFAs, and so cannot be reduced to a single absorbing-reject monitor. Compositional treatment of those classes requires either a product construction across multiple “live” DFA regions or, in the unbounded case, reasoning about infinite-suffix acceptance. A near-term path that stays within the present machinery is bounded response, which is expressible as a finite-window safety DFA and captures a large fraction of practical AV requirements without leaving the absorbing-reject framework.

Two further directions follow naturally. The current implementation lives as an extension of CompositionalAnalysisEngine; upstreaming the DFA monitor and Scenic parser into VerifAI proper would expose them to the existing falsifier pipeline. And the boundary-distribution overlap that compositional estimation requires is currently tuned by hand (spawn-distance and initial-speed calibration on Set A, randomized cruise prewarm on Set B); a diagnostic based on per-handoff effective sample size, paired with an automatic spawn/prewarm adjustment, would remove the manual calibration step and make the framework usable on new primitive libraries without per-scenario tuning.