Precision on Demand: Propositional Logic for Event-Trigger Threshold Regulation

TL;DR

The paper tackles excessive data transmission in cyber-physical systems by introducing an event-triggered threshold (ETT) regulation mechanism grounded in the quantitative semantics of Propositional Logic (PL). It builds from a constant-$ETT$ baseline to robustness-driven regulation for inequality properties and extends to propositional and arbitrarily nested PL properties, providing formal guarantees for detection of satisfaction/violation via interval arithmetic. A key contribution is the parameter-selection framework and a normalization-based refinement that allocates measurement effort according to property criticality, enabling substantial reductions in triggered events while preserving safety—for example, in a convoy ACC case study, the proposed approach achieves 41.8–96.3% fewer events than constant ETT under comparable safety levels. The work offers a versatile methodology for encoding system requirements as PL properties, enabling precise, scalable, and safety-aware communication reduction in multi-sensor CPS, with future directions including STL integration and broader co-design considerations.

Abstract

We introduce a novel event-trigger threshold (ETT) regulation mechanism based on the quantitative semantics of propositional logic (PL). We exploit the expressiveness of the PL vocabulary to deliver a precise and flexible specification of ETT regulation based on system requirements and properties. Additionally, we present a modified ETT regulation mechanism that provides formal guarantees for satisfaction/violation detection of arbitrary PL properties. To validate our proposed method, we consider a convoy of vehicles in an adaptive cruise control scenario. In this scenario, the PL operators are used to encode safety properties and the ETTs are regulated accordingly, e.g., if our safety metric is high there can be a higher ETT threshold, while a smaller threshold is used when the system is approaching unsafe conditions. Under ideal ETT regulation conditions in this safety scenario, we show that reductions between 41.8 - 96.3% in the number of triggered events is possible compared to using a constant ETT while maintaining similar safety conditions.

Figures (7)

• Figure 1: Visualization of periodic transmission (top), static (middle) and safety-dependent (bottom) event-triggering conditions. Yellow dots indicate measurement transmission. The static event trigger prioritizes change in the signal regardless of safety, while the safety-dependent event trigger prioritizes change relative to the safety of the system.
• Figure 2: An overview of the system architecture considered in this paper. Dotted black lines indicate an optional data flow. The control input $\boldsymbol{u}_{t_k}$ is necessary for the monitor if we wish to verify or monitor control actions in the system properties and $\hat{y}_{i, t_k}$ is necessary if the innovation update error is used (described in Section \ref{['sec:event-triggering-mechanisms']}).
• Figure 3: A binary tree representation of the PL property $((\varphi_1 \land \varphi_2) \lor \varphi_3) \lor (\varphi_4 \land (\varphi_5 \land \varphi_6))$. The solid black arrows indicate the application of Definition \ref{['def:ett-recursive-upstream']} and the red dotted arrows indicate the applied $\beta$ value in Definition \ref{['def:arbitrary-prop-operators-ett-regulation']} for each inequality property.
• Figure 4: An overview of the case-study simulated scenarios. The blue vehicle corresponds to the ACC vehicle which can measure its own speed ($v$), the distance to the preceding vehicle in the same lane $x_{p}$ and the distance to the preceding $x_{l_o, p}$ and following $x_{l_o, f}$ vehicles in the fast lane in the multi-lane scenario.
• Figure 5: A contour plot of $\epsilon_{v, \varphi_a}$ and $\epsilon_{x_\Delta, \varphi_a}$ parameter combinations where the red area indicates a feasible configuration and the grey hatched area indicates an infeasible configuration. The white area indicates untested parameter configurations. The shade of red indicates the average number of transmitted measurements.

Theorems & Definitions (31)

• Example 1: SOD Event-trigger
• Definition 1: Modified Kalman filter adapted from suhModifiedKalmanFilter2007
• Definition 2: Robustness adapted from malerMonitoringTemporalProperties2004
• Lemma 1
• proof
• Lemma 2
• proof
• Definition 3
• Proposition 1
• Example 2: Robustness interval