Runtime Monitoring of Time Window Temporal Logic
Runtime Monitoring of Time Window Temporal Logic
复制标题
时间窗口时序逻辑的运行时监控
DOI：
--
复制
发表时间：
2022
影响因子：
5.2
通讯作者：
K. A. Hoque
中科院分区：
文献类型：
--
作者：
Ernest Bonnah;K. A. Hoque
时态逻辑在动态系统的分析和控制中的应用日益广泛。时间窗时序逻辑（TWTL）是一种丰富的表达语言，用于以紧凑的方式指定有时间限制的串行任务，在许多控制应用中很常见，例如机器人。通常，TWTL规范使用基于自动机的模型检查算法进行验证。然而，在设计时使用模型检查对给定系统的重要属性进行验证并不能保证系统在运行时操作期间的行为符合预期，这福尔斯运行时验证的范围。在这封信中，我们提出了一个重写为基础的算法，用于运行时监控的安全需求表示在TWTL。我们所提出的方法的可行性和效率证明了使用两个案例研究有关的无人机（UAV）的监视和工业机器人制造。
Temporal logic is becoming increasingly popular for its application in the analysis and control of dynamic systems. Time window temporal logic (TWTL) is a rich expressive language for specifying time-bounded serial tasks in a compact manner that is common in many control applications, such as robotics. Typically, TWTL specifications are verified using an automata-based model checking algorithm. However, verification of important properties of a given system using model checking in design time does not guarantee that the system will behave as expected during the runtime operation which falls under the scope of runtime verification. In this letter, we present a rewriting-based algorithm for runtime monitoring of safety requirements expressed in TWTL. The feasibility and efficiency of our proposed approach is demonstrated using two case studies related to unmanned aerial vehicle (UAV) surveillance and industrial robotics for manufacturing.