Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Spatiotemporal Robustness of Temporal Logic Tasks using Multi-Objective Reasoning

Oliver Schön, Lars Lindemann

Abstract

The reliability of autonomous systems depends on their robustness, i.e., their ability to meet their objectives under uncertainty. In this paper, we study spatiotemporal robustness of temporal logic specifications evaluated over discrete-time signals. Existing work has proposed robust semantics that capture not only Boolean satisfiability, but also the geometric distance from unsatisfiability, corresponding to admissible spatial perturbations of a given signal. In contrast, we propose spatiotemporal robustness (STR), which captures admissible spatial and temporal perturbations jointly. This notion is particularly informative for interacting systems, such as multi-agent robotics, smart cities, and air traffic control. We define STR as a multi-objective reasoning problem, formalized via a partial order over spatial and temporal perturbations. This perspective has two key advantages: (1) STR can be interpreted as a Pareto-optimal set that characterizes all admissible spatiotemporal perturbations, and (2) STR can be computed using tools from multi-objective optimization. To navigate computational challenges, we propose robust semantics for STR that are sound in the sense of suitably under-approximating STR while being computationally tractable. Finally, we present monitoring algorithms for STR using these robust semantics. To the best of our knowledge, this is the first work to deal with robustness across multiple dimensions via multi-objective reasoning.

Spatiotemporal Robustness of Temporal Logic Tasks using Multi-Objective Reasoning

Abstract

The reliability of autonomous systems depends on their robustness, i.e., their ability to meet their objectives under uncertainty. In this paper, we study spatiotemporal robustness of temporal logic specifications evaluated over discrete-time signals. Existing work has proposed robust semantics that capture not only Boolean satisfiability, but also the geometric distance from unsatisfiability, corresponding to admissible spatial perturbations of a given signal. In contrast, we propose spatiotemporal robustness (STR), which captures admissible spatial and temporal perturbations jointly. This notion is particularly informative for interacting systems, such as multi-agent robotics, smart cities, and air traffic control. We define STR as a multi-objective reasoning problem, formalized via a partial order over spatial and temporal perturbations. This perspective has two key advantages: (1) STR can be interpreted as a Pareto-optimal set that characterizes all admissible spatiotemporal perturbations, and (2) STR can be computed using tools from multi-objective optimization. To navigate computational challenges, we propose robust semantics for STR that are sound in the sense of suitably under-approximating STR while being computationally tractable. Finally, we present monitoring algorithms for STR using these robust semantics. To the best of our knowledge, this is the first work to deal with robustness across multiple dimensions via multi-objective reasoning.

Paper Structure

This paper contains 26 sections, 6 theorems, 33 equations, 6 figures, 3 algorithms.

Table of Contents

  1. Introduction
  2. Background
  3. Signals and Systems
  4. Spatial and Temporal Robustness
  5. System Specification.
  6. Spatial Robustness.
  7. Temporal Robustness.
  8. Multi-Objective Optimization
  9. Spatiotemporal Robustness
  10. Spatiotemporal Robustness as Multi-Objective Reasoning
  11. Spatiotemporal Robustness for Temporal Logic Specifications
  12. Robust Semantics for Spatiotemporal Robustness
  13. Monitoring Algorithms for the Robust Semantics
  14. Computing the Robust Semantics of Predicates
  15. A) General Predicate Functions.
  16. ...and 11 more sections

Key Result

Corollary 1

Let $x\colon\mathbb{Z}\to \mathbb{R}^n$ be a signal, $\phi$ be a specification defined over $x$, and $t\in\mathbb{Z}$ be a time. Assume further that $(x,t)\models \phi$ holds. For each joint perturbation level $({\Delta_X},{\Delta_T})\in \mathcal{STR}^\phi({x},t)$, it holds that $(x_{{\delta_X},{\de

Figures (6)

  • Figure 1: Motivation for spatiotemporal robustness.
  • Figure 2: F-16 fighter jet flight path (nominal and 10 perturbed paths), no-fly zone $Z$ (black area), and collision corridor $C$ (red area).
  • Figure 3: Left panel: Two Pareto optimal sets $D^1$ (red line) and $D^2$ (blue line) and their downward closures $D^1_\downarrow$ (red shaded area) and $D^2_\downarrow$ (blue shaded area). Middle panel: The minimum of $D^1$ and $D^2$, i.e., $\min\{D^1,D^2\}:=\max\{D^1_\downarrow \cap D^2_\downarrow\}$. Right panel: The maximum of $D^1$ and $D^2$, i.e., $\max\{D^1,D^2\}:=\max\{D^1 \cup D^2\}$.
  • Figure 4: Parse tree of the fighter-jet benchmark specification.
  • Figure 5: Spatiotemporal robustness of the fighter jet example.
  • ...and 1 more figures

Theorems & Definitions (15)

  • definition 1: Partial Order
  • definition 2: Spatiotemporal Robustness (STR)
  • Corollary 1: STR Implies Robust Task Satisfaction
  • definition 3: STL Qualitative Semantics
  • definition 4: Minimum and Maximum
  • definition 5: Robust Semantics
  • Theorem 1: Robust Semantics Under-Approximate STR
  • Corollary 2: Robust Semantics Capture Robust Task Satisfaction
  • Corollary 3: Soundness
  • Theorem 2: Equivalent Representation for $\boldsymbol{\rho^\mu(x,t)}$
  • ...and 5 more