Flow-Based Synthesis of Reactive Tests for Discrete Decision-Making Systems With Temporal Logic Specifications

Designing tests for autonomous systems is challenging due to their complexity. This work proposes a flow-based approach for reactive test synthesis from temporal logic specifications, enabling the synthesis of test environments consisting of static and reactive obstacles, and dynamic test agents that can transition between states. These specifications describe desired test behavior, including system requirements as well as a test objective not revealed to the system. The synthesized test strategy places restrictions on system actions in closed-loop with system behavior, accomplishing the test objective while ensuring realizability of the system's objective without aiding it (a general-sum setting). Automata theory and flow networks are leveraged to formulate a mixed-integer linear program (MILP) for test synthesis. For a dynamic test agent, the agent strategy is synthesized for a generalized reactivity of rank 1 (GR(1)) specification constructed from the MILP solution. If this solution is not realizable with the test agent's dynamics, we add a counterexample-guided constraint to re-solve the MILP until a strategy is found. This flow-based, reactive test synthesis is conducted offline and is agnostic to the system controller. Finally, the resulting test strategy is demonstrated in simulation and hardware experiments on a pair of quadrupedal robots for a variety of specifications.