PaperlayerView exact revision on arXiv

Source-linked AI summary

Runtime Monitoring of Distributed Cyber-Physical Systems Without a Global Clock

Charles Koll, Houssam Abbas

arXiv:2608.13486v1cs.LO

TL;DR

Distributed CPS monitoring must interpret dense-time temporal requirements when agents have drifting local clocks and no shared global clock. The paper develops a DiSTL monitor for partially synchronous systems, characterizes possible satisfying cuts, and demonstrates conservative real-time monitoring under substantial clock skew.

  • Problem

    Distributed CPS monitoring must interpret dense-time temporal requirements despite drifting local clocks and asynchronous signal observations.

  • Method

    The paper characterizes possibly synchronous satisfying cuts for a DiSTL fragment and approximates them using a sound, arbitrarily precise offline monitor.

  • Results

    Real-time monitoring remained possible for clock skews between 0.16 and 6 seconds, depending on the formula.

  • Takeaways & Limitations

    The results demonstrate conservative real-time monitoring for DiSTL, with simpler formulas supporting more agents and complex formulas supporting moderate group sizes.

  • Takeaways & Limitations

    DiSTL excludes generalized conjunctions, limiting the constraints formula designers can express through arbitrary conjunction.

Abstract

from arXiv · show

We give the first theoretical characterization, and the first algorithm, for continuous monitoring of a distributed Cyber-Physical System (CPS) against a dense-time temporal logic specification. A distributed CPS is composed of multiple agents, each with a local clock; these clocks drift from each other, so there is no well-defined global time. When monitoring such a system's output signal against a temporal logic specification, it is not evident how to interpret the temporal constraints of the formula, and what satisfaction means. Yet CPS designers, like control engineers, typically think of their system's operation in terms of global time. Most existing techniques for monitoring distributed systems work with discrete-time specifications not suitable for CPS, and/or require an explicit mapping of temporal constraints to local clocks. We introduce an algorithm that addresses the above challenges for a fragment of Signal Temporal Logic (STL) that still includes all temporal operators. It relies on a novel extension of satisfaction signals to this partially synchronous setting (where clocks drift), and an analysis of the geometry of multi-dimensional partially synchronous time. The algorithm returns the set of all possible global moments that can satisfy the specification. Knowledge of these possible global moments is important for debugging distributed hybrid control systems such as fleets of drones and electrical grids. We derive the worst-case complexity of the algorithm, and implement a sound approximation of it that experimentally illustrates effective monitoring, even in scenarios of up to 50 agents.

1 Introduction: Monitoring Dense-Time Requirements Without a Shared Clock

The section motivates runtime monitoring of dense-time temporal requirements in distributed CPS with unsynchronized local clocks. It presents partially synchronous monitoring through DiSTL, satcut geometry, and an offline monitor that approximates all possibly synchronous satisfying moments.

  • Motivation: Distributed CPS require runtime monitoring of hybrid-system outputs against temporal-logic correctness requirements.Examples include autonomous-vehicle networks, drone fleets, smart electrical-grid controllers, and geographically dispersed sensor networks.
  • Problem setting: Partially synchronous monitoring treats signal values within ε time units as potentially synchronous and explores them for specification satisfaction or violation.The system uses clock synchronization to keep local clocks within a known bound ε.
  • Contributions: The paper provides the first offline monitor that approximates the entire set of satcuts to arbitrary precision.Satcuts are also described as the satisfaction signal in the contribution list.
  • Related work: Prior work largely uses discrete or logical time, handles dense time only for boolean predicates, or returns satisfaction only at time 0 rather than all possibly synchronous moments.The paper states that no directly comparable work exists.

2 Preliminaries

This section defines distributed signals and the partially synchronous clock model, then introduces concurrent events and consistent cuts for reasoning about distributed time. It also summarizes the STL syntax and synchronous satisfaction semantics used for CPS requirements.

  • Distributed signals: Each agent’s output is a right-continuous, left-limited, non-Zeno function, and a distributed signal is a collection of N such output signals.The timeline is T := R≥0, and each output signal maps time to R^d.
  • Partial synchrony: Under partial synchrony, each local clock is strictly increasing and remains within a known fixed skew ε of a hypothetical reference clock.The clock functions satisfy |c_n(χ) − χ| ≤ ε and c_n(0) = 0; the reference clock is not real or used by the algorithm.
  • Concurrency and cuts: Events from all agents are concurrent when every pair of local timestamps differs by at most 2ε, so their temporal ordering must be treated as potentially synchronous.Signals may drift arbitrarily within the fixed maximum skew ε.
  • Concurrency and cuts: A consistent cut is a Cartesian product of local time prefixes whose frontier is concurrent; concuts are ordered only when every local clock advances.For concuts C and C′, C ≺ C′ requires t_n < t′_n for all agents, while C ⪯ C′ also permits equality.
  • Signal Temporal Logic: STL requirements use Boolean operators and bounded Until, where φ must hold continuously until ψ holds at some time in the specified interval.Eventually and Always are derived from Until, negation, and True.

