ABSTRACT. Synthesizing safety controllers for general nonlinear systems is a highly challenging task, particularly when the system models are unknown, and input constraints are present. While some recent efforts have explored data-driven safety controller design for nonlinear systems, these approaches are primarily limited to specific classes of nonlinear dynamics (e.g., polynomials) and are not applicable to general nonlinear systems. This paper develops a direct data-driven approach for discrete-time general nonlinear systems, facilitating the simultaneous learning of control barrier certificates (CBCs) and dynamic controllers to ensure safety properties under input constraints. Specifically, by leveraging the adding-one-integrator approach, we incorporate the controller’s dynamics into the system dynamics to synthesize a virtual static-feedback controller for the augmented system, resulting in a dynamic safety controller for the actual dynamics. We collect input-state data from the augmented system during a finite-time experiment, referred to as a single trajectory. Using this data, we learn augmented CBCs and the corresponding virtual safety controllers, ensuring the safety of the actual system and adherence to input constraints over a finite time horizon. We demonstrate that our proposed conditions boil down to some data-dependent linear matrix inequalities (LMIs), which are easy to satisfy. We demonstrate the effectiveness of our data-driven approach through a case study involving highly nonlinear terms with unknown dynamics.

ABSTRACT. We offer a compositional data-driven scheme for synthesizing controllers that ensure global asymptotic stability (GAS) across large-scale interconnected networks, characterized by unknown mathematical models. In light of each network's configuration composed of numerous subsystems with smaller dimensions, our proposed framework gathers data from each subsystem's trajectory, enabling the design of local controllers that ensure input-to-state stability (ISS) properties over subsystems, signified by ISS Lyapunov functions. To accomplish this, we require only a single input-state trajectory from each unknown subsystem up to a specified time horizon, fulfilling certain rank conditions. Subsequently, under small-gain compositional reasoning, we leverage ISS Lyapunov functions derived from data to offer a control Lyapunov function (CLF) for the interconnected network, ensuring GAS certificate over the network. We demonstrate that while the computational complexity for designing a CLF increases polynomially with the network dimension using sum-of-squares (SOS) optimization, our compositional data-driven approach significantly mitigates it to linear with respect to the number of subsystems. We showcase the efficacy of our data-driven approach over a set of benchmarks, involving physical networks with diverse interconnection topologies.

ABSTRACT. In recent years, many different methods for identifying hybrid automata from data have been proposed. However, most of these methods consider clean simulator data, and consequently do not perform well for noisy data measured from real systems. We address this shortcoming with a new approach for the identification of hybrid automata that is specifically designed to be robust to noise. In particular, we propose a new high-level strategy consisting of the following three steps: clustering based on the dynamics identified from a local dataset, state space partitioning using decision trees, and conversion of the decision tree to a hybrid automaton. In addition, we introduce several new concepts for the realization of the single steps. For example, we propose an automated regularization of the dynamic models used for clustering via rank adaption, as well as a new variant of the Gini impurity index for decision tree learning, tailored toward hybrid systems where different dynamics can be active within the same state space region. As our experiments on 19 challenging benchmarks with different characteristics demonstrate, in addition to being robust to both process and measurement noise, our approach avoids the need for extensive hyper-parameter tuning and also performs well for clean data without noise.

ABSTRACT. We present a neural network verification toolbox to 1) assess the probability of satisfaction of a constraint, and 2) synthesize a set expansion factor to achieve the probability of satisfaction. Specifically, the tool box establishes with a user-specified level of confidence whether the output of the neural network for a given input distribution is likely to be contained within a given set. Should the tool determine that the given set cannot satisfy the likelihood constraint, the tool also implements an approach outlined in this paper to alter the constraint set to ensure that the user-defined satisfaction probability is achieved. The toolbox is comprised of sampling-based approaches which exploit the properties of signed distance function to define set containment.

