Approximate Distributed Monitoring under Partial Synchrony: Balancing Speed and Accuracy

TL;DR

The paper tackles the high computational cost of exact distributed runtime verification for Signal Temporal Logic under partial synchrony. It introduces Adm, an approximate STL$^+$ monitoring framework that overapproximates interleavings by canonical segmentation and value expressions, and complements it with exact monitoring to recover precision when needed. The approach supports variants (Adm-F, Adm-C, Adm-Fr, Adm-Cr) and a mixed Adm+Edm strategy to balance efficiency and accuracy, with formal guarantees that $[(S,\rightsquigarrow) \models \varphi]_+ \in \{\top,\bot,?\}$ implies the true verdict can be recovered or refined. Empirical results demonstrate speedups from three to five orders of magnitude across synthetic traces and real-world scenarios (e.g., water distribution and drone swarms), while maintaining acceptable accuracy and enabling improved efficiency through combining approximate and exact monitors.

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.

Figures (2)

• Figure 1: A distributed signal in with consistent cuts $C_1, C_2, C_3$ constituting a consistent cut flow. Note that $C'$ is a non-example since $(2.5, x_2(2.5)) \in \mathsf{fr}(C')$ and $(1.6, x_1(1.6)) \notin \mathsf{fr}(C')$, but $(1.6, x_1(1.6))$ happened before $(2.5, x_2(2.5))$.
• Figure 2: (a) A distributed signal $(S,{\rightsquigarrow})$ with $x_1$ (top, red) and $x_2$ (bottom, blue) whose edges are marked with solid balls and their uncertainty regions are given as semi-transparent boxes around the edges. The resulting canonical segmentation $G_S$ is shown below the graphical representation of the signals. (b) The uncertainty regions of $(S,{\rightsquigarrow})$ and the corresponding value expressions. (c) The tabular representation of the function $\gamma$ for $(S,{\rightsquigarrow})$, e.g., $\gamma(x_1, [3,4)) = (\textsf{suffix}(01) \cdot \textsf{prefix}(10)) \setminus \{\epsilon\} = \{ 01, 010, 1, 10\}$.

Theorems & Definitions (4)

• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition
• theorem 1.1