Paper deep dive
Scenario-Based Compositional Statistical Model Checking for Safety Specifications
Abhinav Pomalapally, Arya Raeesi, Kevin Kai-Chun Chang, Beyazit Yalcinkaya, Sanjit A. Seshia
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract: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.
Tags
Links
- Source: https://arxiv.org/abs/2610.05571v1
- Canonical: https://arxiv.org/abs/2610.05571v1
Trouble viewing inline? Open PDF directly →
Full Text
50,663 characters extracted from source content.
Expand or collapse full text
Scenario-Based Compositional Statistical Model Checking for Safety Specifications Abhinav Pomalapally Arya Raeesi Kevin Kai-Chun Chang Beyazit Yalcinkaya Sanjit A. Seshia E-mail kaichunchang,beyazit,sseshia@berkeley.edu Affiliation: University of California, Berkeley, USA E-mail abhinav_pomalapally,aryaraeesi@berkeley.edu Abstract 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. Keywords: Statistical Model Checking Compositional Verification Scenario-Based Testing Safety Specifications Runtime Verification 1 Introduction Artificial intelligence (AI) systems are increasingly deployed in safety-critical domains, including autonomous driving, robotics, healthcare, and cyber-physical systems in general. As these systems become more pervasive, ensuring their safety and reliability remains a fundamental challenge. However, the complexity of modern AI-based systems renders traditional verification techniques largely inapplicable. Classical formal verification methods typically require an explicit and tractable model of the system under analysis, an assumption that is often violated in contemporary AI systems due to their inherent opacity. A practical alternative is to treat the system under analysis as a black box and reason about its behavior through simulation-based analysis [20]. This approach is particularly prevalent in autonomous driving, where validating a system through exhaustive real-world testing is infeasible. Instead, developers evaluate autonomous driving systems using a corpus of scenarios, either manually designed by domain experts or extracted from real-world driving data, and assess the system’s performance across these scenarios through repeated simulations. Statistical model checking (SMC) provides a principled framework for such simulation-based verification [16]. SMC is a formal verification technique that determines whether a stochastic system satisfies a given property within a particular scenario by analyzing a finite set of execution traces using statistical methods such as hypothesis testing or confidence interval estimation. By mitigating the state-space explosion associated with exhaustive model checking, SMC enables verification of systems whose complexity would otherwise make formal analysis intractable. Nevertheless, SMC continues to face significant scalability challenges. Obtaining meaningful and high-confidence verification results often requires executing a large number of computationally expensive, long-running simulations. Moreover, SMC must typically be repeated whenever the scenario defining the environment conditions changes, leading to redundant computation. In this paper, we introduce a scenario-based compositional SMC framework for safety and co-safety specifications, i.e., specifications whose violation or satisfaction can be determined from finite executions. Our approach leverages both scenario and specification decomposition. Given a composite scenario, we first decompose it into a collection of primitive scenarios. Simultaneously, we decompose the target safety specification into a set of sub-specifications. The black-box system is then evaluated independently on each primitive scenario with respect to all relevant sub-specifications. These verification tasks can be executed in parallel and require shorter simulation runs than the original monolithic verification problem. Finally, we compose the resulting statistical estimates to obtain a verification result for the original composite scenario and specification. Furthermore, our compositional framework enables the reuse of traces generated for primitive scenarios across multiple composite scenarios, thereby avoiding redundant simulation effort and significantly reducing overall verification cost. We summarize our contributions as follows: (i) we introduce a novel compositional statistical model checking framework for safety and co-safety specifications; (i) we implement the proposed framework and integrate it into VerifAI [9], a toolkit for the formal design and analysis of AI-based systems; and (i) we conduct an empirical evaluation of the proposed approach and demonstrate its effectiveness in improving verification efficiency while maintaining accuracy. Related Work. To address the verification of AI-based systems, simulation-based formal analysis has been widely adopted [20, 9, 1]. Specifically, statistical model checking (SMC) [18, 19, 25, 26, 16, 6, 27, 2] mitigates the state-space explosion of exact formal methods by evaluating a finite set of execution traces, providing probabilistic guarantees bounded by statistical confidence intervals. Seshia et al. [20] advocate for a compositional approach to scale up verification of AI systems. Classic compositional verification (e.g., [5, 7, 4, 14, 22]) is not directly applicable to simulation-based verification of AI systems. Existing compositional approaches for AI systems vary in their axes of decomposition; while some frameworks decompose internal system architectures or neural network layers [21, 10], our work focuses on the spatial and temporal decomposition of environmental scenarios and specifications. Dreossi et al. [8] has proposed a framework combining compositional analysis with simulation-based verification, but it focuses strictly on component-level decomposition and targets active falsification rather than SMC. The closest prior work to the proposed framework introduces a compositional approach to SMC [24]. However, it is strictly restricted to Markovian, i.e., memoryless, specifications. Our new framework extends compositional SMC to non-Markovian safety and co-safety specifications, overcoming a fundamental limitation. Another related line of work explores scenario decomposition, where environments and specifications are divided into primitive segments either spatially [23, 13] or temporally [3]. However, these differ significantly in their verification methods: they rely on explicit white-box access [13], offline probabilistic abstractions [23], or remain confined to falsification [3]. In contrast, our framework achieves black-box compositional SMC for safety and co-safety properties. 2 Motivating Example ((a)) ((b)) ((c)) ((d)) Figure 1: Primitive scenarios considered throughout the paper: a straight road segment (S), an intersection (X), a roundabout (O), and a curved road segment (C). Consider evaluating an autonomous vehicle across various driving scenarios (Figure 1). A common approach to constructing such scenarios is to use a set of simpler primitive scenarios as building blocks for defining more complex composite scenarios. Suppose that our primitive scenarios consist of a straight road segment (S), an intersection (X), a roundabout (O), and a curved road segment (C). Scenario description languages such as Scenic [11, 12] support this style of programmatic scenario construction through several composition operators. Sequential composition specifies the exact order in which scenarios are encountered (e.g., S → X). Choice composition randomly selects one scenario from a set of alternatives (e.g., choose(S,X,O,C) choose( S, X, O, C)). Finally, shuffle composition randomly permutes the order of a collection of scenarios (e.g., shuffle(S,X,O,C) shuffle( S, X, O, C)). Our goal is to efficiently test the autonomous vehicle in composite scenarios against safety and co-safety specifications, i.e., temporal specifications whose satisfaction or violation can be determined from a finite execution. A monolithic application of SMC treats each composite scenario independently. For every new scenario and specification pair, SMC executes a large number of simulations and analyzes the resulting traces. As the complexity of composite scenarios grows, this process quickly becomes computationally expensive, requiring repeated execution of long-running simulations that often share substantial structure. Our approach avoids this redundancy by shifting the computational effort to the primitive scenarios. Instead of directly evaluating every composite scenario, we execute the system independently within each primitive scenario and store the resulting traces. We then evaluate these traces against all sub-specifications induced by the target specification, corresponding to the sub-automata of its monitor automaton. Given a composite scenario, we compose the previously computed results to estimate the probability of satisfying the target specification. A key challenge is that the distribution of behaviors observed in an isolated primitive scenario may differ from the distribution induced when that same primitive appears as part of a larger composite scenario. To account for this distributional mismatch, we employ importance sampling [15] together with kernel density estimation (KDE). Intuitively, traces generated from primitive scenarios are weighted according to their likelihood under the target composite scenario. This enables us to estimate results for previously unseen composite scenarios without actually running the system in those scenarios. Consequently, our approach generates computationally efficient and highly accurate estimates for SMC queries. 3 Method In this section, we present our compositional approach for checking safety specifications. We assume that the controller under consideration is Markovian, i.e., it outputs actions that solely depend on the current state of the plant, and that it operates in a Markov Decision Process (MDP). A primitive scenario defines environment conditions from a set of initial states to a set of terminal states, e.g., the primitive scenario in starts at the car’s initial position and ends when the car leaves the intersection. A composite scenario is a composition of such primitives, e.g., S → X sequentially composes S and X, defining a scenario that starts at the beginning of a straight road and ends after an intersection. Let τ∼(π,)τ (π,S) denote a (labeled) trace sampled by running a policy π in a scenario S, let T be a finite set of such traces, and let ϕφ be a safety specification in automaton form. SMC estimates the specification satisfaction probability as: Pr[τ⊧ϕ]=1||∑τi∈τi⊧ϕ, [τ φ]= 1|T| _ _i 1\ _i φ\, (1) where τ⊧ϕτ φ denotes that the trace τ satisfies the safety specification ϕφ. Note that |||T| can be chosen via Hoeffding’s inequality to achieve a desired confidence level. We rewrite this expression in terms of the state distribution of the safety specification. Observe that for a safety specification ϕ=(Q,Σ,δ,q0,F)φ=(Q, ,δ,q_0,F), its state distribution μ0∈Δ(Q) _0∈ (Q) is initially concentrated at q0q_0, i.e., μ0(q0)=1 _0(q_0)=1, as q0q_0 is the initial state. Let μ _S denote the state distribution induced by transitioning the automaton using traces τ∼(π,)τ (π,S). μ _S summarizes execution history within each trace relevant to the specification, allowing our method to handle non-Markovian temporal properties through Markovian updates over automaton states. Therefore, we can rewrite Equation 1 as follows: Pr[τ⊧ϕ]=∑q∈Qδ∗(q,τ)∈Fμ0(q)=∑q∈Qq∈Fμ(q), [τ φ]= _q∈ Q 1\δ^*(q,τ)∈ F\ _0(q)= _q∈ Q 1\q∈ F\ _S(q), (2) where δ∗δ^* is the transitive closure of the automaton transition function δ. Observe that the expression in the middle marginalizes over all initial states using the initial state distribution μ0 _0, and the expression on the right marginalizes over all final states using the resulting output state distribution μ _S. Let q→q′T_q→ q denote the subset of the given traces T that ends at an automaton state q′q starting from an automaton state q. We can estimate μ _S using μ0 _0 and T as follows: μ(q′)=∑q∈Qμ0(q)1|q→q′|∑τi∈q→q′δ∗(q,τi)=q′. _S(q )= _q∈ Q _0(q) 1|T_q→ q | _ _i _q→ q 1\δ^*(q, _i)=q \. (3) This expression shows the one-step propagation rule for computing the resulting automaton state distribution after a scenario S. We emphasize that Equation 3 is not intended as a novel derivation; rather, it provides the empirical estimation needed to obtain the automaton state distribution induced by a scenario from the initial distribution and available traces. We use this idea to compositionally compute SMC queries for sequential, choose, and shuffle compositions. As co-safety specifications are the complement of safety specifications, given a co-safety specification ϕφ, we take its complement ϕ¯ φ which is a safety specification, run SMC, and take the complement of the resulting satisfaction probability, i.e., Pr[τ⊧ϕ]=1−Pr[τ⊧ϕ¯], [τ φ]=1- [τ φ], (4) where ϕ¯ φ is a safety specification, and Pr[τ⊧ϕ¯] [τ φ] is computed as in Equation 1. 3.1 Sequential Composition Consider the sequential composition S → X. Let ST S and XT X denote traces independently generated for the primitive scenarios S and X, respectively. Our goal is to use the primitive scenario traces ST S and XT X to estimate the satisfaction probability for the composite scenario S → X without actually generating traces for it. Let τS→Xτ S$→$ X, τSτ S, and τXτ X denote traces sampled for S → X, S, and X, respectively. Let μ0 _0 be the initial automaton state distributions, and let μS→X _ S$→$ X, μS _ S, and μX _ X denote the automaton state distribution induced by the scenarios S → X, S, and X, respectively. Using Equation 2, we can compute the SMC query as follows: Pr[τS→X⊧ϕ]=∑q∈Qq∈FμS→X(q). [τ S$→$ X φ]= _q∈ Q 1\q∈ F\ _ S$→$ X(q). (5) We can estimate μS→X _ S$→$ X using μS _ S and Equation 3 as follows: μS→X(q′)=∑q∈QμS(q)1|q→q′X|∑τi∈q→q′Xδ∗(q,τi)=q′oS,q(τi)ιX(τi), _ S$→$ X(q )= _q∈ Q _ S(q) 1|T X_q→ q | _ _i X_q→ q 1\δ^*(q, _i)=q \ o_ S,q( _i) _ X( _i), (6) where μS _ S is estimated recursively using μ0 _0 and Equation 3. Here, notice that XT X is generated using the initial MDP state distribution of X, denoted by ιX _ X, and the result we want is with respect to the induced output MDP state distribution of S for traces that end at the automaton state q (since we are marginalizing over q), denoted by oS,qo_ S,q. Therefore, we perform importance sampling to account for this distributional mismatch, given by the fraction at the end of the expression. This allows us to treat traces in XT X as if they were generated starting from the resulting output MDP state distribution of the preceding scenario S. Using this approach, we start from the initial state distribution and compute its evolution throughout the given sequential composition, i.e., μ0→SμS→XμS→X _0 S _ S X _ S$→$ X. Equation 6 is a valid decomposition of the monolithic SMC query due to the assumed Markovian dynamics of the underlying stochastic process, i.e., it is sufficient to account for the distributional mismatch between the last and the first MDP states of the scenarios S and X, respectively. In practice, it is crucial to ensure that the output and input MDP state distributions of sequentially composed scenarios like S and X overlap. We assume it to be the case, and thus, we only account for the distributional mismatch through importance sampling. As such, we estimate ιX _ X and oSo_ S using Gaussian kernel density estimation (KDE), an asymptotically valid nonparametric method. KDE performs well in moderate dimensions, whereas it might suffer from the curse of dimensionality in high-dimensional spaces. We expect to apply the proposed approach in moderately sized semantic feature spaces; therefore, for our purposes, KDE suffices. 3.2 Choose Composition Consider the choose composition choose(S,X) choose( S, X). Let τchoose(S,X)τ choose( S, X), τSτ S, and τXτ X denote traces sampled for the composite scenario and the corresponding primitive scenarios. The satisfaction probability can be written as a mixture distribution: Pr[τchoose(S,X)⊧ϕ]=12Pr[τS⊧ϕ]+12Pr[τX⊧ϕ]. [τ choose( S, X) φ]= 12 [τ S φ]+ 12 [τ X φ]. (7) Intuitively, the composite scenario induces a probabilistic choice over the constituent scenarios, and the overall satisfaction probability is obtained by marginalizing over the selected branch. This expression can be easily extended to n-ary and weighted choose compositions by marginalizing with branch probabilities. 3.3 Shuffle Composition Finally, consider the shuffle composition shuffle(S,X) shuffle( S, X), which randomly picks a permutation of the given scenarios to sequentially compose. Let τshuffle(S,X)τ shuffle( S, X) denote a trace sampled from it. We can decompose the SMC query as follows: Pr[τshuffle(S,X)⊧ϕ]=12Pr[τS→X⊧ϕ]+12Pr[τX→S⊧ϕ]. [τ shuffle( S, X) φ]= 12 [τ S$→$ X φ]+ 12 [τ X$→$ S φ]. (8) This can be trivially extended to n-ary and weighted shuffle compositions. While shuffle composition results in a factorial growth in the number of permutations, we expect the number of shuffled scenarios to remain relatively small. 4 Empirical Evaluation In this section, we empirically evaluate the proposed framework along two dimensions: accuracy and efficiency. To evaluate accuracy, we impose a fixed trace budget on both our compositional SMC approach and a monolithic SMC baseline, and compare the resulting satisfaction-probability estimates against those obtained by the baseline. To evaluate efficiency, we impose a fixed time budget, limiting both approaches to generating traces within the allotted time. We then compare the resulting estimates with their respective counterparts from the fixed-trace-budget experiment, assessing whether each approach can converge to accurate estimates under a limited data budget. This setting is particularly relevant during early-stage system development, when rapid feedback is valuable. We implemented the proposed framework11 1 Our code is at https://github.com/abhip02/VerifAI/tree/compositional-analysis. as a prototype integrated with VerifAI [9], a toolkit for the formal design and analysis of AI-based systems. We use MetaDrive [17] as the simulator and Scenic [11, 12] as the scenario description language. We test MetaDrive’s built-in expert policy, a neural controller trained to handle general driving scenarios. We evaluate the framework on seven composite scenarios: (i) S → X, (i) S → X → S, (i) S → O → C, (iv) C → S → X → S, (v) C → X → S → X → C, (vi) S → choose (C, X, O), and (vii) S → shuffle (C, X, O). These comprise five sequential compositions of varying lengths and two compositions using choose and shuffle. We consider four specifications: two safety properties, 2-Stop, which forbids more than one near-stop event, and Tollgate, which forbids remaining below a slow-speed threshold for more than three consecutive steps; and two co-safety properties, V-Shaped, which requires the ego to eventually complete a fast–slow–fast speed profile, and Sustained, which requires the ego to eventually sustain a large steering input for three consecutive steps. The four specifications are detailed in Appendix 0.A. This yields 2828 scenario–specification pairs, each evaluated in both experiments. 4.1 Evaluating Accuracy In the fixed-trace-budget experiment, we generate 10001000 composite scenario traces for the monolithic SMC baseline. For our compositional SMC method, we instead generate 10001000 traces for each primitive scenario and reuse these traces across all considered composite scenarios. Table 1: Estimated satisfaction probabilities for the Tollgate specification under the fixed-trace-budget regime. Scenario Monolithic SMC (baseline) Compositional SMC (ours) Δ S → X 0.67500.6750 0.70740.7074 +0.0324+0.0324 S → X → S 0.65200.6520 0.68980.6898 +0.0378+0.0378 S → O → C 0.43100.4310 0.47400.4740 +0.0430+0.0430 C → S → X → S 0.56700.5670 0.62060.6206 +0.0536+0.0536 C → X → S → X → C 0.38200.3820 0.38190.3819 −0.0001-0.0001 S → choose (C, X, O) 0.98000.9800 0.95840.9584 −0.0216-0.0216 S → shuffle (C, X, O) 0.91500.9150 0.89410.8941 −0.0209-0.0209 Table 1 presents results for the Tollgate specification as an example. The compositional estimates closely track the values reported by the monolithic baseline, demonstrating the accuracy of our compositional framework. We observe similar agreement for nearly all remaining scenario–specification pairs, as reported in Table 2 of Appendix 0.B. One notable exception is the Sustained specification for the S → shuffle (C, X, O) scenario, for which Δ reaches +0.1162+0.1162. This gap arises from MDP initial-state correlation discussed in Section 3.1: in the monolithic execution, each subsequent scenario begins from an MDP state the previous scenario left off at, whereas the compositional model samples each subsequent scenario from its own initial MDP state distribution. Although we use importance sampling to account for this distributional mismatch, the quality of the compositional estimate depends directly on the degree of overlap between the MDP state distributions at the interfaces of consecutive scenarios. This highlights that the initial state distributions of primitive scenarios must be chosen carefully to ensure accurate compositional estimates. One way we ensure this in our experiments is by simulating distinct geometries of the same primitive scenario to yield a representative state distribution. For example, we randomly sample four-way intersections on the same map with varying initial velocities and headings. By diversifying these initial conditions, we maximize the likelihood that state distributions overlap across scenario boundaries. Finally, note that the expert policy used in our experiments was not trained to satisfy any of the considered specifications; rather, it serves as a placeholder. 4.2 Evaluating Efficiency In the fixed-time-budget experiment, both the compositional approach and the monolithic baseline are given a 15-minute wall-clock budget for trace generation. Under this budget, the compositional estimates converge faster toward their respective fixed-trace-budget references than the monolithic baseline, with a mean deviation of 0.0290.029 versus 0.0390.039. This improvement is enabled by the compositional method generating 14.6×14.6× more traces on average (ranging from 5.2×5.2× to 32.3×32.3× more traces). Figure 2 shows a representative scenario–specification pair. Within the same wall-clock budget, the compositional method generates 14,87114,871 primitive traces, compared with 753753 monolithic traces. Full results are provided in Section 0.C.1. Figure 2: Fixed-time-budget convergence for the V-Shaped specification on the C → S → X → S scenario. 753753 monolithic and 1487114871 compositional traces generated within the 15-minute budget. The gap is concentrated among pairs involving choose/shuffle scenarios, where the per-trace cost is sufficiently high that the 15-minute budget yields as few as 2020 monolithic traces. The gap is largest for the ⟨ -Shaped, S → shuffle (C, X, O)⟩ pair, for which the monolithic estimate has an error of 0.2750.275 relative to the reference, compared with 0.0140.014 for the compositional approach. Even when the time budget is extended to 6060 minutes, the monolithic baseline still achieves an error of 0.1880.188, substantially higher than the error achieved by the compositional approach with only one quarter of the time budget (1515 minutes). Full results for the 6060-minute experiment are provided in Section 0.C.2. Finally, we conduct a compute-matched ablation in which the monolithic baseline retains the 15-minute budget, while the compositional approach receives an equal budget for each of the four primitive scenarios (S, X, O, C), yielding 225225 seconds per primitive. With the sample-count advantage removed, the two approaches are essentially tied, with mean deviations of 0.0380.038 and 0.0390.039, respectively, across the 2828 scenario–specification pairs. This result further validates that the primary benefit of our approach comes from sample reuse: a single pool of primitive traces can serve all composite scenarios, whereas the monolithic baseline must regenerate traces independently for each composite scenario. Full results are provided in Section 0.C.3. 5 Conclusion We presented a scenario-based compositional statistical model checking framework for safety and co-safety specifications. By decomposing composite scenarios into primitive scenarios and specifications into sub-specifications, our approach enables independent verification of primitive scenarios whose results are then composed using importance sampling and kernel density estimation to answer SMC queries about previously unseen composite scenarios. The framework supports sequential, choose, and shuffle compositions. Our empirical evaluation demonstrates that the proposed approach produces accurate estimates while reducing simulation cost through parallelization and trace reuse—a particularly valuable property in early-stage development when rapid feedback is essential. Acknowledgements This work was partially supported by the DARPA TIAMAT program, NSF grant 2303564, the California Partners for Advanced Transportation Technology (PATH) Future Mobility Research Center (FMRC), and Nissan through the iCyPhy Center. This work originated as a class project in EECS 219C at UC Berkeley. References [1] H. Abbas, G. Fainekos, S. Sankaranarayanan, F. Ivančić, and A. Gupta (2013) Probabilistic temporal logic falsification of cyber-physical systems. ACM Transactions on Embedded Computing Systems (TECS) 12 (2s), p. 1–30. Cited by: §1. [2] G. Agha and K. Palmskog (2018) A survey of statistical model checking. ACM Transactions on Modeling and Computer Simulation (TOMACS) 28 (1), p. 1–39. Cited by: §1. [3] K. K. Chang, K. Xu, E. Kim, A. Sangiovanni-Vincentelli, and S. A. Seshia (2024) Dynamic, multi-objective specification and falsification of autonomous CPS. In International Conference on Runtime Verification (RV), p. 40–58. Cited by: §1. [4] C. Chilton, B. Jonsson, and M. Kwiatkowska (2014) Compositional assume–guarantee reasoning for input/output component theories. Science of Computer Programming 91, p. 115–137. Cited by: §1. [5] E.M. Clarke, D.E. Long, and K.L. McMillan (1989) Compositional model checking. In 4th Annual Symposium on Logic in Computer Science (LICS), p. 353–362. Cited by: §1. [6] E. M. Clarke and P. Zuliani (2011) Statistical model checking for cyber-physical systems. In International symposium on automated technology for verification and analysis (ATVA), p. 1–12. Cited by: §1. [7] J. M. Cobleigh, D. Giannakopoulou, and C. S. Păsăreanu (2003) Learning assumptions for compositional verification. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), p. 331–346. Cited by: §1. [8] T. Dreossi, A. Donzé, and S. A. Seshia (2019) Compositional falsification of cyber-physical systems with machine learning components. Journal of Automated Reasoning 63 (4), p. 1031–1053. Cited by: §1. [9] T. Dreossi, D. J. Fremont, S. Ghosh, E. Kim, H. Ravanbakhsh, M. Vazquez-Chanlatte, and S. A. Seshia (2019) VerifAI: a toolkit for the formal design and analysis of artificial intelligence-based systems. In International Conference on Computer Aided Verification (CAV), p. 432–442. Cited by: §1, §1, §4. [10] H. Duong, D. Shriver, T. Nguyen, and M. Dwyer (2025) Compositional neural network verification via assume-guarantee reasoning. Advances in Neural Information Processing Systems (NeurIPS) 38, p. 64158–64182. Cited by: §1. [11] D. J. Fremont, T. Dreossi, S. Ghosh, X. Yue, A. L. Sangiovanni-Vincentelli, and S. A. Seshia (2019) Scenic: a language for scenario specification and scene generation. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), p. 63–78. Cited by: §2, §4. [12] D. J. Fremont, E. Kim, T. Dreossi, S. Ghosh, X. Yue, A. L. Sangiovanni-Vincentelli, and S. A. Seshia (2023) Scenic: a language for scenario specification and data generation. Machine Learning 112 (10), p. 3805–3849. Cited by: §2, §4. [13] R. Ivanov, K. Jothimurugan, S. Hsu, S. Vaidya, R. Alur, and O. Bastani (2021) Compositional learning and verification of neural network controllers. ACM Transactions on Embedded Computing Systems (TECS) 20 (5s), p. 1–26. Cited by: §1. [14] S. Junges and M. T. Spaan (2022) Abstraction-refinement for hierarchical probabilistic models. In International Conference on Computer Aided Verification (CAV), p. 102–123. Cited by: §1. [15] T. Kloek and H. K. Van Dijk (1978) Bayesian estimates of equation system parameters: an application of integration by monte carlo. Econometrica: Journal of the Econometric Society, p. 1–19. Cited by: §2. [16] A. Legay, B. Delahaye, and S. Bensalem (2010) Statistical model checking: an overview. In International conference on runtime verification (RV), p. 122–135. Cited by: §1, §1. [17] Q. Li, Z. Peng, L. Feng, Q. Zhang, Z. Xue, and B. Zhou (2022) MetaDrive: composing diverse driving scenarios for generalizable reinforcement learning. IEEE transactions on pattern analysis and machine intelligence (TPAMI) 45 (3), p. 3461–3475. Cited by: §4. [18] K. Sen, M. Viswanathan, and G. Agha (2004) Statistical model checking of black-box probabilistic systems. In International Conference on Computer Aided Verification (CAV), p. 202–215. Cited by: §1. [19] K. Sen, M. Viswanathan, and G. Agha (2005) On statistical model checking of stochastic systems. In International conference on computer aided verification (CAV), p. 266–280. Cited by: §1. [20] S. A. Seshia, D. Sadigh, and S. S. Sastry (2022) Toward verified artificial intelligence. Communications of the ACM 65 (7), p. 46–55. Cited by: §1, §1. [21] E. Vin, K. A. Miller, I. Incer, S. A. Seshia, and D. J. Fremont (2025) ScenicProver: a framework for compositional probabilistic verification of learning-enabled systems. arXiv preprint arXiv:2511.02164. Cited by: §1. [22] K. Watanabe, C. Eberhart, K. Asada, and I. Hasuo (2023) Compositional probabilistic model checking with string diagrams of MDPs. In International Conference on Computer Aided Verification (CAV), p. 40–61. Cited by: §1. [23] C. Watson, R. Alur, D. Gopinath, R. Mangal, and C. S. Păsăreanu (2025) Scenario-based compositional verification of autonomous systems with neural perception. In International Symposium on AI Verification (SAIV), p. 3–28. Cited by: §1. [24] B. Yalcinkaya, H. Torfah, D. J. Fremont, and S. A. Seshia (2023) Compositional simulation-based analysis of ai-based autonomous systems for markovian specifications. In International Conference on Runtime Verification (RV), p. 191–212. Cited by: §1. [25] H. L. Younes, M. Kwiatkowska, G. Norman, and D. Parker (2006) Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer 8 (3), p. 216–228. Cited by: §1. [26] H. L. Younes and R. G. Simmons (2006) Statistical probabilistic model checking with a focus on time-bounded properties. Information and Computation 204 (9), p. 1368–1409. Cited by: §1. [27] P. Zuliani, A. Platzer, and E. M. Clarke (2013) Bayesian statistical model checking with application to stateflow/simulink verification. Formal Methods in System Design 43 (2), p. 338–367. Cited by: §1. Appendix 0.A Formal Specifications Figure 3 illustrates the four specifications used in the experiments. q0q_0q1q_1q⊥q_ v≥3.5v≥ 3.5v<3.5v<3.5v≥3.5v≥ 3.5v<3.5v<3.5∗ ((a)) q0q_0q1q_1q2q_2q⊥q_ v≥3.5v≥ 3.5v<3.5v<3.5v<3.5v<3.5v<3.5v<3.5v≥3.5v≥ 3.5v≥3.5v≥ 3.5∗ ((b)) q0q_0q1q_1q2q_2qFq_Fv<7v<7v≥7v≥ 7v>3.5v>3.5v≤3.5v≤ 3.5v<7v<7v≥7v≥ 7∗ ((c)) q0q_0q1q_1q2q_2q3q_3qFq_F|δ|≤0.2|δ|≤ 0.2|δ|>0.2|δ|>0.2|δ|>0.2|δ|>0.2|δ|≤0.2|δ|≤ 0.2|δ|≤0.2|δ|≤ 0.2|δ|≤0.2|δ|≤ 0.2∗ ((d)) 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, q0q_0 is the initial state, and ∗ marks a self-loop on any symbol. Appendix 0.B Full Accuracy Results This section presents the full experimental results corresponding to Section 4.1. 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. Scenario Monolithic Compositional Δ 2-Stop (safety) S → X 0.66500.6650 0.67120.6712 +0.0062+0.0062 S → X → S 0.60000.6000 0.67000.6700 +0.0700+0.0700 S → O → C 0.38900.3890 0.45110.4511 +0.0621+0.0621 C → S → X → S 0.53800.5380 0.61560.6156 +0.0776+0.0776 C → X → S → X → C 0.35500.3550 0.38490.3849 +0.0299+0.0299 S → choose (C, X, O) 0.97700.9770 0.95110.9511 −0.0259-0.0259 S → shuffle (C, X, O) 0.89100.8910 0.87750.8775 −0.0135-0.0135 Tollgate (safety) S → X 0.67500.6750 0.70740.7074 +0.0324+0.0324 S → X → S 0.65200.6520 0.68980.6898 +0.0378+0.0378 S → O → C 0.43100.4310 0.47400.4740 +0.0430+0.0430 C → S → X → S 0.56700.5670 0.62060.6206 +0.0536+0.0536 C → X → S → X → C 0.38200.3820 0.38190.3819 −0.0001-0.0001 S → choose (C, X, O) 0.98000.9800 0.95840.9584 −0.0216-0.0216 S → shuffle (C, X, O) 0.91500.9150 0.89410.8941 −0.0209-0.0209 V-Shaped (co-safety) S → X 0.35800.3580 0.33270.3327 −0.0253-0.0253 S → X → S 0.39300.3930 0.35240.3524 −0.0406-0.0406 S → O → C 0.55700.5570 0.57840.5784 +0.0214+0.0214 C → S → X → S 0.47200.4720 0.41940.4194 −0.0526-0.0526 C → X → S → X → C 0.61500.6150 0.65770.6577 +0.0427+0.0427 S → choose (C, X, O) 0.01300.0130 0.04150.0415 +0.0285+0.0285 S → shuffle (C, X, O) 0.32500.3250 0.31010.3101 −0.0149-0.0149 Sustained (co-safety) S → X 0.56800.5680 0.53050.5305 −0.0375-0.0375 S → X → S 0.62800.6280 0.54790.5479 −0.0801-0.0801 S → O → C 0.96300.9630 0.99600.9960 +0.0330+0.0330 C → S → X → S 0.71800.7180 0.66120.6612 −0.0568-0.0568 C → X → S → X → C 0.84200.8420 0.87290.8729 +0.0309+0.0309 S → choose (C, X, O) 0.25500.2550 0.23770.2377 −0.0173-0.0173 S → shuffle (C, X, O) 0.31000.3100 0.42620.4262 +0.1162+0.1162 Appendix 0.C Full Efficiency Results This section presents the complete experimental results corresponding to Section 4.2. We evaluate efficiency under three settings: (i) both the compositional approach and the monolithic baseline are given a 15-minute wall-clock budget for trace generation (Section 0.C.1), (i) both approaches are given a 60-minute wall-clock budget for trace generation (Section 0.C.2), and (i) a compute-matched ablation in which the monolithic baseline retains the 15-minute budget, while the compositional approach receives an equal budget for each of the four primitive scenarios (S, X, O, C), yielding 225225 seconds per primitive (Section 0.C.3). 0.C.1 15-Minute Time-Budget Experiments Table 3 reports the compositional and monolithic estimates under a fixed 15-minute time budget for all 28 specification–scenario cells, and Figures 4 to 7 show how these estimates converge as the budget grows. 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. Monolithic Compositional Scenario N ρ N ρ Δ Two-stop (safety) S → X 23472347 0.64120.6412 1226212262 0.65580.6558 +0.0146+0.0146 S → X → S 16181618 0.60570.6057 1226212262 0.65330.6533 +0.0476+0.0476 S → O → C 788788 0.38200.3820 1233512335 0.44100.4410 +0.0590+0.0590 C → S → X → S 753753 0.56180.5618 1487114871 0.58920.5892 +0.0275+0.0275 C → X → S → X → C 460460 0.32170.3217 1487114871 0.35470.3547 +0.0330+0.0330 S → choose (C, X, O) 4949 1.00001.0000 312312 0.96760.9676 −0.0324-0.0324 S → shuffle (C, X, O) 2020 0.95000.9500 312312 0.90620.9062 −0.0438-0.0438 Tollgate (safety) S → X 23472347 0.68600.6860 1226212262 0.67920.6792 −0.0068-0.0068 S → X → S 16181618 0.65080.6508 1226212262 0.67700.6770 +0.0262+0.0262 S → O → C 788788 0.42260.4226 1233512335 0.46380.4638 +0.0412+0.0412 C → S → X → S 753753 0.60690.6069 1487114871 0.61950.6195 +0.0126+0.0126 C → X → S → X → C 460460 0.36300.3630 1487114871 0.39220.3922 +0.0292+0.0292 S → choose (C, X, O) 4949 1.00001.0000 312312 0.97690.9769 −0.0231-0.0231 S → shuffle (C, X, O) 2020 0.95000.9500 312312 0.93220.9322 −0.0178-0.0178 V-shaped (co-safety, reported as 1−ρ1-ρ) S → X 23472347 0.37750.3775 1226212262 0.34670.3467 −0.0308-0.0308 S → X → S 16181618 0.40170.4017 1226212262 0.36890.3689 −0.0328-0.0328 S → O → C 788788 0.57990.5799 1233512335 0.58600.5860 +0.0061+0.0061 C → S → X → S 753753 0.44490.4449 1487114871 0.43800.4380 −0.0069-0.0069 C → X → S → X → C 460460 0.67830.6783 1487114871 0.67780.6778 −0.0005-0.0005 S → choose (C, X, O) 4949 0.02040.0204 312312 0.02060.0206 +0.0002+0.0002 S → shuffle (C, X, O) 2020 0.60000.6000 312312 0.29640.2964 −0.3036-0.3036 Sustained (co-safety, reported as 1−ρ1-ρ) S → X 23472347 0.56840.5684 1226212262 0.49600.4960 −0.0724-0.0724 S → X → S 16181618 0.61930.6193 1226212262 0.51670.5167 −0.1025-0.1025 S → O → C 788788 0.96570.9657 1233512335 0.99540.9954 +0.0296+0.0296 C → S → X → S 753753 0.68660.6866 1487114871 0.64650.6465 −0.0401-0.0401 C → X → S → X → C 460460 0.85650.8565 1487114871 0.86270.8627 +0.0062+0.0062 S → choose (C, X, O) 4949 0.20410.2041 216216 0.08130.0813 −0.1228-0.1228 S → shuffle (C, X, O) 2020 0.55000.5500 216216 0.24390.2439 −0.3061-0.3061 ((a)) ((b)) ((c)) ((d)) ((e)) ((f)) ((g)) Figure 4: 15-minute time-budget results for the 2-Stop specification. NmN_m and NcN_c are the number of monolithic and compositional primitive traces generated within the budget. ((a)) ((b)) ((c)) ((d)) ((e)) ((f)) ((g)) Figure 5: 15-minute time-budget results for the Tollgate specifications. NmN_m and NcN_c are the number of monolithic and compositional primitive traces generated within the budget. ((a)) ((b)) ((c)) ((d)) ((e)) ((f)) ((g)) Figure 6: 15-minute time-budget results for the V-Shaped specification. NmN_m and NcN_c are the number of monolithic and compositional primitive traces generated within the budget. ((a)) ((b)) ((c)) ((d)) ((e)) ((f)) ((g)) Figure 7: 15-minute time-budget results for the Sustained specification. NmN_m and NcN_c are the number of monolithic and compositional primitive traces generated within the budget. As described in Section 4.2, the monolithic estimate deviates from each method’s own fixed-trace-budget reference (Table 2) by 0.0390.039 against 0.0290.029 for the compositional one. The gap is concentrated among scenarios involving choose and shuffle (0.0890.089 vs. 0.0590.059), where the 1515-minute monolithic budget buys as few as 2020 traces. 0.C.2 60-Minute Time-Budget Experiments To obtain a sharper monolithic baseline for the sample-starved choose/shuffle scenarios, we increase the time budget to 60 minutes. Table 4 reports the resulting estimates and Figure 8 shows their convergence. 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. Monolithic Compositional Scenario N ρ N ρ Δ Two-stop (safety) S → choose (C, X, O) 188188 0.97340.9734 11611161 0.95030.9503 −0.0231-0.0231 S → shuffle (C, X, O) 7676 0.92110.9211 11611161 0.87950.8795 −0.0415-0.0415 Tollgate (safety) S → choose (C, X, O) 188188 0.97870.9787 11611161 0.95680.9568 −0.0219-0.0219 S → shuffle (C, X, O) 7676 0.92110.9211 11611161 0.89640.8964 −0.0246-0.0246 V-shaped (co-safety, reported as 1−ρ1-ρ) S → choose (C, X, O) 188188 0.05320.0532 11611161 0.05090.0509 −0.0023-0.0023 S → shuffle (C, X, O) 7676 0.51320.5132 11611161 0.34900.3490 −0.1642-0.1642 Sustained steering (co-safety, reported as 1−ρ1-ρ) S → choose (C, X, O) 188188 0.22340.2234 816816 0.12290.1229 −0.1005-0.1005 S → shuffle (C, X, O) 7676 0.51320.5132 816816 0.36650.3665 −0.1467-0.1467 ((a)) ((b)) ((c)) ((d)) ((e)) ((f)) ((g)) ((h)) Figure 8: 60-minute time-budget results on the choose/shuffle scenarios. Figures (a)–(d) are the two safety specifications (2-Stop, Tollgate). Figures (e)–(h) are the two co-safety specifications (V-shaped, Sustained), reported as 1−ρ1-ρ. NmN_m and NcN_c are the number of monolithic and compositional primitive traces generated within the budget. With four times the budget, the monolithic estimate becomes more accurate but still does not catch up. Averaged across the eight scenario–specification pairs, its deviation from the reference decreases from 0.0890.089 at 1515 minutes to 0.0630.063, whereas the compositional deviation drops from 0.0590.059 to 0.0290.029, leaving the monolithic estimate roughly twice as far from the reference. The remaining gap is concentrated in the two co-safety shuffle pairs: even at Nm=76N_m=76, the monolithic estimate remains 0.1880.188 (V-Shaped) and 0.2030.203 (Sustained) from its reference, compared with 0.0390.039 and 0.0600.060, respectively, for the compositional method. For V-Shaped shuffle, whose two reference values differ by only 0.0150.015, this provides a clear convergence comparison: the compositional estimate is already within 0.0390.039 of the shared reference value, while the 6060-minute monolithic run remains 0.1880.188 away. 0.C.3 Compute-Matched Ablation A natural concern is whether the compositional method’s advantage is genuine or merely a consequence of sample count: within a fixed wall-clock window it generates many short primitive traces, whereas the monolithic baseline generates only a few long ones. To control for this, we level the comparison by giving both methods the same total simulation budget rather than the same wall-clock time, charging the compositional method only the cost of generating a single monolithic scenario and asking whether it still recovers the same estimates. Each primitive pool PiP_i (i=1,…,ki=1,…,k) contains NiN_i traces generated within budget T, equal to the budget for one monolithic scenario. Splitting the same budget evenly across the k primitives allocates T/kT/k to each. Assuming a roughly constant per-trace cost, this corresponds to the first ⌊Ni/k⌋ N_i/k traces in each pool. We therefore truncate every pool to this prefix, preserving a total budget of T while leaving the estimator unchanged. 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. Monolithic Compositional (matched) Scenario N ρ N ρ Δ Two-stop (safety) S → X 23472347 0.64120.6412 30643064 0.64820.6482 +0.0070+0.0070 S → X → S 16181618 0.60570.6057 30643064 0.64590.6459 +0.0402+0.0402 S → O → C 788788 0.38200.3820 30823082 0.46170.4617 +0.0797+0.0797 C → S → X → S 753753 0.56180.5618 37163716 0.57810.5781 +0.0163+0.0163 C → X → S → X → C 460460 0.32170.3217 37163716 0.34220.3422 +0.0205+0.0205 S → choose (C, X, O) 4949 1.00001.0000 7777 0.96230.9623 −0.0377-0.0377 S → shuffle (C, X, O) 2020 0.95000.9500 7777 0.89050.8905 −0.0595-0.0595 Tollgate (safety) S → X 23472347 0.68600.6860 30643064 0.67360.6736 −0.0124-0.0124 S → X → S 16181618 0.65080.6508 30643064 0.67140.6714 +0.0206+0.0206 S → O → C 788788 0.42260.4226 30823082 0.48370.4837 +0.0611+0.0611 C → S → X → S 753753 0.60690.6069 37163716 0.60860.6086 +0.0017+0.0017 C → X → S → X → C 460460 0.36300.3630 37163716 0.37980.3798 +0.0168+0.0168 S → choose (C, X, O) 4949 1.00001.0000 7777 0.96230.9623 −0.0377-0.0377 S → shuffle (C, X, O) 2020 0.95000.9500 7777 0.89050.8905 −0.0595-0.0595 V-shaped (co-safety, reported as 1−ρ1-ρ) S → X 23472347 0.37750.3775 30643064 0.35100.3510 −0.0265-0.0265 S → X → S 16181618 0.40170.4017 30643064 0.37550.3755 −0.0262-0.0262 S → O → C 788788 0.57990.5799 30823082 0.55800.5580 −0.0219-0.0219 C → S → X → S 753753 0.44490.4449 37163716 0.44830.4483 +0.0034+0.0034 C → X → S → X → C 460460 0.67830.6783 37163716 0.68950.6895 +0.0112+0.0112 S → choose (C, X, O) 4949 0.02040.0204 7777 0.03460.0346 +0.0142+0.0142 S → shuffle (C, X, O) 2020 0.60000.6000 7777 0.30450.3045 −0.2955-0.2955 Sustained (co-safety, reported as 1−ρ1-ρ) S → X 23472347 0.56840.5684 30643064 0.49220.4922 −0.0762-0.0762 S → X → S 16181618 0.61930.6193 30643064 0.51400.5140 −0.1053-0.1053 S → O → C 788788 0.96570.9657 30823082 0.99750.9975 +0.0318+0.0318 C → S → X → S 753753 0.68660.6866 37163716 0.61910.6191 −0.0675-0.0675 C → X → S → X → C 460460 0.85650.8565 37163716 0.83890.8389 −0.0176-0.0176 S → choose (C, X, O) 4949 0.20410.2041 5353 0.03330.0333 −0.1708-0.1708 S → shuffle (C, X, O) 2020 0.55000.5500 5353 0.10000.1000 −0.4500-0.4500 With the budget split evenly across the k primitive pools (here, k=4k=4, yielding 225225 seconds per pool), the compositional advantage in raw sample count disappears, yet its accuracy remains essentially unchanged. Relative to their respective 1,0001,000-trace references (Table 2), the compositional and monolithic estimates achieve nearly identical mean deviations across the 2828 pairs: 0.0380.038 and 0.0390.039, respectively. Thus, the compositional method retains its accuracy without relying on additional traces, while a single truncated primitive pool can still be reused across all composite scenarios, unlike the monolithic baseline, which must regenerate traces from scratch for each scenario.