An official website of the United States government
We present ResilienC, a framework for resilient control of Cyber- Physical Systems subject to STL-based requirements. ResilienC uti- lizes a recently developed formalism for specifying CPS resiliency in terms of sets of (rec,dur) real-valued pairs, where rec repre- sents the system’s capability to rapidly recover from a property violation (recoverability), and dur is reflective of its ability to avoid violations post-recovery (durability). We define the resilient STL control problem as one of multi-objective optimization, where the recoverability and durability of the desired STL specification are maximized. When neither objective is prioritized over the other, the solution to the problem is a set of Pareto-optimal system trajectories. We present a precise solution method to the resilient STL control problem using a mixed-integer linear programming encoding and an a posteriori n-constraint approach for efficiently retrieving the complete set of optimally resilient solutions. In ResilienC, at each time-step, the optimal control action selected from the set of Pareto- optimal solutions by a Decision Maker strategy realizes a form of Model Predictive Control. We demonstrate the practical utility of the ResilienC framework on two significant case studies: autonomous vehicle lane keeping and deadline-driven, multi-region package delivery.
more »
« less
An STL-Based Formulation of Resilience in Cyber-Physical Systems
Resiliency is the ability to quickly recover from a violation and avoid future violations for as long as possible. Such a property is of fundamental importance for Cyber-Physical Systems (CPS), and yet, to date, there is no widely agreed-upon formal treatment of CPS resiliency. We present an STL-based framework for reasoning about resiliency in CPS in which resiliency has a syntactic characterization in the form of an STL-based Resiliency Specification (SRS). Given an arbitrary STL formula φ, time bounds α and β, the SRS of φ, Rα,β (φ), is the STL formula ¬φU[0,α]G[0,β)φ, specifying that recovery from a violation of φ occur within time α (recoverability), and subsequently that φ be maintained for duration β (durability). These R-expressions, which are atoms in our SRS logic, can be combined using STL operators, allowing one to express composite resiliency specifications, e.g., multiple SRSs must hold simultaneously, or the system must eventually be resilient. We define a quantitative semantics for SRSs in the form of a Resilience Satisfaction Value (ReSV) function r and prove its soundness and completeness w.r.t. STL’s Boolean semantics. The r-value for Rα,β (φ) atoms is a singleton set containing a pair quantifying recoverability and durability. The r-value for a composite SRS formula results in a set of non-dominated recoverability-durability pairs, given that the ReSVs of subformulas might not be directly comparable (e.g., one subformula has superior durability but worse recoverability than another). To the best of our knowledge, this is the first multi-dimensional quantitative semantics for an STL-based logic. Two case studies demonstrate the practical utility of our approach. https://doi.org/10.1007/978-3-031-15839-1_7
more »
« less
- Award ID(s):
- 1918225
- PAR ID:
- 10432253
- Editor(s):
- Bogomolov, Sergiy; Parker, David
- Date Published:
- Journal Name:
- Formal Modeling and Analysis of Timed Systems
- Page Range / eLocation ID:
- 117--135
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Predictive monitoring—making predictions about future states and monitoring if the predicted states satisfy requirements—offers a promising paradigm in supporting the decision making of Cyber-Physical Systems (CPS). Existing works of predictive monitoring mostly focus on monitoring individual predictions rather than sequential predictions. We develop a novel approach for monitoring sequential predictions generated from Bayesian Recurrent Neural Networks (RNNs) that can capture the inherent uncertainty in CPS, drawing on insights from our study of real-world CPS datasets. We propose a new logic named Signal Temporal Logic with Uncertainty (STL-U) to monitor a flowpipe containing an infinite set of uncertain sequences predicted by Bayesian RNNs. We define STL-U strong and weak satisfaction semantics based on whether all or some sequences contained in a flowpipe satisfy the requirement. We also develop methods to compute the range of confidence levels under which a flowpipe is guaranteed to strongly (weakly) satisfy an STL-U formula. Furthermore, we develop novel criteria that leverage STL-U monitoring results to calibrate the uncertainty estimation in Bayesian RNNs. Finally, we evaluate the proposed approach via experiments with real-world CPS datasets and a simulated smart city case study, which show very encouraging results of STL-U based predictive monitoring approach outperforming baselines.more » « less
-
We propose a novel passive learning approach, TeLex, to infer signal temporal logic (STL) formulas that characterize the behavior of a dynamical system using only observed signal traces of the system. First, we present a template-driven learning approach that requires two inputs: a set of observed traces and a template STL formula. The unknown parameters in the template can include time-bounds of the temporal operators, as well as the thresholds in the inequality predicates. TeLEx finds the value of the unknown parameters such that the synthesized STL property is satisfied by all the provided traces and it is tight. This requirement of tightness is essential to generating interesting properties when only positive examples are provided and there is no option to actively query the dynamical system to discover the boundaries of legal behavior. We propose a novel quantitative semantics for satisfaction of STL properties which enables TeLEx to learn tight STL properties without multidimensional optimization. The proposed new metric is also smooth. This is critical to enable the use of gradient-based numerical optimization engines and it produces a 30x to 100x speed-up with respect to the state-of-art gradient-free optimization. Second, we present a novel technique for automatically learning the structure of the STL formula by incrementally constructing more complex formula guided by the robustness metric of subformula. We demonstrate the effectiveness of the overall approach for learning STL formulas from only positive examples on a set of synthetic and real-world benchmarks.more » « less
-
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
-
The purpose of this study was to evaluate the use of compressible soft robotic sensors (C-SRS) in determining plantar pressure to infer vertical and shear forces in wearable technology: A ground reaction pressure sock (GRPS). To assess pressure relationships between C-SRS, pressure cells on a BodiTrakTM Vector Plate, and KistlerTM Force Plates, thirteen volunteers performed three repetitions of three different movements: squats, shifting center-of-pressure right to left foot, and shifting toes to heels with C-SRS in both anterior–posterior (A/P) and medial–lateral (M/L) sensor orientations. Pearson correlation coefficient of C-SRS to BodiTrakTM Vector Plate resulted in an average R-value greater than 0.70 in 618/780 (79%) of sensor to cell comparisons. An average R-value greater than 0.90 was seen in C-SRS comparison to KistlerTM Force Plates during shifting right to left. An autoregressive integrated moving average (ARIMA) was conducted to identify and estimate future C-SRS data. No significant differences were seen in sensor orientation. Sensors in the A/P orientation reported a mean R2 value of 0.952 and 0.945 in the M/L sensor orientation, reducing the effectiveness to infer shear forces. Given the high R values, the use of C-SRSs to infer normal pressures appears to make the development of the GRPS feasible.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1007/978-3-031-15839-1_7
