Robustness Measures and Monitors for Time Window Temporal Logic
Abstract
Temporal logics (TLs) have been widely used to formalize interpretable tasks for cyber-physical systems. Time Window Temporal Logic (TWTL) has been recently proposed as a specification language for dynamical systems. In particular, it can easily express robotic tasks, and it allows for efficient, automata-based verification and synthesis of control policies for such systems. In this paper, we define two quantitative semantics for this logic, and two corresponding monitoring algorithms, which allow for real-time quantification of satisfaction of formulas by trajectories of discrete-time systems. We demonstrate the new semantics and their runtime monitors on numerical examples.
Cite
@article{arxiv.2304.06645,
title = {Robustness Measures and Monitors for Time Window Temporal Logic},
author = {Ahmad Ahmad and Cristian-Ioan Vasile and Roberto Tron and Calin Belta},
journal= {arXiv preprint arXiv:2304.06645},
year = {2023}
}
Comments
Submitted to the 62nd IEEE Conference on Decision and Control (CDC2023)