Approximate Distributed Monitoring under Partial Synchrony: Balancing Speed and Accuracy

TL;DR

This paper introduces an approximate distributed monitoring algorithm for Signal Temporal Logic in partially synchronous systems, significantly improving speed by abstracting interleavings, while maintaining accuracy through a combined approach with exact monitoring.

Contribution

It presents a novel approximate monitoring method for STL under partial synchrony, balancing computational efficiency and precision, and integrates it with exact monitoring for enhanced performance.

Findings

Significant speedup in distributed monitoring performance.

Effective tradeoff management between speed and accuracy.

Successful validation in real-world and synthetic scenarios.

Abstract

In distributed systems with processes that do not share a global clock, \emph{partial synchrony} is achieved by clock synchronization that guarantees bounded clock skew among all applications. Existing solutions for distributed runtime verification under partial synchrony against temporal logic specifications are exact but suffer from significant computational overhead. In this paper, we propose an \emph{approximate} distributed monitoring algorithm for Signal Temporal Logic (STL) that mitigates this issue by abstracting away potential interleaving behaviors. This conservative abstraction enables a significant speedup of the distributed monitors, albeit with a tradeoff in accuracy. We address this tradeoff with a methodology that combines our approximate monitor with its exact counterpart, resulting in enhanced efficiency without sacrificing precision. We evaluate our approach with multiple experiments, showcasing its efficacy in both real-world applications and synthetic examples.