Oleg Sokolsky

Cyber-physical systems (CPS) play a pivotal role in industrial automation, transportation, and critical infrastructure, where meeting stringent timing constraints is essential to ensure operational safety and efficiency. While reinforcement learning (RL) has shown promise in synthesizing controllers for time-critical applications, existing approaches often prioritize speed (as soon as possible, or ASAP) without explicitly addressing deadline compliance. This misalignment can lead to unsafe or suboptimal behaviors, which are unacceptable in industrial contexts requiring both safety and reliability under hard deadlines. For example, with inappropriate rewards, a control policy for a industrial robot can be encouraged to be less safe but fast instead of being steady and meeting the deadlines. To address this challenge, we investigate the relationship between ASAP behavior and deadline-safe behavior, introducing a novel Markov decision process formulation (R-MDP) that includes time-awareness while preserving the Markov property. We propose a reward design method that systematically encourages deadline compliance and guarantees safety in reach-avoid tasks. Our approach is validated on multiple benchmarks, including linear and nonlinear systems representative of industrial applications, such as DC motor control and real-time attitude control. Experimental results demonstrate the efficacy of our method in achieving deadline-safe control while maintaining system safety, offering a reliable solution for industrial CPS where failure to meet deadlines can have severe consequences.

Prolonged loneliness in older adults increases the risk of dementia, cardiovascular diseases, and premature death. However, timely detection and behavioral pattern analysis are challenging due to the slow progression of loneliness and diverse individual lifestyles. To address these barriers, we propose SMILE, an end-to-end framework for sensor-driven detection and counterfactual pattern analysis of loneliness. Our approach uses non-intrusive sensors to passively observe behavior and build a personalized profile over time. When SMILE detects meaningful changes in activity patterns, it employs generative models to produce counterfactual sensor profiles—synthetic representations of behavior predicted to result in lower loneliness scores. Suggested pattern changes are identified as the difference between observed and counterfactual profiles, highlighting the behaviors most associated with loneliness. We conducted a 6-month feasibility study with 18 participants from the United States and 15 from Japan to develop and evaluate SMILE. Our framework integrates a Time-series Transformer (TST) model for loneliness detection, which achieved 96.25% accuracy, and a diffusion model for generating behavioral explanations, which outperformed a baseline by up to 76.69%. These findings highlight the potential of SMILE to support sensor-driven, personalized loneliness detection and behavioral explanation in aging populations.

Social isolation and loneliness pose critical health risks to elderly populations, with mortality impacts that rival smoking and obesity. The COVID-19 pandemic has intensified these risks and exposed the limitations of current monitoring approaches. Most sensor-based monitoring systems remain impractical for wide deployment due to their complex maintenance needs and heavy technical overhead. They often demand dense sensor networks, frequent interventions, and substantial infrastructure - barriers that prevent adoption beyond controlled research settings. To address these challenges, we present a simplified sensing system that enables practical monitoring of elderly loneliness across different cultural contexts. Our approach uses a small set of carefully chosen sensors to capture key behavioral indicators while minimizing maintenance needs. Tests with 33 participants across Japan and US senior communities demonstrate practical accuracy (MAE = 3.98 for Japan and MAE = 6.35 for the US) with significantly reduced complexity. Post-deployment feedback revealed high system acceptability and low privacy concerns among participants, supporting the feasibility of long-term monitoring. The deployments revealed several differences in how social isolation manifests across cultures - from sleep patterns to activity rhythms. Through systematic feature selection based on these behavioral differences, we achieved improved predictive performance.We detail the technical architecture, deployment methods, and maintenance protocols needed for community-scale implementation. Our results show that effective elderly monitoring is possible without a large number of sensors, opening the path for sustainable, community-managed deployments.

Neural network (NN)-based control policies have proven their advantages in cyber-physical systems (CPS). When an NN-based policy fails to fulfill a formal specification, engineers leverage NN repair algorithms to fix its behaviors. However, such repair techniques risk breaking the existing correct behaviors, losing not only correctness but also verifiability of initial state subsets. That is, the repair may introduce new risks, previously unaccounted for. In response, we formalize the problem of Repair with Preservation (RwP) and develop Incremental Simulated Annealing Repair (ISAR). ISAR is an NN repair algorithm that aims to preserve correctness and verifiability—while repairing as many failures as possible. Our algorithm leverages simulated annealing on a barriered energy function to safeguard the already-correct initial states while repairing as many additional ones as possible. Moreover, formal verification is utilized to guarantee the repair results. ISAR is compared to a reviewed set of state-of-the-art algorithms, including (1) reinforcement learning-based techniques (STLGym and F-MDP), (2) supervised learning-based techniques (MIQP and minimally deviating repair) and (3) online shielding techniques (tube MPC shielding). Upon evaluation on two standard benchmarks, OpenAI Gym mountain car and an unmanned underwater vehicle, ISAR not only preserves correct behaviors from previously verified initial state regions, but also repairs 81.4% and 23.5% of broken state spaces in the two benchmarks. Moreover, the signal temporal logic (STL) robustness of the ISAR-repaired policies is higher than the baselines.

