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.

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.

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.

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.