论文标题
过去CTL运行时监视器的预测语义
Predictive Semantics for Past-CTL Runtime Monitors
论文作者
论文摘要
与共同全球目标合作的一群设备的分布式监控变得越来越重要，因为此类系统被用于关键应用程序，例如在紧急情况下进行搜索和救援任务。在本文中，我们针对的是在时间逻辑中以逻辑公式表示的群体的全局特性的分布式运行时验证。特别是，为了实施分散的监视器，我们采用了字段演算（FC）语言，并利用了先前作品的结果，这些结果表明有可能自动将时间逻辑公式转化为FC程序。这种工作的主要局限性在于，公式是在过去的CTL逻辑中表达的，该公式仅具有过去的方式，因此无法预测有关系统未来演变的属性。在本文中，我们通过在多价值逻辑上提供扩展的语义，然后评估这如何影响自动化转换为字段计算显示器，从而将一些有限的预测能力注入了过去的CTL逻辑。
The distributed monitoring of swarms of devices cooperating to common global goals is becoming increasingly important, as such systems are employed for critical applications, e.g., in search and rescue missions during emergencies. In this paper, we target the distributed run-time verification of global properties of a swarm expressed as logical formulas in a temporal logic. In particular, for the implementation of decentralized monitors, we adopt the Field Calculus (FC) language, and exploit the results of previous works which have shown the possibility of automatically translating temporal logic formulas into FC programs. The main limitation of such works lies in the fact that the formulas are expressed in the past-CTL logic, which only features past modalities, and is therefore ineffective in predicting properties about the future evolution of a system. In this paper, we inject some limited prediction capability into the past-CTL logic by providing an extended semantics on a multi-valued logic, then assessing how this affects the automated translation into field calculus monitors.
