Imandra for
Autonomous Systems

As autonomous systems become ubiquitous, assurance that their designers have considered all of the relevant "edge-cases" is ever more important. Many global projects seek to address the rigorous generation of such scenarios for testing and certification. We strive to extend their efforts and propose deriving concrete driving scenarios (for testing autonomous systems) from higher-level "digital twin" models representing the physical world. When encoded as infinite state machines, these models become much more expressive and "natural" for encoding than individual scenarios. Furthermore, they are susceptible to formal verification and reasoning, empowering the designers to tackle even the most complex domains.

Test Scenario
Generation

The current industry efforts focus on creating/operating on scenarios directly and then "running" them in simulation environments.

There are several recognized problems with this approach:

  • Coverage metrics: given a collection of "hand-written" scenarios, there's no methodology for reasoning about their coverage.

  • Mapping: how to map actual driving data back into a particular driving scenario. A particular "run" of a scenario may exhibit non-deterministic behavior, making such mapping especially difficult.

  • Scalability: there are potentially many unique driving scenarios, and encoding them "by hand" does not scale.

Imandra logo with data
Imandra logo with data

“Lifting” Test Scenario Generation

Instead, we propose to focus on encoding "digital twin" models and then use them to derive scenarios via state-space region decomposition.

There are multiple advantages to this approach:

  • It's much more natural to encode such models and reason about their completeness.

  • Each model may be decomposed into a finite number of symbolic "edge cases" or "regions" of its state-space.

  • Scenarios may be synthesized from such regions and vice versa; given vehicle driving data, we can map it into a particular region of the model state-space.

Imandra logo with data

Modeling “Digital Twins” As Infinite State Machines

Infinite state machines are the natural method for encoding "digital twin" models representing particular driving geographies and the associated physical representations.

As with any formal model of a physical phenomenon, there are various degrees of representing "reality."

Digital Twins
Illustration of Model Refinement process

Imandra’s
Region Decomposition

Region Decomposition is a feature of Imandra inspired by Cylindrical Algebraic Decomposition (CAD) but lifted for algorithms at large. With Region Decomposition, Imandra can take a function (or a model) written in the "pure" subset of OCaml (or ReasonML) and describe its behavior with a finite number of regions of its state-space.

Each such region of the state-space contains:
● A set of symbolic constraints on the inputs
● A symbolic invariant describing expected output

Imandra can further synthesize concrete inputs into the model satisfying a particular region - these instances will then be printed as driving scenario descriptions (e.g., CARLA's Python Strategy Interface).

Region Decomposition Illustration

State-space Regions
of “Digital Twin” Models

state machine encoding particular geography (with physics, etc.), each region of its state-space represents a distinct symbolic driving scenario.

State-space Regions

Generating Test Cases

Imandra is a cloud-native automated reasoning engine allowing you to:
• Encode "digital twin" models using OCaml or ReasonML
• Decompose their state-spaces to create quantitative coverage metrics (symbolic driving scenarios)
• Synthesize and print (in whatever format is best suited for your simulation environment) concrete driving scenarios

Generating Test Cases

Quantifying Testing Coverage

You can actually map the driving data into regions to understand what subset of the state-space has been covered.

Quantifying Testing Coverage

State Explorer

The following regions were decomposed from the simple intersection model.

Select a region below for details

    Velocity

  • Steady
  • Braking
  • Accelerating

    Lights

  • Green
  • Yellow
  • Red
  • Yellow&Red

    Passing

  • Will pass
  • Won't pass
crossroad-scene First line of text Second line of text Third line of text.

Region Name

Constraints

Invariant

Not sure how to get started? Join us on

Discord
By using this website, you agree to our cookie policy

Please note that the Imandra website no longer supports Internet Explorer

We recommend upgrading to the latest Microsoft Edge, Google Chrome, or Firefox