Artificial intelligence systems in critical fields like autonomous driving and medical imaging analysis often continually learn new tasks using a shared stream of input data. For instance, after learning to detect traffic signs, a model may later need to learn to classify traffic lights or different types of vehicles using the same camera feed. This scenario introduces a challenging setting we term Continual Multitask Learning (CMTL), where a model sequentially learns new tasks on an underlying data distribution without forgetting previously learned abilities. Existing continual learning methods often fail in this setting because they learn fragmented, task-specific features that interfere with one another. To address this, we introduce Learning with Preserving (LwP), a novel framework that shifts the focus from preserving task outputs to maintaining the geometric structure of the shared representation space. The core of LwP is a Dynamically Weighted Distance Preservation (DWDP) loss that prevents representation drift by regularizing the pairwise distances between latent data representations. This mechanism of preserving the underlying geometric structure allows the model to retain implicit knowledge and support diverse tasks without requiring a replay buffer, making it suitable for privacy-conscious applications. Extensive evaluations on time-series and image benchmarks show that LwP not only mitigates catastrophic forgetting but also consistently outperforms state-of-the-art baselines in CMTL tasks.

Federated Learning (FL) enables privacy-preserving model training across heterogeneous distributed systems, such as smartgrid forecasting or traffic-flow prediction from geographically dispersed sensors and devices. A key challenge in such settings is capturing client-specific patterns while addressing data heterogeneity and uncertainty at scale. Existing approaches, including Bayesian Neural Networks (BNNs) and clustering-based methods, struggle with scalability and consistent personalization. We propose LogiCP, a novel FL framework that integrates formal logic reasoning with uncertainty quantification (UQ) to support scalable and personalized learning with theoretical guarantees. LogiCP uses Signal Temporal Logic (STL) to extract temporal patterns and form semantically coherent client clusters, controlling intra-cluster heterogeneity. Within each cluster, LogiCP applies decentralized Conformal Prediction (CP) to produce distribution-free prediction intervals with mathematical guarantees that encompass the real value. LogiCP dynamically assigns clients to clusters at runtime without retraining, improving practicality. Evaluations on three real-world datasets—traffic, temperature, and electricity—show that LogiCP consistently outperforms BNN-, clustering-, and CP-based baselines, achieving up to a 95% improvement in client-level MSE while maintaining strong scalability.

As deep neural networks are deployed in safety-critical domains such as autonomous driving and medical diagnosis, stakeholders need explanations of model behavior that are not only interpretable but also trustworthy with formal guarantees. Existing XAI methods fall short of this requirement: heuristic attribution techniques (e.g., LIME, Integrated Gradients) highlight influential features for individual predictions but offer no mathematical guarantees about decision boundaries, while formal explanation methods verify robustness properties yet remain untargeted, analyzing the nearest boundary regardless of whether it represents a critical risk. In safety-critical systems, however, not all misclassifications carry equal consequences; confusing a “Stop” sign for a “60 kph” sign is far more dangerous than confusing it with a “No Passing” sign. Practitioners therefore lack a principled way to answer a fundamental safety question: how resilient is a model’s classification against a specific, high-risk alternative? We introduce ViTaX (Verified and Targeted Explanations), a formal XAI framework that addresses this gap by generating targeted semifactual explanations with mathematical guarantees. For a given input (class y) and a user-specified critical alternative (class t), ViTaX performs two key steps: (1) it identifies the minimal feature subset most sensitive to the y → t transition using class-specific sensitivity heuristics, and (2) it applies formal reachability analysis to guarantee that perturbing these features by ε is insufficient to flip the classification to t. This guarantee constitutes a verified semifactual: “even if these critical features change by ε classification y persists against t." We formalize this reasoning through Targeted ε-Robustness, a formal property that certifies whether an identified feature subset remains robust under perturbation toward a specific target class. By unifying semifactual explanations, class-specific targeting, and formal verification, ViTaX is the first method to provide formally guaranteed explanations of a model’s resilience against specific, user-identified alternatives. Our evaluations on image classification (MNIST, GTSRB, EMNIST) and regression (TaxiNet) demonstrate that ViTaX achieves significantly higher fidelity (e.g., over 30% improvement) and minimal explanation cardinality compared to existing methods. These results establish ViTaX as a scalable and trustworthy foundation for verifiable, targeted XAI.

