Flow-Based Synthesis of Reactive Tests for Discrete Decision-Making Systems with Temporal Logic Specifications
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要