ABSTRACT. Occupancy sensing is essential for vehicle safety and security applications such as seat belt reminders, airbag deployment, intrusion detection, and child-left-behind alerts. This paper presents UMusic, a novel in-car occupancy sensing system that reuses the ultra-wideband (UWB) devices already installed for access control in modern vehicles. However, due to the compact size and metal structure, the in-car environment is full of reflected propagation paths, which cannot be precisely resolved even with UWB's wide-bandwidth feature. To overcome this challenge, UMusic introduces a reflected-path decomposition technique to extract a high-resolution power delay profile (PDP) from the channel impulse response (CIR) provided by commodity UWB devices, enabling precise environmental perception. By comparing PDPs in empty and occupied conditions, UMusic is able to detect the occupancy status in both a sedan and an SUV with multiple passengers across various scenarios. Our results show that UMusic achieves a 90.2% detection rate using a single CIR measurement collected within 50 ms, outperforming the state-of-the-art by 15.7%. When aggregating six consecutive CIR measurements, UMusic reaches 99.4% accuracy, demonstrating its effectiveness for real-world deployment.

ABSTRACT. Using 3D hand poses as the input of user interfaces can enable many novel human-computer interaction applications. However, conventional solutions for precisely reconstructing the hand poses are either vision-based, which are compute-intensive and may cause privacy issues, or wearable devices-based, which are intrusive to users. In this paper, we propose RAM-Hand, a Robust Acoustic 3D Multi-Hand pose reconstruction system built on a microphone array. Our RAM-Hand system can support multiple hands and is designed for high adaptability to new scenarios with limited training data. Specifically, it should robustly accommodate variations in environment, subject, and hand positions. To achieve this, on one hand, we propose a customized signal processing pipeline to segment multiple hands' reflections and extract the features corresponding to each hand, then feed those features into a transformer-based neural network for precise pose reconstruction. On the other hand, to tackle the challenge that the training data is limited, we propose a series of data augmentation methods to generate virtual training data, and utilize contrastive learning to ensure our model behaves well on new subjects. We conduct extensive experiments on a real-world microphone array testbed to evaluate the performance of the proposed system. The results show that our RAM-Hand system can localize each hand joint with an average error of 10.71 mm, handle multiple hands, and generalize well to the above mentioned new scenarios.

ABSTRACT. We present LeekyFeeder, a mobile application that explores the acoustic signals leaked from headphones to reconstruct gesture motions around the ear for fine-grained gesture control.To achieve this goal, LeekyFeeder repurposes the speaker and a single feed-forward microphone on active noise cancellation (ANC) headphones as a SONAR system, using inaudible frequency-modulated continuous-wave (FMCW) signals to track gesture reflections for accurate sensing. Since this single-receiver  SONAR system is unable to differentiate reflection angles and further disentangle signal reflections from different gesture parts, we draw on principles of multi-modal learning to frame gesture motion reconstruction as a multi-modal translation task and propose a deep learning-based approach to fill the information gap between low-dimensional FMCW ranging readings and high-dimensional 3D hand movements. We implement LeekyFeeder on a pair of Google Pixel Buds and conduct experiments to examine the efficacy and robustness of LeekyFeeder in various conditions. Experiments based on six gesture types inspired by Apple Vision Pro demonstrate that LeekyFeeder achieves a PCK performance of 89% at 3cm across ten users, with an average MPJPE and MPJRPE error of 2.71cm and 1.88cm, respectively.

ABSTRACT. We propose LightLLM, a model that fine tunes pre-trained large language models (LLMs) for light-based sensing tasks. It integrates a sensor data encoder to extract key features, a contextual prompt to provide environmental information, and a fusion layer to combine these inputs into a unified representation. This combined input is then processed by the pre-trained LLM, which remains frozen while being fine-tuned through the addition of lightweight, trainable components, allowing the model to adapt to new tasks without altering its original parameters. This approach enables flexible adaptation of LLM to specialized light sensing tasks with minimal computational overhead and retraining effort. We have implemented LightLLM for three light sensing tasks: light-based localization, outdoor solar forecasting, and indoor solar estimation. Using real-world experimental datasets, we demonstrate that LightLLM significantly outperforms state-of-the-art methods, achieving 4.4x improvement in localization accuracy and 3.4x improvement in indoor solar estimation when tested in previously unseen environments. We further demonstrate that LightLLM outperforms ChatGPT-4 with direct prompting, highlighting the advantages of LightLLM's specialized architecture for sensor data fusion with textual prompts.

