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.

Test Scenario Generation Old Model

"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.

Test Scenario Generation New Model

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 Tween
Model Refinement

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

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.

Digital Tween

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

Region Decomposition

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-sceneFirst line of textSecond line of textThird line of text.

Region Name



Let's talkTalk
to an Expert

a contact

Not sure
if we can help?

We'd be happy to discuss your project to suggest the best solution.

a case analysis