3 Problem Formulation

The paper defines distributed STL satisfaction without requiring engineers to encode partial synchrony in formulas, using bounded retimings to represent possible alignments of drifting local clocks. It then restricts STL to DiSTL, whose cut-based satisfaction signals support finding all possible synchronizations satisfying a specification.

  • 3 Problem Formulation: Distributed STL satisfaction is defined without forcing specification writers to choose a local clock for evaluating temporal intervals intended to measure global time.The formulation first addresses how a distributed signal can satisfy an STL formula under partial synchrony.
  • 3 Problem Formulation: An agent retiming is a strictly increasing curve ρn: R≥0 7→T starting at 0 and satisfying |t − ρn(t)| ≤ ε for every t ∈ R≥0.System retimings combine the individual agent retimings into a curve over TN.
  • 3.1 Why the STL Fragment?: General STL conjunctions require the same retiming to witness both subformulas, even when separate retimings witness them individually.Finitely representing and tracking all such retimings across subformulas creates substantial difficulties.
  • 3.1 Why the STL Fragment?: DiSTL avoids these difficulties by restricting the language so monitoring does not require tracking retimings across subformulas.This restriction enables efficient monitoring in the presence of retimings.
  • 3.2 The DiSTL Fragment: DiSTL retains atomic Boolean structure together with disjunction, restricted conjunction, eventually, always, and until operators over intervals I = [a, b].Its syntax permits φτ ∧ φa and φa UI φτ rather than unrestricted conjunction between general formulas.
  • 3.2 The DiSTL Fragment: In the partially synchronous setting, the satisfaction signal is a Boolean function of concut frontiers and incorporates a choice of retiming.For a concut C, the signal considers retimings passing through C; satisfaction is true when the corresponding satsignal equals ⊤.
  • 3.2 The DiSTL Fragment: The main problem is to find all concuts C of a distributed signal for which λφτ(C) = ⊤, representing all possible synchronizations that satisfy the specification.These concuts can equivalently identify possible synchronizations where the CPS breaches correctness requirements, whose formula is the provided specification’s negation.

4 Offline Monitoring: Characterization and Algorithm

The section characterizes DiSTL satdomains and develops an offline monitor that recursively computes the possible satisfying concut frontiers. It handles Until through sound inner and outer approximations based on geometric box operations.

  • Satdomain characterization: The satdomain [[φτ]] is the set of concut frontiers where the distributed signal’s satisfaction signal evaluates to True.The offline monitor has access to the entire distributed signal and returns this satdomain.
  • Satdomain characterization: Temporal intervals are lifted to (N + 1)-dimensional intervals to represent admissible shifts of local clocks and global time.The lifting handles both intervals beginning at zero and intervals requiring strictly positive local-clock shifts.
  • Satdomain characterization: The Until satdomain consists of cuts connected by a strictly increasing curve that remains in [[φτ]] until reaching [[ψτ]] with a time difference in I.The curve witnesses a retiming under which φτ holds until ψτ becomes satisfied.
  • Offline monitor: The offline monitor recursively computes satdomains using polytope manipulations, with unions, intersections, and shifts preserving non-convex polytope representations.For Until, it invokes specialized procedures rather than only the direct operations used for other operators.
  • Offline monitor: MoveBackin and MoveBackout produce inner and outer approximations, respectively, of the Until satdomain by tracking paths through box partitions.MoveBackout uses bounding boxes, while MoveBackin uses inscribed boxes.
  • Offline monitor: Approximation quality can be made arbitrarily tight by using more or smaller boxes, trading improved accuracy against computational cost.Outer approximations use several boxes instead of one, while inner approximations pack more smaller boxes.

Appendix A.5 sketches a proof of this bound.

The bound follows by combining lemmas for inner and outer approximations of the Until operator. This yields two monitoring algorithms, monin and monout, based on MoveBackin and MoveBackout, respectively.

  • Proof sketch: The monitor consists of two algorithms: monin applies MoveBackin to every Until operator, while monout uses MoveBackout.The resulting set from each Until operator is used at the next level of the formula.
  • Proof sketch: The inner and outer inclusions can be made arbitrarily tight by using more tighter inner and outer bounding boxes in MoveBack.This tightening applies to the approximations used by the monitor.

