Spatiotemporal Robustness of Temporal Logic Tasks using Multi-Objective Reasoning

TL;DR

This paper introduces a novel multi-objective reasoning framework for assessing spatiotemporal robustness of temporal logic specifications in autonomous systems, capturing joint spatial and temporal perturbations.

Contribution

It proposes the concept of spatiotemporal robustness (STR), formalizes it as a multi-objective problem, and develops computationally tractable semantics and monitoring algorithms.

Findings

STR characterizes all admissible spatiotemporal perturbations as a Pareto set.

Robust semantics under-approximate STR while remaining computationally feasible.

First approach to multi-dimensional robustness via multi-objective reasoning in this context.

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.