Wearable cameras provide an efficient and convenient way to record our lives, supporting real-time documentation and analysis across various domains. Recent research has explored diverse methods for temporal segmentation, which aim to transform unstructured video data into structured events. This transformation facilitates deeper video understanding, optimizes computational resources, and improves the accessibility and interpretability of video content for both machines and humans. However, unlike conventional videos, wearable camera recordings present unique challenges. These include highly unstable camera perspectives, diverse activities across various environments, and flexible duration. As a result, traditional temporal segmentation methods often fail to return effective results. This paper introduces SmartSeg, an unsupervised, non-parametric approach for segmenting wearable camera videos without labeled data. By capturing the fundamental meanings of the video, SmartSeg aggregates the video through the Temporal Self-Similarity Metric encoder and groups sequences of frames into coherent events through clustering techniques. We evaluated SmartSeg on three diverse datasets. We achieved a 50% increase in Mean-over-Frames(MoF) compared to the state-of-the-art on one egocentric dataset. We conducted a real-world case study on nursing simulations, demonstrating SmartSeg’s ability to effectively segment complex, noisy interactions with diverse activity transitions. The results highlight SmartSeg’s robustness in handling long, unstructured, and visually challenging wearable camera videos, establishing it as a promising tool for real-world video temporal segmentation tasks.

Emergency response services are vital for enhancing public safety by safeguarding the environment, property, and human lives. As frontline members of these services, 9-1-1 dispatchers have a direct impact on response times and the overall effectiveness of emergency operations. However, traditional dispatcher training methods, which rely on role-playing by experienced personnel, are labor-intensive, time-consuming, and often neglect the specific needs of underserved communities. To address these challenges, we introduce Sim911, the first training simulation for 9-1-1 dispatchers powered by Large Language Models (LLMs). Sim911 enhances training through three key technical innovations: (1) knowledge construction, which utilizes archived 9-1-1 call data to generate simulations that closely mirror real-world scenarios; (2) context-aware controlled generation, which employs dynamic prompts and vector bases to ensure that LLM behavior aligns with training objectives; and (3) validation with looped correction, which filters out low-quality responses and refines the system performance. Experimental results show Sim911's superior performance in effectiveness and equity. Beyond its technical advancements, Sim911 delivers significant social impacts. Successfully deployed in the Metro X of Emergency Communications (MXDEC)(PS: To ensure a double-blind review, we refer to the city as 'City X,' a mid-sized U.S. city with a population of over 700,000. Its Metro Department of Emergency Communications (MXDEC) employs around 80 dispatchers and call-takers. For the rest of the paper, we refer to MXDEC as 'DEC.') Sim911 has been integrated into multiple training sessions, saving time for dispatchers. By supporting a diverse range of incident types and caller tags, Sim911 provides more realistic and inclusive training experiences. In a conducted user study, 90.00 percent of participants found Sim911 to be as effective or even superior to traditional human-led training, making it a valuable tool for emergency communications centers nationwide, particularly those facing staffing challenges.

There is a growing trend toward AI systems interacting with humans to revolutionize a range of application domains such as healthcare and transportation. However, unsafe human-machine interaction can lead to catastrophic failures. We propose a novel approach that predicts future states by accounting for the uncertainty of human interaction, monitors whether predictions satisfy or violate safety requirements, and adapts control actions based on the predictive monitoring results. Specifically, we develop a new quantitative predictive monitor based on Signal Temporal Logic with Uncertainty (STL-U) to compute a robustness degree interval, which indicates the extent to which a sequence of uncertain predictions satisfies or violates an STL-U requirement. We also develop a new loss function to guide the uncertainty calibration of Bayesian deep learning and a new adaptive control method, both of which leverage STL-U quantitative predictive monitoring results. We apply the proposed approach to two case studies: Type 1 Diabetes management and semi-autonomous driving. Experiments show that the proposed approach improves safety and effectiveness in both case studies.

