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

Title	Synthesizing Reactive Test Environments for Autonomous Systems: Testing Reach-Avoid Specifications with Multi-Commodity Flows
Authors	Apurva Badithela, Josefine B. Graebener, Wyatt Ubellacker, Eric V. Mazumdar, Aaron D. Ames and Richard M. Murray
Source	Submitted, 2023 International Conference on Robotics and Automation (ICRA)
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 Bu ̈chi 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.
Type	Conference paper
URL	http://cds.caltech.edu/~murray/preprints/bad+23-icra s.pdf
DOI
Tag	Bad+23-ICRA
ID	2022d
Funding	AFOSR T&E
Flags