Querying Labeled Time Series Data with Scenario Programs

AI summary

Overview

Research area: Formal methods, cyber-physical systems (CPS), autonomous vehicle (AV) safety, simulation-based testing, and probabilistic programming languages (specifically Scenic).

Technical level: Advanced. The paper relies on formal semantics, satisfiability modulo theories (SMT) with non-linear real arithmetic and linear integer arithmetic, hierarchical finite state machines (HFSMs), and probabilistic programming concepts.

Scope: The paper defines a formal notion of when labeled time series sensor data "matches" an abstract AV scenario expressed in Scenic, and presents a sound query algorithm that retrieves the matching subset of a labeled dataset, validated experimentally against commercial vision large language models (VLMs).

What This Paper Is About

Simulation-based testing finds failure scenarios for autonomous systems, but because synthetic sensor data differs from real sensor data (the "sim-to-real gap"), it is unclear whether those simulated failures are reproducible on real systems. This paper addresses that question by treating the scenario as a formal Scenic program and automatically querying large labeled real-world time series datasets (e.g., video) to find real instances that match the scenario. The goal is to determine whether a candidate failure discovered in simulation also exists in real data, without the labor-intensive step of physically reconstructing the scenario on a test track.

Key Contributions

1. A novel problem formulation of querying a labeled time series dataset against a formal scenario model. The formulation is applicable to sensor data of any type (e.g., RGB, LiDAR, radar) provided the data is appropriately labeled, and it defines "matching" as a membership problem over traces of a Scenic program.

2. A sound query algorithm for a fragment of Scenic. The algorithm translates Scenic behaviors into a synchronous composition of hierarchical finite state machines (HFSMs) and checks whether the HFSMs accept a trace consistent with the label trace. The paper proves a correctness guarantee (Theorem 4.1): the algorithm outputs True if and only if the label trace matches the program for a window of length m.

3. A translation and tooling methodology: a syntax-directed translation from the supported Scenic fragment to HFSMs, an SMT-based object-correspondence search (using linear integer arithmetic), and an SMT-based guard evaluation (using non-linear real arithmetic) for memoryless behaviors.

4. Experiments showing that the algorithm is more accurate and orders of magnitude faster in querying scenarios than state-of-the-art commercial vision large language models, and can scale linearly with the duration of queried time series data.

Main Findings

• Query formulation as membership: A label trace is defined to match a Scenic program if the initial scene is in the support of the program's initial distribution and the action trace is in the distribution of output traces generated by the program given the input trace. A set of traces matches the program if their intersection is non-empty.

• Higher accuracy than VLMs: The abstract reports the algorithm is more accurate than state-of-the-art commercial vision large language models when querying scenarios. No specific accuracy figures or benchmark names are reported in the provided content.

• Orders-of-magnitude speedup: The abstract reports the algorithm is orders of magnitude faster than state-of-the-art VLMs. The specific numeric speedup is not reported in the provided content.

• Linear scaling with video duration: The abstract states the algorithm can scale linearly with the duration of queried time series data.

• Ambiguity and guarantees: The paper argues that natural-language queries to VLMs can be ambiguous and offer no accuracy guarantees, whereas Scenic provides expressive modeling with precise semantics and the query algorithm provides a correctness guarantee.

• Supported Scenic fragment: The methodology supports Scenic's operators for scalar, boolean, orientation, vector, and region types, plus position and orientation specifiers, and the statements require boolean, do behavior, do behavior until, and try/interrupt, with distributions Uniform, Range, Normal, and TruncatedNormal. Variable assignments are restricted so that behaviors are memoryless.

• Running example: The illustrative Scenic program models an ego car following a lane and changing lanes to avoid a stationary otherCar in front, with a lane-change trigger based on a distance uniformly sampled from Range(1,15) meters.

Methodology in Plain English

The researchers take a scenario written in Scenic—a language that describes objects, their initial configurations, and their probabilistic behaviors—and turn it into a formal machine model. Each behavior in the program becomes a hierarchical finite state machine (HFSM), where the discrete "primitive behaviors" (such as follow lane, lane change, stationary) become base states. The translation is syntax-directed: the Scenic program is parsed into an abstract syntax tree, then mapped onto HFSMs in a way that preserves the hierarchical structure of do...until, sequential, and try/interrupt constructs.