Ensuring the online safety of youth has motivated research towards the development of machine learning (ML) methods capable of accurately detecting social media risks after-the-fact. However, for these detection models to be effective, they must proactively identify high-risk scenarios (e.g., sexual solicitations, cyberbullying) to mitigate harm. This `real-time' responsiveness is a recognized challenge within the risk detection literature. Therefore, this paper presents a novel two-level framework that first uses reinforcement learning to identify conversation stop points to prioritize messages for evaluation. Then, we optimize state-of-the-art deep learning models to accurately categorize risk priority (low, high). We apply this framework to a time-based simulation using a rich dataset of 23K private conversations with over 7 million messages donated by 194 youth (ages 13-21). We conducted an experiment comparing our new approach to a traditional conversation-level baseline. We found that the timeliness of conversations significantly improved from over 2 hours to approximately 16 minutes with only a slight reduction in accuracy (0.88 to 0.84). This study advances real-time detection approaches for social media data and provides a benchmark for future training reinforcement learning that prioritizes the timeliness of classifying high-risk conversations.

Emergency response services are critical to public safety, with 9-1-1 call-takers playing a key role in ensuring timely and effective emergency operations. To ensure call-taking performance consistency, quality assurance is implemented to evaluate and refine call-takers' skillsets. However, traditional human-led evaluations struggle with high call volumes, leading to low coverage and delayed assessments. We introduce LogiDebrief, an AI-driven framework that automates traditional 9-1-1 call debriefing by integrating Signal-Temporal Logic (STL) with Large Language Models (LLMs) for fully-covered rigorous performance evaluation. LogiDebrief formalizes call-taking requirements as logical specifications, enabling systematic assessment of 9-1-1 calls against procedural guidelines. It employs a three-step verification process: (1) contextual understanding to identify responder types, incident classifications, and critical conditions; (2) STL-based runtime checking with LLM integration to ensure compliance; and (3) automated aggregation of results into quality assurance reports. Beyond its technical contributions, LogiDebrief has demonstrated real-world impact. Successfully deployed at Metro Nashville Department of Emergency Communications, it has assisted in debriefing 1,701 real-world calls, saving 311.85 hours of active engagement. Empirical evaluation with real-world data confirms its accuracy, while a case study and extensive user study highlight its effectiveness in enhancing call-taking performance.

Reward design is a key component of deep reinforcement learning (DRL), yet some tasks and designer’s objectives may be unnatural to define as a scalar cost function. Among the various techniques, formal methods integrated with DRL have garnered considerable attention due to their expressiveness and flexibility in defining the reward and requirements for different states and actions of the agent. Nevertheless, the exploration of leveraging Signal Temporal Logic (STL) for guiding multi-agent reinforcement learning (MARL) reward design is still limited. The presence of complex interactions, heterogeneous goals, and critical safety requirements in multi-agent systems exacerbates this challenge. In this paper, we propose a novel STL-guided multi-agent reinforcement learning framework. The STL requirements are designed to include both task specifications according to the objective of each agent and safety specifications. The robustness values from checking the states against STL specifications are leveraged to generate rewards. We validate our approach by conducting experiments across various testbeds. The experimental results demonstrate significant performance improvements compared to MARL without STL guidance, along with a remarkable increase in the overall safety rate of the multi-agent systems.

Semantic segmentation neural networks (SSNs) are increasingly essential in high-stakes fields such as medical imaging, autonomous driving, and environmental monitoring, where robustness to input uncertainties and adversarial examples is crucial for ensuring safety and reliability. However, traditional probabilistic verification methods struggle to scale effectively with the size and depth of modern SSNs, especially when dealing with their high-dimensional, structured inputs/outputs. As the output dimension increases, these methods tend to become overly conservative, resulting in unnecessarily restrictive safety guarantees. In this work, we propose a probabilistic, data-driven verification algorithm that is architecture-agnostic and scalable, capable of handling the high-dimensional outputs of SSNs without introducing conservative and loose guarantees. We leverage efficient sampling-based reachability analysis to explore the space of possible outputs while maintaining computational feasibility. Our methodology is based on Conformal Inference (CI), which is known for its high data efficiency. However, CI tends to be overly conservative in high-dimensional spaces. To address this, in this paper, we introduce techniques to mitigate these sources of conservatism, enabling us to provide less conservative yet provable guarantees for SSNs. We validate our approach on large segmentation models applied to CamVid, OCTA-500 and Lung\_Segmentation, and Cityscapes datasets, showing that it can offer reliable safety guarantees while lowering the conservatism inherent in traditional methods. We also provide a public GitHub repository for this approach, to support reproducibility.

Smart cities operate on computational predictive frameworks that collect aggregate and utilize data from large-scale sensor networks. However these frameworks are prone to multiple sources of data and algorithmic bias which often lead to unfair prediction results. In this work we first demonstrate that bias persists at a micro-level both temporally and spatially by studying real city data from Chattanooga TN. To alleviate the issue of such bias we introduce FairGuard a micro-level temporal logic-based approach for fair smart city policy adjustment and generation in complex temporal-spatial domains. The FairGuard framework consists of two phases. First we develop a static generator that is able to reduce data bias based on temporal logic conditions by minimizing correlations between selected attributes. Second to ensure fairness in predictive algorithms we design a dynamic component to regulate prediction results and generate future fair predictions by harnessing logic rules. To navigate potential conflicts among these single fairness rules including logical contradictions and data interference we formulate detection strategies grounded in Satisfiability Modulo Theories (SMT) across both logic and data levels. Furthermore acknowledging the limitations of fairness rules focused on a single attribute we enhance the Static FairGuard to accommodate heterogeneous fairness rules that simultaneously consider multiple protected attributes. In addition we develop an interactive online visualizer that displays the adjustments made to correct unfair city states thereby improving fairness alongside the prediction outcomes from the dynamic component. Evaluations showcase that logic-enabled Static FairGuard can effectively reduce the biased correlations while Dynamic FairGuard can guarantee fairness on protected groups at runtime with minimal impact on overall performance.

This paper proposes the utilization of a multi-mode ACC based on interpretable Finite State Machine (FSM) to address challenges in infrastructure and surrounding condition changes while meeting macroscopic safety and comfort requirements in traffic flow. Specifically, the paper designs and simulates a merge yield control mode, a dynamic speed change mode, and a safety and monitoring mode switching under defined state transitions with the traditional car-following mode. Advanced ACC algorithms have been applied to improve traffic efficiency and have demonstrated energy savings. Yet they have typically been deployed in a single-use case: car-following mode. In this mode, where the Autonomous Vehicle (AV) maintains an appropriate distance or time gap with the preceding vehicle, decelerating when the gap is small and accelerating when it is large, the system may struggle to guarantee safety and comfort in complex and variable driving scenarios. Although there exist mode-switching ACC and merge mode controllers, in which even involving latitude direction control have been proposed, their dynamics when driving alongside other controlled or human-driving vehicles under a Connected and Autonomous Vehicles (CAVs) traffic environment remains unclear. The paper includes results from an implementation that was successfully tested on the open road, and simulation results that show dampened disturbances from the mode-switching approach, compared to single-mode use of an ACC controller in the same scenarios.

Recent advancements in federated learning (FL) have greatly facilitated the development of decentralized collaborative applications, particularly in the domain of Artificial Intelligence of Things (AIoT). However, a critical aspect missing from the current research landscape is the ability to enable data-driven client models with symbolic reasoning capabilities. Specifically, the inherent heterogeneity of participating client devices poses a significant challenge, as each client exhibits unique logic reasoning properties. Failing to consider these device-specific specifications can result in critical properties being missed in the client predictions, leading to suboptimal performance. In this work, we propose a new training paradigm that leverages temporal logic reasoning to address this issue. Our approach involves enhancing the training process by incorporating mechanically generated logic expressions for each FL client. Additionally, we introduce the concept of aggregation clusters and develop a partitioning algorithm to effectively group clients based on the alignment of their temporal reasoning properties. We evaluate the proposed method on two tasks: a real-world traffic volume prediction task consisting of sensory data from fifteen states and a smart city multi-task prediction utilizing synthetic data. The evaluation results exhibit clear improvements, with performance accuracy improved by up to 54% across all sequential prediction models.

Emergency and non-emergency response systems are essential services provided by local governments and critical to protecting lives, the environment, and property. The effective handling of (non-)emergency calls is critical for public safety and well-being. By reducing the burden through non-emergency callers, residents in critical need of assistance through 911 will receive a fast and effective response. Collaborating with the Department of Emergency Communications (DEC) in Nashville, we analyzed 11,796 non-emergency call recordings and developed Auto311, the first automated system to handle 311 non-emergency calls, which (1) effectively and dynamically predicts ongoing non-emergency incident types to generate tailored case reports during the call; (2) itemizes essential information from dialogue contexts to complete the generated reports; and (3) strategically structures system-caller dialogues with optimized confidence. We used real-world data to evaluate the system's effectiveness and deployability. The experimental results indicate that the system effectively predicts incident type with an average F-1 score of 92.54%. Moreover, the system successfully itemizes critical information from relevant contexts to complete reports, evincing a 0.93 average consistency score compared to the ground truth. Additionally, emulations demonstrate that the system effectively decreases conversation turns as the utterance size gets more extensive and categorizes the ongoing call with 94.49% mean accuracy.

Monte Carlo tree search (MCTS) is one of the most capable online search algorithms for sequential planning tasks, with significant applications in areas such as resource allocation and transit planning. Despite its strong performance in real-world deployment, the inherent complexity of MCTS makes it challenging to understand for users without technical background. This paper considers the use of MCTS in transportation routing services, where the algorithm is integrated to develop optimized route plans. These plans are required to meet a range of constraints and requirements simultaneously, further complicating the task of explaining the algorithm’s operation in real-world contexts. To address this critical research gap, we introduce a novel computation tree logic-based explainer for MCTS. Our framework begins by taking user-defined requirements and translating them into rigorous logic specifications through the use of language templates. Then, our explainer incorporates a logic verification and quantitative evaluation module that validates the states and actions traversed by the MCTS algorithm. The outcomes of this analysis are then rendered into human-readable descriptive text using a second set of language templates. The user satisfaction of our approach was assessed through a survey with 82 participants. The results indicated that our explanatory approach significantly outperforms other baselines in user preference.

An increasing number of monitoring systems have been developed in smart cities to ensure that a city's real-time operations satisfy safety and performance requirements. However, many existing city requirements are written in English with missing, inaccurate, or ambiguous information. There is a high demand for assisting city policy makers in converting human-specified requirements to machine-understandable formal specifications for monitoring systems. To tackle this limitation, we build CitySpec, the first intelligent assistant system for requirement specification in smart cities. To create CitySpec, we first collect over 1,500 real-world city requirements across different domains from over 100 cities and extract city-specific knowledge to generate a dataset of city vocabulary with 3,061 words. We also build a translation model and enhance it through requirement synthesis and develop a novel online learning framework with validation under uncertainty. The evaluation results on real-world city requirements show that CitySpec increases the sentence-level accuracy of requirement specification from 59.02 % to 86.64 %, and has strong adaptability to a new city and a new domain (e.g., F1 score for requirements in Seattle increases from 77.6 % to 93.75% with online learning).

As more and more monitoring systems have been deployed to smart cities, there comes a higher demand for converting new human-specified requirements to machine-understandable formal specifications automatically. However, these human-specific requirements are often written in English and bring missing, inaccurate, or ambiguous information. In this paper, we present City Spec [1], an intelligent assistant system for requirement specification in smart cities. CitySpec not only helps overcome the language differences brought by English requirements and formal specifications, but also offers solutions to those missing, inaccurate, or ambiguous information. The goal of this paper is to demonstrate how CitySpec works. Specifically, we present three demos: (1) interactive completion of requirements in CitySpec; (2) human-in-the-loop correction while CitySepc encounters exceptions; (3) online learning in CitySpec.

As various smart services are increasingly deployed in modern cities, many unexpected conflicts arise due to various physical world couplings. Existing solutions for conflict resolution often rely on centralized control to enforce predetermined and fixed priorities of different services, which is challenging due to the inconsistent and private objectives of the services. Also, the centralized solutions miss opportunities to more effectively resolve conflicts according to their spatiotemporal locality of the conflicts. To address this issue, we design a decentralized negotiation and conflict resolution framework named DeResolver, which allows services to resolve conflicts by communicating and negotiating with each other to reach a Pareto-optimal agreement autonomously and efficiently. Our design features a two-step self-supervised learning-based algorithm to predict acceptable proposals and their rankings of each opponent through the negotiation. Our design is evaluated with a smart city case study of three services: intelligent traffic light control, pedestrian service, and environmental control. In this case study, a data-driven evaluation is conducted using a large dataset consisting of the GPS locations of 246 surveillance cameras and an automatic traffic monitoring system with more than 3 million records per day to extract real-world vehicle routes. The evaluation results show that our solution achieves much more balanced results, i.e., only increasing the average waiting time of vehicles, the measurement metric of intelligent traffic light control service, by 6.8% while reducing the weighted sum of air pollutant emission, measured for environment control service, by 12.1%, and the pedestrian waiting time, the measurement metric of pedestrian service, by 33.1%, compared to priority-based solution.

With the development of the Internet of Things, millions of sensors are being deployed in cities to collect real-time data. This leads to a need for checking city states against city requirements at runtime. In this article, we develop a novel spatial-temporal specification-based monitoring system for smart cities. We first describe a study of over 1000 smart city requirements, some of which cannot be specified using the existing logic, such as the signal temporal logic (STL) and its variants. To tackle this limitation, we develop spatial aggregation STL (SaSTL)-a novel spatial aggregation STL-for the efficient runtime monitoring of safety and performance requirements in smart cities. We develop two new logical operators in SaSTL to augment STL for expressing spatial aggregation and spatial counting characteristics that are commonly found in real city requirements. We define the Boolean and quantitative semantics for SaSTL in support of the analysis of city performance across different periods and locations. We also develop efficient monitoring algorithms that can check the SaSTL requirement in parallel over multiple data streams (e.g., generated by multiple sensors distributed spatially in a city). Additionally, we build an SaSTL-based monitoring tool to support decision making of different stakeholders to specify and runtime monitor their requirements in smart cities. We evaluate our SaSTL monitor by applying it to three case studies with large-scale real city sensing data (e.g., up to 10 000 sensors in one study). The results show that SaSTL has a much higher coverage expressiveness than other spatial-temporal logics, and with a significant reduction of computation time for monitoring requirements. We also demonstrate that the SaSTL monitor improves the safety and performance of smart cities via simulated experiments.

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.

Recurrent Neural Networks (RNNs) have made great achievements for sequential prediction tasks. In practice, the target sequence often follows certain model properties or patterns (e.g., reasonable ranges, consecutive changes, resource constraint, temporal correlations between multiple variables, existence, unusual cases, etc.). However, RNNs cannot guarantee their learned distributions satisfy these model properties. It is even more challenging for predicting large-scale and complex Cyber-Physical Systems. Failure to produce outcomes that meet these model properties will result in inaccurate and even meaningless results. In this paper, we develop a new temporal logic-based learning framework, STLnet, which guides the RNN learning process with auxiliary knowledge of model properties, and produces a more robust model for improved future predictions. Our framework can be applied to general sequential deep learning models, and trained in an end-to-end manner with back-propagation. We evaluate the performance of STLnet using large-scale real-world city data. The experimental results show STLnet not only improves the accuracy of predictions, but importantly also guarantees the satisfaction of model properties and increases the robustness of RNNs.

Input is a significant problem for wearable devices, particularly for head-mounted virtual and augmented reality systems. Contemporary AR/VR systems use in-air gestures or handheld controllers for interactivity. However, mid-air handwriting provides a natural, subtle, and easy-to-use way to input commands and text. In this demo, we propose and investigate ViFin, a new technique for input commands and text entry which tracks continuous micro finger-level writing with a commodity smartwatch through vibrations. Inspired by the recurrent neural aligner and transfer learning, ViFin recognizes continuous finger writing and works across different users and achieves an accuracy of 90% and 91% for recognizing numbers and letters, respectively. Finally, a real-time writing system with two specific applications using AR smartglasses are implemented.

Family caregivers often report increased anxiety and depression. In order to improve the interactions between in-home patients and caregivers, and reduce strain on caregivers, we build a monitoring, modeling, and interactive recommendation system for caregivers for in-home dementia patient care. The system includes monitoring for mood by speech, building classifiers that work in realistic home settings, and supporting an adaptive recommendation system to reduce stress of the caregiver. This demo shows how our system supports caregivers in practice through several scenarios.

In order to prevent safety violations, predictive monitoring with uncertainty is crucial for deep learning-enabled services in smart cities. We develop a novel predictive monitoring system for smart city applications, which consists of an RNN-based predictor with uncertainty estimation and a new specification language, named Signal Temporal Logic with Uncertainty. The solution first predicts a sequence of distributions representing city's future states with uncertainty estimation and then checks the predicted results against STL-U specified safety and performance requirements. The system supports decision making by providing a quantitative satisfaction degree with confidence guarantees. We receive promising results from evaluations on two large-scale city datasets, and on a case study on real-time predictive monitoring in a simulated smart city.

Cities are deploying tens of thousands of sensors and actuators and developing a large array of smart services. The smart services use sophisticated models and decision-making policies supported by Cyber Physical Systems and Internet of Things technologies. The increasing number of sensors collects a large amount of city data across multiple domains. The collected data have great potential value, but has not yet been fully exploited. This survey focuses on the domains of transportation, environment, emergency and public safety, energy, and social sensing. This article carefully reviews both the data sets being collected across 14 smart cities and the state-of-the-art work in modeling and decision making methodologies. The article also points out the characteristics, challenges faced today, and those challenges that will be exacerbated in the future. Key data issues addressed include heterogeneity, interdisciplinary, integrity, completeness, real-timeliness, and interdependencies. Key decision making issues include safety and service conflicts, security, uncertainty, humans in the loop, and privacy.

Textual health advice generated from different online sources (e.g., health apps and websites) can be conflicting. Conflicts can occur due to lexical features, (such as, negation, antonyms, or numerical mismatch) or can be conditioned upon time and/or physiological status. Detecting conflicts from textual health advice poses several challenges, including, large structural variation between text and hypothesis pairs, finding conceptual overlap between pairs of advice, and inference of the semantics of an advice (i.e., what to do, why, and how). In this demonstration, we present a semantic rule-based system to detect different types of conflicts in online textual health advice statements in a context-aware and interpretable manner.

Research in the area of internet-of-things, cyberphysical-systems, and smart health often employ sensor systems at residences for continuous monitoring. Such research-oriented residential monitoring systems (RRMSs) usually face two major challenges, long-term reliable operation management and validation of system functionality with minimal human effort. Targeting these two challenges, this paper describes a monitor of monitoring systems with ground-truth validation capabilities, M2G. It consists of two subsystems, the Monitor2system and the Ground-truth validation system. The Monitor2system encapsulates a flexible set of general-purpose components to monitor the operation and connectivity of heterogeneous sensor devices (e.g. smart watches, smart phones, microphones, beacons, etc.), a local base-station, as well as a cloud server. It provides a user-friendly interface and supports different types of RRMSs in various contexts. The system also features a ground truth validation system to support obtaining ground truth in the field. Additionally, customized alerts can be sent to remote administrators and other personnel to report any dysfunction or inaccuracy of the system in real time. M2G is applied to three very different case studies: the M2FED system which monitors family eating dynamics [1], an in-home wireless sensing system for monitoring nighttime agitation [2], and the BESI system which monitors behavioral and environmental parameters to predict health events and to provide interventions [3]. The results indicate that M2G is a comprehensive system that (i) requires small cost in time and effort to adapt to an existing RRMS, (ii) provides reliable data collection and reduction in data loss by detecting faults in real-time, and (iii) provides a convenient and timely ground truth validation facility.

With the rapid digitalization of the health sector, people often turn to mobile apps and online health websites for health advice. Health advice generated from different sources can be conflicting as they address different aspects of health (e.g., weight loss, diet, disease) or as they are unaware of the context of a user (e.g., age, gender, physiological condition). Conflicts can occur due to lexical features, (such as, negation, antonyms, or numerical mismatch) or can be conditioned upon time and/or physiological status. We formulate the problem of finding conflicting health advice and develop a comprehensive taxonomy of conflicts. While a similar research area in the natural language processing domain explores the problem of textual contradiction identification, finding conflicts in health advice poses its own unique lexical and semantic challenges. These include large structural variation between text and hypothesis pairs, finding conceptual overlap between pairs of advice, and inference of the semantics of an advice (i.e., what to do, why and how). Hence, we develop Preclude, a novel semantic rule-based solution to detect conflicting health advice derived from heterogeneous sources utilizing linguistic rules and external knowledge bases. As our solution is interpretable and comprehensive, it can guide users towards conflict resolution too. We evaluate Preclude using 1156 real advice statements covering 8 important health topics that are collected from smart phone health apps and popular health websites. Preclude results in 90% accuracy and outperforms the accuracy and F1 score of the baseline approach by about 1.5 times and 3 times, respectively.

The populations of large cities around the world are growing rapidly. Cities are beginning to address this problem by implementing significant sensing and actuation infrastructure and building services on this infrastructure. However, as the density of sensing and actuation increases and as the complexities of services grow there is an increasing potential for conflicts across Smart City services. These conflicts can cause unsafe situations and disrupt the benefits that the services were originally intended to provide. Although some of the conflicts can be detected and avoided during designing the services, many can still occur unpredictably during runtime. This paper carefully defines and enumerates the main issues regarding the detection and resolution of runtime conflicts in smart cities. In particular, it focuses on conflicts that arise across services. This issue is becoming more and more important as Smart City designs attempt to integrate services from different domains (transportation, energy, public safety, emergency, medical, and many others). Research challenges are identified and then addressed that deal with uncertainty, dynamism, real-time, mobility and spatio-temporal availability, duration and scale of effect, efficiency, and ownership. A watchdog architecture is also described that oversees the services operating in a Smart City. This watchdog solution detects and resolves conflicts, it learns and adapts, and it provides additional inputs to decision making aspects of services. Using data from a Smart City dataset, an emulated set of services and activities using those services are created to perform a conflict analysis. A second analysis hypothesizes 41 future services across 5 domains. Both of these evaluations demonstrate the high probability of conflicts in smart cities of the future.

Nature has always been a muse for those who dream in art or science. As it goes, optimization algorithms inspired by nature have been widely used to solve various scientific and engineering problems because of their intelligence and simplicity. As a novel nature‐inspired algorithm, the crystal energy optimizer (CEO) is proposed in this article. The proposed CEO is motivated by the following general observation on lake freezing in nature: the dynamics of crystals have possession of parallelism, openness, local interactivity, and self‐organization. It stimulates us to extend a crystal dynamic model in physics to a generalized crystal energy optimizer for traveling salesman problems, so as to exploit the advantages of crystal dynamic system and to realize the aforementioned purposes. The proposed CEO has these advantages: (1) it has the ability to perform large‐scale distributed parallel optimization; (2) it can converge and avoid local optimum; and (3) it is flexible and easy to adapt to a wide range of optimization problems.