ABSTRACT. Sensing friction coefficient is vital for various cyber-physical system applications, including robotic grasping. We present RoboTera, a novel system for the non-contact coefficient of friction (COF) estimation using sub-Terahertz (sub-THz) perception in robotics for the first time. While advanced tactile sensors can provide friction inputs, they require direct contact, which might not be suitable for various applications. Non-contact estimation of friction between the gripper and a target object requires extracting the minute surface perturbations which is unfortunately not supported by existing imaging modalities (such as camera and LiDAR). Our key insight is that sub-THz signals are best suited to infer such information as their sub-millimeter wavelength is comparable with surface perturbations. Hence, impinging sub-THz waves on everyday objects creates diffuse backscattering whose spectral profile hints at surface texture properties. Leveraging this, we use sub-THz wireless signals to extract surface roughness. By integrating sub-THz-estimated roughness inputs with conventional image-based material classification schemes, RoboTera provides a non-contact and precise COF inference framework. Further, we exploit COF inferences to identify stable grasp configurations and improve grasping performance. Our experiments demonstrate an average accuracy of over 92% in COF estimation. We implemented RoboTera on a robotic arm to assess its real-world grasping performance, achieving a 31.8% average improvement across objects with diverse COF profiles and shapes.

ABSTRACT. As assisted and autonomous driving systems become more prevalent, the need for accurate interpretation of road traffic signs is critical for driving safety and functionality. Current camera-based recognition methods face challenges due to the variability of traffic signs and environmental conditions, leading to potential inaccuracies. To address this, we propose LiDARMarker, a type of machine-readable traffic sign using infrared materials, making it invisible to human drivers but detectable by LiDAR-equipped vehicles. This paper introduces the design, fabrication, and efficient decoding methods of LiDARMarker. LiDARMarker is tailored to the emerging capabilities and needs of modern vehicles, enhancing their ability and accuracy in traffic sign recognition while avoiding interference with human drivers. Through the proposal of LiDARMarker, we aim to inspire the rethinking of the design of traffic sign systems in the context of modern vehicles.

ABSTRACT. Modern cyber-physical systems (CPS) can consist of various networked components and agents interacting and communicating with each other. In the context of spatially distributed CPS, these connections can be dynamically dependent on the spatial configuration of the various components and agents. In these settings, robust monitoring of the distributed components is vital to ensuring complex behaviors are achieved, and safety properties are maintained. To this end, we look at defining the automaton semantics for the Spatio-Temporal Reach and Escape Logic (STREL), a formal logic designed to express and monitor spatio-temporal requirements over mobile, spatially distributed CPS. Specifically, STREL reasons about spatio-temporal behavior over dynamic weighted graphs. While STREL is endowed with well defined qualitative and quantitative semantics, in this paper, we propose a novel construction of (weighted) alternating finite automata from STREL specifications that efficiently encodes these semantics. Moreover, we demonstrate how this automaton semantics can be used to perform both, offline and online monitoring for STREL specifications using a simulated drone swarm environment.

ABSTRACT. Cyber-Physical Systems (CPSs), especially those involving autonomy, need guarantees of their safety. Runtime Enforcement (RE) is a lightweight method to formally ensure that some specified properties are satisfied over the executions of the system. Hence, there is recent interest in the RE of CPS. However, existing methods are not designed to tackle specifications suitable for the hybrid dynamics of CPS. With this in mind, we develop runtime enforcement of CPS using properties defined in Signal Temporal Logic (STL).In this work, we aim to construct a runtime enforcer for a given STL formula to minimally modify a signal to satisfy the formula. To achieve this, the STL formula to be enforced is first translated into a timed transducer, while the signal to be corrected is encoded as timed words. We provide timed transducers for the temporal operators \emph{until} and \emph{release} noting that other temporal operators can be expressed using these two. Our approach enables effective enforcement of STL properties for CPS. A case study is provided to illustrate the approach and generate empirical evidence of its suitability for CPS.

