Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Josefine B. Graebener, Apurva S. Badithela, Denizalp Goktas, Wyatt Ubellacker, Eric V. Mazumdar, Aaron D. Ames, Richard M. Murray

TL;DR

The paper addresses automatic synthesis of test environments for autonomous systems by combining temporal-logic specifications with flow-based optimization. It builds a virtual product graph to capture system and test objectives, then solves a mixed-integer linear program to identify the minimal edge-cuts (restrictions) needed to force the test objective while preserving system feasibility. For dynamic test agents, a GR(1) synthesis step via TuLiP coupled with a counterexample-guided refinement ensures realizable strategies, all performed offline. The approach is demonstrated on grid-world simulations and hardware with quadrupeds, showing that it yields least-restrictive tests and scalable runtimes on medium-sized problems. Overall, the work provides a practical, off-line, semi-cooperative testing framework that complements falsification and classical reactive synthesis.

Abstract

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.

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

TL;DR

The paper addresses automatic synthesis of test environments for autonomous systems by combining temporal-logic specifications with flow-based optimization. It builds a virtual product graph to capture system and test objectives, then solves a mixed-integer linear program to identify the minimal edge-cuts (restrictions) needed to force the test objective while preserving system feasibility. For dynamic test agents, a GR(1) synthesis step via TuLiP coupled with a counterexample-guided refinement ensures realizable strategies, all performed offline. The approach is demonstrated on grid-world simulations and hardware with quadrupeds, showing that it yields least-restrictive tests and scalable runtimes on medium-sized problems. Overall, the work provides a practical, off-line, semi-cooperative testing framework that complements falsification and classical reactive synthesis.

Abstract

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.
Paper Structure (29 sections, 14 theorems, 56 equations, 34 figures, 6 tables, 2 algorithms)

This paper contains 29 sections, 14 theorems, 56 equations, 34 figures, 6 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Background on Test and Evaluation
  3. Contributions
  4. Preliminaries
  5. Automata Theory and Temporal Logic
  6. Network Flows
  7. Problem Statement
  8. Graph Construction
  9. Network Flow Optimization for Identifying Restrictions on System Actions
  10. Optimization Setup
  11. Characterizing Optimization Results
  12. Test Strategy Synthesis
  13. Test Environments with Static and/or Reactive Obstacles
  14. Synthesizing a Dynamic Test Strategy
  15. Complexity
  16. ...and 14 more sections

Key Result

Lemma 1

For every path $(s, q_{\text{sys}})_0, (s, q_{\text{sys}})_1,\ldots,(s, q_{\text{sys}})_n$ on $G_{\text{sys}}$, there exists at least one corresponding path on $G$.

Figures (34)

  • Figure 1: Overview of the flow-based test synthesis framework which consists of three key parts: i) graph construction, ii) routing optimization, and iii) test environment synthesis (e.g., reactive test strategy / test agent strategy, static obstacles).
  • Figure 2: Example \ref{['ex:med_ex']}.
  • Figure 3: Example \ref{['ex:small_reactive']}.
  • Figure 5: $\mathcal{B}_\text{sys}$
  • Figure 6: $\mathcal{B}_\text{test}$
  • ...and 29 more figures

Theorems & Definitions (57)

  • Definition 1: Finite Transition System
  • Definition 2: System
  • Definition 3: Test Harness
  • Definition 4: Test Environment
  • Definition 5: Linear Temporal Logic baier2008principles
  • Definition 6: Deterministic Büchi Automaton
  • Remark 1
  • Definition 7: Test Objective
  • Definition 8: System Objective
  • Definition 9: System Guarantees
  • ...and 47 more