Synthesizing Reactive Test Environments for Autonomous Systems: Testing Reach-Avoid Specifications with Multi-Commodity Flows

TL;DR

This paper presents a method for automatically generating reactive test environments for autonomous systems using multi-commodity flow optimization, ensuring system behaviors meet specified reach-avoid criteria in simulation and real hardware.

Contribution

It introduces a novel framework combining automata-based specifications with multi-commodity network flow optimization for reactive test synthesis.

Findings

Successfully verified locomotion behaviors on hardware.

Demonstrated effectiveness in grid world simulations.

Framework ensures system meets complex test specifications.

Abstract

We study automated test generation for verifying discrete decision-making modules in autonomous systems. We utilize linear temporal logic to encode the requirements on the system under test in the system specification and the behavior that we want to observe during the test is given as the test specification which is unknown to the system. First, we use the specifications and their corresponding non-deterministic B\"uchi automata to generate the specification product automaton. Second, a virtual product graph representing the high-level interaction between the system and the test environment is constructed modeling the product automaton encoding the system, the test environment, and specifications. The main result of this paper is an optimization problem, framed as a multi-commodity network flow problem, that solves for constraints on the virtual product graph which can then be projected to the test environment. Therefore, the result of the optimization problem is reactive test synthesis that ensures that the system meets the test specifications along with satisfying the system specifications. This framework is illustrated in simulation on grid world examples, and demonstrated on hardware with the Unitree A1 quadruped, wherein dynamic locomotion behaviors are verified in the context of reactive test environments.