Predictive Semantics for Past-CTL Runtime Monitors

TL;DR

This paper enhances past-CTL logic with limited predictive capabilities using multi-valued semantics, enabling more effective runtime verification of distributed swarm systems expressed in Field Calculus.

Contribution

It introduces a novel extension of past-CTL logic with prediction features and evaluates its impact on translating formulas into decentralized monitors.

Findings

Extended past-CTL with multi-valued semantics improves prediction.

Enhanced logic enables better monitoring of future system states.

Translation into Field Calculus remains effective with the extension.

Abstract

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.