5 A Boxed Implementation and Experimental Results

The boxed algorithm replaces arbitrary-polytope partitioning with box outer approximations, enabling conservative real-time monitoring of DiSTL formulas. Experiments show scalability depends on formula complexity, agent count, clock skew, and signal values.

  • Implementation: Box outer-approximations make exact monitoring practical by avoiding partitioning arbitrary polytopes along every edge.The Rust implementation always processes boxes and outer-approximates each subformula’s satdomain.
  • Experimental setup: The experiments used 6-second, continuously varying ±1 signals with 10 roots/s on a Rust implementation running on an AMD Ryzen 7 PRO 7840U with 16 GB RAM.Signals switched linearly every 10 ms with probability 0.1.
  • Results: 57 agents can be monitored in real time for Formula 1, compared with 9 for Formula 3 and 6 for Formula 2.The real-time threshold is a monitoring time below the 6-second signal length; boolean Formula 1 is much faster than the temporal formulas.
  • Results: At 63 agents, Formula 1 runtime ranged from 0.2 to 95 seconds across signals, showing strong dependence on input-signal values.Signals with many predicate intersections require more box and intersection calculations, while signals without intersections require little further work.
  • Results: For fixed N, runtime increases with clock skew ε, then levels off for Formula 1 around ε = 2.5 seconds.Larger skew permits more concurrent events, producing larger satdomains and more intersections; beyond this point, the skew boundary no longer constrains Formula 1 boxes.
  • Results: The monitor remains real-time for clock skews between 0.16 and 6 seconds, depending on formula, while larger agent counts increase runtime.The results demonstrate conservative real-time monitoring, with simpler formulas supporting more agents and complex formulas supporting moderate groups at realistic skews.

6 Conclusion

The paper characterizes satisfaction domains for dense-time temporal logic in partially synchronous distributed CPS and presents an algorithm returning all satisfactions, not only those at global time 0. It also implements a conservative monitor for an STL fragment containing all temporal operators.

  • The work provides the first theoretical characterization of satisfaction domains for dense-time temporal logic formulas in partially synchronous distributed CPS.
  • The first algorithm returns all satisfactions of such formulas, rather than only satisfactions at global time 0.
  • The monitor supports a fragment of dense-time Signal Temporal Logic that includes all temporal operators.
  • The authors implemented a conservative monitor based on the algorithm and demonstrated monitoring experimentally.

A Proofs · A.1 Theorem 1

The proof of Theorem 1 establishes lemmas showing that non-timed satisfaction is invariant under retiming and that preceding cuts can be incorporated without changing satisfaction. It then applies these properties recursively to temporal operators, including eventually, conjunction, and disjunction.

  • A.1 Theorem 1: Non-timed DiSTL satisfaction is unaffected by retimings, as shown by structural cases for constants, propositions, negation, conjunction, and disjunction.The proposition and negation cases reduce directly to the corresponding signal values, while conjunction and disjunction are immediate.
  • A.1 Theorem 1: For cuts C ⪯ C′, a retiming passing through C′ can be adjusted to pass through C as well without changing satisfaction at C′.This relies on STL containing only future-time operators, so satisfaction at C′ does not depend on retimed values before C′.
  • A.1 Theorem 1: The constructed agent retiming is well formed because its deviation from time remains within ε across the intervals before, between, and after the relevant cuts.The proof checks the bound separately for t ≤ C[N + 1], C[N + 1] < t ≤ C′[N + 1], and t ≥ C′[N + 1].
  • A.1 Theorem 1: Theorem 1 is proved by considering the recursive structure of the formula, with constants and atomic propositions handled immediately or through Lemma 3.The proof states that conjunction and disjunction follow the same pattern.
  • A.1 Theorem 1: For the eventually operator, satisfaction at a future time t′ is converted into an equivalent existential condition over a later cut C′.The cut satisfies C′ ⪰ C and C′[N + 1] ∈ C[N + 1] ⊕ I.
  • A.1 Theorem 1: The proof replaces time instances with cut indices and, for a fixed retiming, identifies the relevant intermediate cut within the interval between C and C′.It notes that each retiming has exactly one cut at index N + 1.
  • A.1 Theorem 1: Although one implication initially follows from a weakening property of first-order logic, the reverse implication is obtained by combining retimings through a common cut.Future-time dependence lets the proof preserve the satisfaction properties when replacing the original retimings.

