skip to main content


Title: A compositional framework for algebraic quantitative online monitoring over continuous-time signals
We investigate online monitoring algorithms over dense-time and continuous-time signals for properties written in metric temporal logic (MTL). We consider an abstract algebraic semantics based on complete lattices. This semantics includes as special cases the standard Boolean (qualitative) semantics and the widely-used real-valued robustness (quantitative) semantics. Our semantics also extends to truth values that are partially ordered and allows the modeling of uncertainty in satisfaction. We propose a compositional approach for the construction of online monitors that transform exact representations of piecewise constant (dense-time and continuous-time) signals. These monitors are based on a class of infinite-state deterministic signal transducers that (1) are allowed to produce the output signal with some bounded delay relative to the input signal, and (2) do not introduce unbounded variability in the output signal. A key ingredient of our monitoring framework is an efficient algorithm for sliding-window aggregation over dense-time signals. We have implemented and experimentally evaluated our monitoring framework by comparing it to the recently proposed online monitoring tools Reelay and RTAMT.  more » « less
Award ID(s):
2008096
NSF-PAR ID:
10475718
Author(s) / Creator(s):
; ;
Publisher / Repository:
Springer
Date Published:
Journal Name:
International Journal on Software Tools for Technology Transfer
Volume:
25
Issue:
4
ISSN:
1433-2779
Page Range / eLocation ID:
557 to 573
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. Continuous monitoring of respiration provides invaluable insights about health status management (e.g., the progression or recovery of diseases). Recent advancements in radio frequency (RF) technologies show promise for continuous respiration monitoring by virtue of their non-invasive nature, and preferred over wearable solutions that require frequent charging and continuous wearing. However, RF signals are susceptible to large body movements, which are inevitable in real life, challenging the robustness of respiration monitoring. While many existing methods have been proposed to achieve robust RF-based respiration monitoring, their reliance on supervised data limits their potential for broad applicability. In this context, we propose, RF-Q, an unsupervised/self-supervised model to achieve signal quality assessment and quality-aware estimation for robust RF-based respiration monitoring. RF-Q uses the recon- struction error of an autoencoder (AE) neural network to quantify the quality of respiratory information in RF signals without the need for data labeling. With the combination of the quantified sig- nal quality and reconstructed signal in a weighted fusion, we are able to achieve improved robustness of RF respiration monitor- ing. We demonstrate that, instead of applying sophisticated models devised with respective expertise using a considerable amount of labeled data, by just quantifying the signal quality in an unsupervised manner we can significantly boost the average end-to-end (e2e) respiratory rate estimation accuracy of a baseline by an improvement ratio of 2.75, higher than the gain of 1.94 achieved by a supervised baseline method that excludes distorted data. 
    more » « less
  2. Seismic monitoring systems sift through seismograms in real-time, searching for target events, such as underground explosions. In this monitoring system, a burst of aftershocks (minor earthquakes occur after a major earthquake over days or even years) can be a source of confounding signals. Such a burst of aftershock signals can overload the human analysts of the monitoring system. To alleviate this burden at the onset of a sequence of events (e.g., aftershocks), a human analyst can label the first few of these events and start an online classifier to filter out subsequent aftershock events. We propose an online few-shot classification model FewSig for time series data for the above use case. The framework of FewSig consists of a selective model to identify the high-confidence positive events which are used for updating the models and a general classifier to label the remaining events. Our specific technique uses a %two-level decision tree selective model based on sliding DTW distance and a general classifier model based on distance metric learning with Neighborhood Component Analysis (NCA). The algorithm demonstrates surprising robustness when tested on univariate datasets from the UEA/UCR archive. Furthermore, we show two real-world earthquake events where the FewSig reduces the human effort in monitoring applications by filtering out the aftershock events. 
    more » « less
  3. Abstract

    The use of air quality monitoring networks to inform urban policies is critical especially where urban populations are exposed to unprecedented levels of air pollution. High costs, however, limit city governments’ ability to deploy reference grade air quality monitors at scale; for instance, only 33 reference grade monitors are available for the entire territory of Delhi, India, spanning 1500 sq km with 15 million residents. In this paper, we describe a high-precision spatio-temporal prediction model that can be used to derive fine-grained pollution maps. We utilize two years of data from a low-cost monitoring network of 28 custom-designed low-cost portable air quality sensors covering a dense region of Delhi. The model uses a combination of message-passing recurrent neural networks combined with conventional spatio-temporal geostatistics models to achieve high predictive accuracy in the face of high data variability and intermittent data availability from low-cost sensors (due to sensor faults, network, and power issues). Using data from reference grade monitors for validation, our spatio-temporal pollution model can make predictions within 1-hour time-windows at 9.4, 10.5, and 9.6% Mean Absolute Percentage Error (MAPE) over our low-cost monitors, reference grade monitors, and the combined monitoring network respectively. These accurate fine-grained pollution sensing maps provide a way forward to build citizen-driven low-cost monitoring systems that detect hazardous urban air quality at fine-grained granularities.

     
    more » « less
  4. Runtime verificationis a lightweight method for monitoring the formal specification of a system during its execution. It has recently been shown that a given state predicate can be monitored consistently by a set of crash-prone asynchronousdistributedmonitors observing the system, only if each monitor can emit verdicts taken from alarge enoughfinite set. We revisit this impossibility result in the concrete context of linear-time logic (ltl) semantics for runtime verification, that is, when the correctness of the system is specified by anltlformula on its execution traces. First, we show that monitors synthesized based on the 4-valued semantics ofltl(rv-ltl) may result in inconsistent distributed monitoring, even for some simpleltlformulas. More generally, given anyltlformula φ, we relate the number of different verdicts required by the monitors for consistently monitoring φ, with a specific structural characteristic of φ called itsalternation number. Specifically, we show that, for everyk ≥ 0, there is anltlformula φ with alternation number kthat cannot be verified at runtime by distributed monitors emitting verdicts from a set of cardinality smaller thank+ 1. On the positive side, we define a family of logics, calleddistributedltl(abbreviated asdltl), parameterized byk≥ 0, which refinesrv-ltlby incorporating2k+ 4 truth values. Our main contribution is to show that, for everyk≥ 0, everyltlformula φ with alternation number kcan be consistently monitored by distributed monitors, each running an automaton based on a (2 ⌈k/2 ⌉ +4)-valued logic taken from thedltlfamily.

     
    more » « less
  5. We propose an interval extension of Signal Temporal Logic (STL) called Interval Signal Temporal Logic (I-STL). Given an STL formula, we consider an interval inclusion function for each of its predicates. Then, we use minimal inclusion functions for the min and max functions to recursively build an interval robustness that is a natural inclusion function for the robustness of the original STL formula. The resulting interval semantics accommodate, for example, uncertain signals modeled as a signal of intervals and uncertain predicates modeled with appropriate inclusion functions. In many cases, verification or synthesis algorithms developed for STL apply to I-STL with minimal theoretic and algorithmic changes, and existing code can be readily extended using interval arithmetic packages at negligible computational expense. To demonstrate I-STL, we present an example of offline monitoring from an uncertain signal trace obtained from a hardware experiment and an example of robust online control synthesis enforcing an STL formula with uncertain predicates. 
    more » « less