Designing tests to evaluate if a given autonomous system satisfies complex specifications is challenging due to the complexity of these systems. 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. The temporal logic specifications describe desired test behavior, including system requirements as well as a test objective that is not revealed to the system. The synthesized test strategy places restrictions on system actions in reaction to the system state. The tests are minimally restrictive and accomplish the test objective while ensuring realizability of the system's objective without aiding it (semi-cooperative setting). Automata theory and flow networks are leveraged to formulate a mixed-integer linear program (MILP) to synthesize the test strategy. For a dynamic test agent, the agent strategy is synthesized for a GR(1) specification constructed from the solution of the MILP. If the specification is unrealizable by the dynamics of the test agent, a counterexample-guided approach is used to resolve 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 experimentally on a pair of quadrupedal robots for a variety of specifications.

翻译：设计测试以评估给定自主系统是否满足复杂规范具有挑战性，原因在于这些系统的复杂性。本文提出了一种基于流的时态逻辑规范反应式测试生成方法，能够合成包含静态与反应式障碍物及动态测试智能体的测试环境。时态逻辑规范描述了期望的测试行为，包括系统要求以及不向系统披露的测试目标。综合生成的测试策略会根据系统状态对系统动作施加约束。这些测试具有最小限制性，既能实现测试目标，又能确保系统目标的可实现性但不对其提供辅助（半协作场景）。利用自动机理论与流网络构建混合整数线性规划（MILP）以合成测试策略。对于动态测试智能体，通过从MILP解中构建的GR(1)规范来合成智能体策略。若该规范因测试智能体动力学不可实现，则采用反例引导方法迭代求解MILP直至找到可行策略。这种基于流的反应式测试合成方法可离线执行，且与系统控制器无关。最后，在仿真与双足机器人实验中针对多种规范验证了所提测试策略的有效性。