A.2 Theorem 2

Theorem 2 is established by structural equivalences for Boolean and temporal operators, including a reduction of bounded globally to eventually and until semantics. The proof also characterizes temporal dilation through configuration shifts and Minkowski difference.

  • Boolean operators: The disjunction case follows from Theorem 1 and induction, equating its satisfaction domain with the union of the component satisfaction domains.The proof states C ∈ [[φa ∨ψa]] iff C ∈ [[φa]] ∪ [[ψa]].
  • Boolean operators: The remaining disjunction and conjunction cases follow by the same proof with the corresponding operator changes.The cited cases are [[φτ ∨ψτ]], [[φa∧ψa]], and [[φτ ∧ψa]].
  • Temporal operators: Temporal dilation is rewritten as existence of a future configuration C′ satisfying φτ with C′ ∈ C ⊕ L(I), equivalently C ∈ ([[φτ]] ⊖ L(I)).The derivation expands C ⊕ L(I) into C + K and rearranges C′ = C + K as C = C′ − K.
  • Temporal operators: For □[b,c]φa, the proof first establishes λ□[b,c]φa(C) = λ♢[b,b]□[0,c−b]φa(C), then rewrites the inner globally operator using until.It concludes λ□[b,c]φa(C) = λ♢[b,b](φa U[c−b,c−b] ⊤)(C), with the satdomain given by the satisfaction signal’s support.

A.3 Lemma 1

Lemma 1 proves that the relevant satisfaction sets are unions of non-convex polytopes. The proof establishes this for atomic predicates and temporal and Boolean operators, while MoveBackout preserves the representation through outer approximation and partitioning.

  • Atomic predicates: Atomic predicate satisfaction sets are intersections of a polytope with unions of polytopes, hence unions of non-convex polytopes.The argument uses the signal constraint that each threshold set {t | x_n(t) ≥ p_n} is a disjoint union of intervals; negated predicates follow similarly.
  • Boolean operators: Boolean disjunction and conjunction preserve unions of non-convex polytopes through union and intersection operations.The proof applies closure of UNCPs under these set operations.
  • Temporal operators: The eventually operator preserves the representation because the shift operation preserves convexity and distributes over unions of polytopes.The always operator is reduced to a combination of previously established cases.
  • Algorithmic preservation: MoveBackout maps non-convex polytopes to non-convex polytopes by outer-approximating, partitioning, and intersecting boxes.This preserves the non-convex-polytope representation used by the theorem’s unions, intersections, and shifts.

A.4 Lemma 2 · A.5 Complexity Analysis Eq. (1)

Lemma 2 proves that MoveBackout returns a superset containing every satisfying cut, while the complexity analysis derives the dominant cost of bounding-box computation from worst-case polytope vertex counts. The proof propagates satisfying cuts through I-away regions and increasing paths across blocks.

  • A.4 Lemma 2: MoveBackout(φ_a UI ψ_τ) is shown to be a superset of [[φ_a UI ψ_τ]].The inner-approximation case follows by similar reasoning.
  • A.4 Lemma 2: The algorithm takes non-convex polytopes A1 and B1 that overapproximate [[φ_a]] and [[ψ_τ]], respectively.The proof shows every satisfying cut is contained in the output Y ∩ [[⊤]].
  • A.4 Lemma 2: For a single block S′ ⊆ B, every cut I-away from a destination point lies in the generated region G.This follows from the definition of L(I) and the erosion S′ ⊖ L(I).
  • A.4 Lemma 2: Across blocks S1, …, Sk from L, G contains points that are I-away from S′ and have strictly increasing paths within A1.Such paths must cross lower boundaries, and adjacent blocks sharing those boundaries are added to L.
  • A.4 Lemma 2: Every satisfying cut belongs to some G ∩ S and is therefore returned by the algorithm.Points in G ∩ S are added to the results, while satisfying cuts lie in [[⊤]] by definition.
  • A.5 Complexity Analysis Eq. (1): O(N · V) is the cost of finding a bounding box for a polytope in R^N with V vertices.The procedure enumerates vertices and finds their minimum and maximum along each dimension.
  • A.5 Complexity Analysis Eq. (1): The worst-case vertex count is obtained from the dual of a cyclic polytope using the upper bound theorem, determining the fastest-growing complexity term.The cited result uses cyclic polytopes’ maximal face counts for a given number of vertices.
Loading 2608.13486v1…