To query a dataset, the algorithm needs to know which objects in the labeled trace correspond to which objects in the program, but this mapping is unknown up front. The algorithm therefore encodes object correspondence as an SMT formula using linear integer arithmetic, pruning infeasible matches by object type and minimum observation duration, and iterates over satisfying correspondences.

For each correspondence, the algorithm slides a window of length m across the label trace. It first checks whether the window's initial input is in the support of the program's initial distribution (using a method from the authors' prior work). If that passes, it steps the HFSMs timestep by timestep: guards are encoded as SMT formulas with non-linear real arithmetic, evaluated by an SMT solver, and states transition where guards are true. After transitioning, the set of outputs from each object's HFSM is intersected with the observed outputs in the label trace, and base states whose outputs are inconsistent are pruned. If any object's feasible set becomes empty at any timestep, that window is a mismatch; if all timesteps of a window succeed, the trace matches. Unobserved variables—such as the Range(1,15) distance threshold in the example—are handled by encoding their domain into the guard formula, which allows non-deterministic transitions where multiple primitive behaviors are feasible.

Why This Matters

Impact on research: The work reframes sim-to-real validation as a formal query problem over real labeled data, connecting formal methods (Scenic, SMT) with the large real-world datasets now being collected for training autonomous systems. It provides a soundness guarantee that natural-language VLM querying cannot offer, and its formulation is sensor-type agnostic.

Real-world applications:

• Validating whether AV failure scenarios found in simulation also occur in real driving data before investing in track testing.
• Verifying that supposedly rare safety-critical scenarios are actually represented in a training dataset, and flagging when a scenario is absent.
• Retrieving specific temporal behaviors (not just static object presence) from large labeled video or sensor archives.
• Supporting perception, behavior prediction, and planning validation tasks in autonomous driving pipelines, where the authors note the algorithm can be applied.

Industry relevance: Companies that collect and label large-scale driving datasets and rely on simulation for safety assessment could use this approach to triage which simulated failures deserve physical testing. The rejected baseline is state-of-the-art commercial vision large language models, indicating direct relevance to industry practice around VLM-based video understanding.

Future Directions

• Extending the supported Scenic fragment: The current methodology restricts statement types and disallows variable assignments, making behaviors memoryless. Supporting stateful behaviors would broaden the class of scenarios that can be queried.
• Choosing the window length m: The paper notes m must be carefully chosen by a user, since too small an m (e.g., m = 1) may return many traces that match for a single timestep but not for most of the trace. A principled way to select m is an open question.
• Scaling to larger correspondences and datasets: The algorithm searches combinatorially over object correspondences via SMT; how it behaves with many objects or very long traces is a natural extension question.
• Applying to additional sensor modalities: Although the formulation is sensor-agnostic, the experiments in the provided content focus on video; validating the approach on LiDAR, radar, and other labeled modalities remains a direction.

Target Audience

Researchers and practitioners in autonomous vehicle safety, formal methods, and cyber-physical systems who are working on simulation-based testing, sim-to-real validation, or scenario specification. It will also interest engineers building dataset query and retrieval systems for labeled sensor data, and readers familiar with Scenic, SMT solving, or finite state machine models who want a rigorous alternative to natural-language querying with vision language models. Readers without a background in formal semantics or probabilistic programming will find the paper challenging.

Authors’ abstract

Simulation-based testing has become a crucial complement to road testing for ensuring the safety of cyber physical systems (CPS). As a result, significant research efforts have been directed toward identifying failure scenarios within simulation environments. However, a critical question remains. Are the AV failure scenarios discovered in simulation reproducible on actual systems in the real world? The sim-to-real gap caused by differences between simulated and real sensor data means that failure scenarios identified in simulation might either be artifacts of synthetic sensor data or actual issues that also occur with real sensor data. To address this, an effective approach to validating simulated failure scenarios is to locate occurrences of these scenarios within real-world datasets and verify whether the failure persists on the datasets. To this end, we introduce a formal definition of how labeled time series sensor data can match an abstract scenario, represented as a scenario program using the Scenic probabilistic programming language. We present a querying algorithm that, given a scenario program and a labeled dataset, identifies the subset of data that matches the specified scenario. Our experiment shows that our algorithm is more accurate and orders of magnitude faster in querying scenarios than the state-of-the-art commercial vision large language models, and can scale with the duration of queried time series data.