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.
翻译:对为实现全球共同目标而合作的装置的成群分布式监测越来越重要,因为这种系统用于关键应用,例如紧急情况期间的搜索和救援任务。在本文件中,我们的目标是对以时间逻辑逻辑逻辑逻辑表达的群群的全球特性进行分布的运行时间核查。特别是,为了实施分散监测器,我们采用了外地计算语言,并利用以往工作的结果,这些工程显示有可能将时间逻辑公式自动转换到FC程序。这些工程的主要局限性在于:公式是以过去CTL逻辑表达的,而过去CTL逻辑只是以过去的方式表达的,因此在预测系统未来演变的特性方面是无效的。在本文中,我们通过在多值逻辑上提供扩展的语义,将有限的预测能力注入到过去CTL逻辑中,然后评估这如何影响自动转换成外地计算监测器。