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.

翻译：时间逻辑被广泛用于为物理系统规定可解释的任务。时间窗口时间逻辑(TWTL)是最近为动态系统提出的规范语言。特别地，它可以轻松地表达机器人任务，并允许对此类系统的控制策略进行高效的、基于自动机的验证和合成。在本文中，我们定义了两种量化语义和两种相应的监测算法，使离散时间系统的轨迹在实时满足公式的满足度可以实时量化。我们在数字实例上演示了新语义及其运行时监视。