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.

翻译：时序逻辑（Temporal Logics, TLs）已被广泛应用于形式化信息物理系统的可解释任务。近年来，时间窗时序逻辑（Time Window Temporal Logic, TWTL）被提出作为动态系统的规约语言。该语言能简洁地表达机器人任务，并支持基于自动机的高效验证及此类系统的控制策略综合。本文针对该逻辑定义了两种量化语义及其对应的两种监控算法，用于实时量化离散时间系统轨迹对公式的满足程度。我们通过数值算例验证了新语义及其运行时监控器的有效性。