ABSTRACT. Autonomous systems are integral to many safety-critical applications, such as industrial automation, autonomous vehicles, and the Industrial Internet of Things (IIoT). The verification of both functional and temporal correctness of these systems is crucial prior to deployment to ensure safety. However, due to the interaction of continuous-time dynamics in physical systems and discrete-time constraints in computational models, achieving end-to-end verification poses significant challenges. A promising solution is the development of a comprehensive "digital twin"---a model-based twin that mirrors the real system’s physical and computational behaviors. By creating this digital twin, we can rigorously assess and verify the system’s correctness within a virtual framework, capturing both physical dynamics and computational requirements. Most existing works in the real-time systems community are focused only on formal proofs of the temporal correctness of computational models, whereas the control system community addresses the continuous dynamics of physical processes and how to control them within `provided' real-time constraints. Unlike those, this digital twin approach allows for an integrated verification process that addresses both physical models and timing requirements, as well as their deep correlation concurrently. This paper introduces SOTERIA\footnote{SOTERIA was the Greek goddess of safety, deliverance, and preservation from harm.}, a hybrid formal framework serving as a ``model twin" for autonomous systems' safety verification. As a model twin, SOTERIA functions as an end-to-end digital twin for the target system, integrating both physical and computational aspects to facilitate comprehensive verification. By modeling the physical system's hybrid dynamics alongside the computational model and the operating environment, SOTERIA enables a rigorous safety assurance process that verifies both functional and temporal correctness. Using well-established verification tools, SOTERIA ensures that end-to-end latencies align with formal specifications, bridging the gap between computational and physical requirements. An extensive case study on the F1Tenth racing car demonstrates SOTERIA's capabilities, leveraging \uppaal to achieve superior results in worst-case latency and safe operational environments, yielding more verified safe racing tracks compared to conventional schedulability analyses. This digital twin-based approach underscores the importance of a cohesive verification strategy that enhances safety and reliability in autonomous systems.

ABSTRACT. Hybrid games are a powerful framework for modelling interactions between cyber-physical systems (CPS). While their high level of nondeterminism allows the modelling of complex systems, it also makes many properties undecidable. This paper presents Hybrid Games with Triggers (HGT), an extension that reduces nondeterminism by embedding agents’ rational decision-making as triggers - conditions that, when met, prompt the agents to act. This approach leads to a time-abstract discrete game with a countable state space, where an agent has a winning strategy in the discrete game if and only if they do in the HGT. Our discretisation preserves both the continuous and discrete dynamics of the original hybrid game, providing a more structured, analysable model without sacrificing dynamic expressivity.

ABSTRACT. Code Large Language Models (LLMs) enhance software development efficiency by automatically generating code and documentation in response to user requirements. However, code LLMs cannot synthesize specialized programs when tasked with IoT applications that require domain knowledge. While Retrieval-Augmented Generation (RAG) offers a promising solution by fetching relevant domain knowledge, it necessitates powerful cloud LLMs (e.g., GPT-4) to process user requirements and retrieved contents, which raises significant privacy concerns. This approach also suffers from unstable networks and prohibitive LLM query costs. Moreover, it is challenging to ensure the correctness and relevance of the fetched contents. To address these issues, we propose GPIoT, a code generation system for IoT applications by fine-tuning locally deployable Small Language Models (SLMs) on IoT-specialized datasets. SLMs have smaller model sizes, allowing efficient local deployment and execution to mitigate privacy concerns and network uncertainty. Furthermore, by fine-tuning the SLMs with our IoT-specialized datasets, the SLMs' ability to synthesize IoT-related programs can be substantially improved. To evaluate GPIoT's capability in synthesizing programs for IoT applications, we develop a benchmark, IoTBench. Extensive experiments and user trials demonstrate the effectiveness of GPIoT in generating IoT-specialized code, outperforming state-of-the-art code LLMs with an average task accuracy increment of 64.7% and significant improvements in user satisfaction.

ABSTRACT. An increasing number of environments, such as smart homes and factories, are being equipped with multiple sensor systems to enable diverse intelligent applications. However, most existing sensor coordination systems require manually predefined rules, limiting their ability to handle flexible and complex tasks. While recent approaches leverage large language models (LLMs) to interact with external APIs, they struggle to fully understand the capabilities and data dependencies of practical sensor systems. This paper introduces TaskSense, a novel system that coordinates multiple sensor systems in response to users' complex queries. TaskSense introduces a sensor language that automatically translates the capabilities and data dependencies of sensor systems into vocabularies and grammar rules that can be understood by LLMs. It then interprets user intentions into executable task plans for sensor systems using this sensor language in combination with LLMs. Meanwhile, TaskSense checks the solvability of user queries and verifies the correctness of task plan dependencies. To further enhance robustness, TaskSense incorporates a dynamic plan execution mechanism that adjusts plans based on real-time feedback from sensor data availability, data quality and execution results. TaskSense is deployed on real-world smart home systems, utilizing six popular LLMs. The system is evaluated across 4 scenarios involving 9 types of sensor systems, over 60 APIs, 170 tasks and 5 types of data modalities. Results show that TaskSense achieves up to 2× higher planning accuracy and a 75% increase in answer accuracy using the similar amount of tokens compared with baseline approaches.

ABSTRACT. Self-supervised learning enables effective model pre-training on large-scale unlabeled data, which is crucial for user-specific fine-tuning in mobile sensing applications. However, pre-trained models often face significant domain shifts during fine-tuning due to user diversity, leading to performance degradation. To address this, we propose SelfReplay, an adaptive approach designed to align self-supervised models to different domains. SelfReplay consists of two stages: MetaSSL, which leverages meta-learning with self-supervised learning to pre-train domain-adaptive weights, and ReplaySSL, which further adapts the pre-trained model to each user's domain by replaying the meta-learned self-supervised task with a few user-specific samples. This produces a personalized model tailored to each user. Evaluations on mobile sensing benchmarks demonstrate that SelfReplay outperforms existing baselines, improving the F1-score by 9.4%p on average. On-device analyses on a commodity smartphone show the efficiency of SelfReplay's adaptation step, required just once after deployment, with SimCLR completing in only 10 seconds while using less than 100MB of memory.

ABSTRACT. This paper presents Babel, the expandable modality alignment model, specially designed for multi-modal sensing. While there has been considerable work on multi-modality alignment, they all struggle to effectively incorporate multiple sensing modalities due to the data scarcity constraints. How to utilize multi-modal data with partial pairings in sensing remains an unresolved challenge.

Babel tackles this challenge by introducing the concept of expandable modality alignment. The key idea involves transforming the N-modality alignment into a series of binary-modality alignments. Novel techniques are also proposed to further mitigate data scarcity issue and balance the contribution of the newly incorporated modality with the previously established modality alignment during the expandable alignment process. We provide the comprehensive implementation. In the pre-training phase, Babel currently aligns 6 sensing modalities, namely Wi-Fi, mmWave, IMU, LiDAR, video, and depth. For the deployment phase, as a foundation model, any single or combination of aligned modalities could be selected from Babel and applied to downstream tasks.

Evaluation demonstrates Babel's outstanding performance on eight human activity recognition datasets, compared to a broad range of baselines e.g., the SOTA single-modal sensing networks, multi-modal sensing framework, and multi-modal large language models. Babel not only improves the performance of individual modality sensing (12% averaged accuracy improvement), but also effectively fuses multiple available modalities (up to 22% accuracy increase). Case studies also highlight emerging application scenarios empowered by Babel, including cross-modality retrieval (i.e.,sensing imaging), and bridging LLMs for sensing comprehension.

ABSTRACT. This paper explores sensor-informed personal agents that can take advantage of sensor hints on wearables to enhance the personal agent's response. We demonstrate that such a sensor-in-the-loop AI agent design can be easily integrated into existing LLM agents by building a prototype named WellMax based on existing well-developed techniques such as structured prompt templates and few-shot prompting. The head-to-head comparison with a non-sensor-informed agent across five use scenarios demonstrates that this sensor-in-the-loop design can effectively improve users' needs and their overall experience. The deep-dive into agents' replies and participants' feedback further reveals that sensor-in-the-loop agents not only provide more contextually relevant responses but also exhibit a better understanding of user priorities and situational nuances. In addition, we conduct two case studies to examine the potential pitfalls and distill key insights from this sensor-in-the-loop agent. We hope this work can spawn new ideas for building more intelligent, empathetic, and effective AI-driven personal assistants.

ABSTRACT. Wireless sensing technologies, leveraging ubiquitous sensors such as acoustics or mmWave, can enable various applications such as human motion and health tracking. However, the recent trend of incorporating deep learning into wireless sensing introduces new challenges, such as the need for extensive training data and poor model generalization. As a remedy, data augmentation is one solution well-explored in other fields such as computer vision; yet they are not directly applicable due to the unique characteristics of wireless signals. Hence, we propose a custom data augmentation framework, WixUp, tailored for wireless human sensing. Our goal is to build a generic data augmentation framework applicable to various tasks, models, data formats, or wireless modalities. Specifically, WixUp achieves this by a custom Gaussian mixture and probability-based transformation, making any data formats capable of an in-depth augmentation at the dense range profile level.Additionally, our mixing-based augmentation enables unsupervised domain adaptation via self-training, allowing model training with no ground truth labels from new users or environments in practice.We extensively evaluated WixUp across four datasets of two sensing modalities (mmWave, acoustics), two model architectures, and three tasks (pose estimation, identification, action recognition). WixUp provides consistent performance improvement (2.79%-84.25%) across these various scenarios and outperforms other data augmentation baselines.

ABSTRACT. We present the idea of successive control barrier functions for nonlinear (polynomial) control systems. Control Barrier Functions (CBFs) can be used to maintain safety properties for a system through the online modification of control inputs to ensure that the state remains inside a controlled invariant set that excludes a set of unsafe states. However, the synthesis of CBFs is quite difficult in practice, especially for nonlinear dynamical systems. Computationally inexpensive approaches employ relaxed control barrier conditions that result in relatively small control invariant sets. In turn, this can result in unnecessary modification of the nominal control input to keep the dynamics inside this set.

In this paper, we propose the concept of "successive" CBFs.Rather than rely on a single CBF, our approach uses a hierarchy of functions wherein functions at one level of a hierarchybecome active only if the functions at the previous levels have failed. Using a well-known approach to finding barrierfunctions for polynomial dynamical systems using sum of squares optimization, we show how to adapt it to synthesize successive barrier functions. We also provide "transit time" guarantees to construct a chattering-free runtime enforcement scheme that avoids collisions with fixed obstacles. We demonstrate our approach on a set of interesting nonlinearbenchmarks, while comparing it with state of the art approaches for synthesizing CBFs.

ABSTRACT. Finding Lyapunov functions to certify the stability of control systems has been an important topic for certifying safety-critical systems. Most existing methods on finding Lyapunov functions require access to the dynamics of the system. Accurately describing the complete dynamics of a control system however remains highly challenging in practice. Latest trend of using learning-enabled control systems further reduces the transparency. Hence, a method for black-box systems would have much wider applications.

Our work stems from the idea of sampling and exploiting Lipschitz continuity to approximate the unknown dynamics. Given Lipschitz constants, one can derive a non-statistical upper bounds on approximation errors; hence a strong certification on this approximation can certify the unknown dynamics. We significantly improve this idea by directly approximating the Lie derivative of Lyapunov functions instead of the dynamics. We propose a framework based on the learner-verifier architecture from Counterexample-Guided Inductive Synthesis (CEGIS). Our insight of combining regional verification conditions and counterexample-guided sampling enables a guided search for samples to prove stability region-by-region. Our CEGIS algorithm further ensures termination.

Our numerical experiments suggest that it is possible to prove the stability of 2D and 3D systems with a few thousands of samples. In comparison with the existing black-box approach, our approach at the best case requires less than 0.01% of samples.

ABSTRACT. We present a counterexample-guided approach for synthesizing convex piecewise affine control Lyapunov functions, obtained as the maximumover a finite number of affine functions, for stabilizing switched linear systems. Our approachconsiders systems whose dynamics are defined by a set of affine ODEs over different regions of the state-space. The goal is to synthesize a control feedback functionthat uses state-based switching by assigning a dynamical mode to each state from the set of available dynamics. This is achieved by synthesizing a piecewise affinecontrol Lyapunov function that guarantees that for each state variable, the appropriate choice of a control input can cause an instantaneous decrease in the valueof the Lyapunov function. Since piecewise affine functions are not smooth, we use a non-smooth analytic characterization of piecewise affine Lyapunov functions.The key contribution of our approach is a counterexample driven algorithm that alternates between verification that a given convex PWA function is a control Lyapunovfunction or generating a counterexample point where the Lyapunov conditions fail, and synthesis from a finite set of counterexamples generated in the past.We demonstrate that the two steps can be performed using mixed integer linear programming problems (MILP) although no termination guarantees are possible. We show that the branch andcut approach used inside a MILP solver can be adapted to yield a termination guarantee. Although the resulting approach is computationally expensive, it has the advantage of not requiring a "demonstrator" or a pre-existing controller. We provide an empirical evaluation that explores the results of this approach over a set of numerical examples.