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.

翻译：自主系统的可靠性取决于其鲁棒性，即在不确定性条件下实现目标的能力。本文研究基于离散时间信号评估的时序逻辑规范的时空鲁棒性。现有工作已提出不仅捕获布尔可满足性，还捕获与不可满足性之间几何距离（即给定信号可允许的空间扰动对应距离）的鲁棒语义。与之相对，我们提出时空鲁棒性（STR），该概念联合考虑可允许的空间与时间扰动。这一概念对多智能体机器人、智慧城市及空中交通管制等交互系统尤为重要。我们将STR定义为通过空间与时间扰动的偏序关系形式化的多目标推理问题。该视角具有两大优势：(1) STR可解释为表征所有可允许时空扰动的帕累托最优集；(2) STR可利用多目标优化工具进行计算。为应对计算挑战，我们提出STR的鲁棒语义，该语义在计算可处理的前提下合理逼近STR的下界。最后，我们利用这些鲁棒语义提出了STR的监控算法。据我们所知，这是首个通过多目标推理处理多维度鲁棒性的工作。