The safety of learning-enabled cyber-physical systems is compromised by the well-known vulnerabilities of deep neural networks to out-of-distribution (OOD) inputs. Existing literature has sought to monitor the safety of such systems by detecting OOD data. However, such approaches have limited utility, as the presence of an OOD input does not necessarily imply the violation of a desired safety property. We instead propose to directly monitor safety in a manner that is itself robust to OOD data. To this end, we predict violations of signal temporal logic safety specifications based on predicted future trajectories. Our safety monitor additionally uses a novel combination of adaptive conformal prediction and incremental learning. The former obtains probabilistic prediction guarantees even on OOD data, and the latter prevents overly conservative predictions. We evaluate the efficacy of the proposed approach in two case studies on safety monitoring: 1) predicting collisions of an F1Tenth car with static obstacles, and 2) predicting collisions of a race car with multiple dynamic obstacles. We find that adaptive conformal prediction obtains theoretical guarantees where other uncertainty quantification methods fail to do so. Additionally, combining adaptive conformal prediction and incremental learning for safety monitoring achieves high recall and timeliness while reducing loss in precision. We achieve these results even in OOD settings and outperform alternative methods.

Anomaly detection is widely used for identifying critical errors and suspicious behaviors, but current methods lack interpretability. We leverage common properties of existing methods and recent advances in generative models to introduce counterfactual explanations for anomaly detection. Given an input, we generate its counterfactual as a diffusion-based repair that shows what a non-anomalous version should have looked like. A key advantage of this approach is that it enables a domain-independent formal specification of explainability desiderata, offering a unified framework for generating and evaluating explanations. We demonstrate the effectiveness of our anomaly explainability framework, AR-Pro, on vision (MVTec, VisA) and time-series (SWaT, WADI, HAI) anomaly datasets. The code used for the experiments is accessible at: https://github.com/xjiae/arpro.

Uncertainty in the predictions of learning-enabled components hinders their deployment in safety-critical cyber-physical systems (CPS). A shift from the training distribution of a learning-enabled component (LEC) is one source of uncertainty in the LEC’s predictions. Detection of this shift or out-of-distribution (OOD) detection on individual datapoints has therefore gained attention recently. But in many applications, inputs to CPS form a temporal sequence. Existing techniques for OOD detection in time-series data for CPS either do not exploit temporal relationships in the sequence or do not provide any guarantees on detection. We propose using deviation from the in-distribution temporal equivariance as the non-conformity measure in conformal anomaly detection framework for OOD detection in time-series data for CPS. Computing independent predictions from multiple conformal detectors based on the proposed measure and combining these predictions by Fisher’s method leads to the proposed detector CODiT with bounded false alarms. CODiT performs OOD detection on fixed-length windows of consecutive time-series datapoints by using Fisher value of the input window. We further propose performing OOD detection on real-time time-series traces of variable lengths with bounded false alarms. This can be done by using CODiT to compute Fisher values of the sliding windows in the input trace and combining these values by a merging function. Merging functions such as Harmonic Mean, Arithmetic Mean, Geometric Mean, Bonferroni Method, and so on, can be used to combine Fisher values of the sliding windows in the input trace, and the combined value can be used for OOD detection on the trace with bounded false alarm rate guarantees. We illustrate the efficacy of CODiT by achieving state-of-the-art results in two case studies for OOD detection on fixed-length windows. The first one is on an autonomous driving system with perception (or vision) LEC. The second case study is on a medical CPS for walking pattern or GAIT analysis where physiological (non-vision) data is collected with force-sensitive resistors attached to the subject’s body. For OOD detection on variable length traces, we consider the same case studies on the autonomous driving system and medical CPS for GAIT analysis. We report our results with four merging functions on the Fisher values computed by CODiT on the sliding windows of the input trace. We also compare the false alarm rate guarantees by these four merging functions in the autonomous driving system case study. Code, data, and trained models are available at https://github.com/kaustubhsridhar/time-series-OOD .