Ensuring fairness is essential for ethical decision-making in various domains. Informally, a neural network is considered fair if it treats similar individuals similarly in a given task. We introduce FaVeR (Fairness Verification and Repair), a framework for efficiently verifying and repairing pre-trained neural networks with respect to individual fairness properties. FaVeR ensures fairness via iterative search of high-sensitivity neurons and backward adjustment of their weights, guided by counterexamples generated from fairness verification using satisfiability modulo convex programming. By addressing fairness at the neuronal level, FaVeR aims to minimize the impact of neural network repair on overall performance. Empirical evaluations on common fairness datasets show that FaVeR achieves a 100% fairness repair rate across all models with an accuracy reduction of less than 2.27% and significantly lower average runtime than alternative repair methods. © 2025 International Joint Conferences on Artificial Intelligence. All rights reserved.

Many decision-making scenarios in engineering, sociology, and epidemiology, among other fields, can be effectively modeled by a large population of learning agents, captured by an evolutionary dynamics model (EDM), which can possibly act non-cooperatively and interact with an exogenous dynamical system (ES). In these systems, the agents' collective behavior can drive the ES into undesirable states and significantly compromise its stability and safety. In this paper, we propose a method using control barrier functions to design payoffs that can guide the population's strategy selection while ensuring safe and stable behavior of the ES. We first address the need to avoid undesirable population states in the EDM. We then extend our approach to coupled EDM-ES systems, where the designed payoffs can prevent undesirable states and guarantee convergence to a target state. Finally, we establish general conditions under which the designed payoffs remain effective across different classes of EDMs, ensuring broad applicability. Numerical simulations validate our approach in both standalone EDMs and coupled EDM-ES systems that satisfy the proposed conditions. © 2025 IEEE.

Constrained Markov decision process (CMDP) models are increasingly important in many applications with multiple objectives. When the model is unknown and must be learned online, it is desirable to ensure that the constraint is met, or at least the violation is bounded with time. In the recent literature, progress has been made on this very challenging problem, but with either unsatisfactory assumptions, such as the knowledge of a safe policy, or high cumulative regret. We propose the Safe-PSRL (posterior sampling-based RL) algorithm that does not need such assumptions and yet performs very well, both in terms of theoretical regret bounds as well as empirically. The algorithm efficiently trades-off exploration and exploitation using posterior sampling-based exploration, and yet provably suffers only bounded constraint violation using carefully-crafted pessimism. We establish a sub-linear Õ (H2.5√|S|2|A|K) upper bound on the Bayesian objective regret along with a bounded, i.e., Õ (1) constraint-violation regret over K episodes for an |S|-state, |A|action, and horizon H CMDP, which improves over state-of-the-art algorithms for the same setting. Copyright 2025 by the author(s).

Graph neural networks (GNNs) have displayed significant potential in various graph-based learning tasks. However, the computational demands of deploying GNNs on large-scale graphs can grow exponentially. A recent method, termed unified graph sparsification (UGS), shows that there exists a pair consisting of a subgraph and a sparse subnetwork, called graph lottery ticket (GLT), that can effectively speed up GNN inference. However, despite their advantages, the performance of GLTs against adversarial structure perturbations remains largely unexplored. In this paper, we investigate the resilience of GLTs against different structure perturbation attacks under the poisoning attack setting. The evaluation results show that the GLTs identified by UGS are vulnerable and exhibit a large drop in classification accuracy for the adversarially perturbed graphs. We then propose a new technique for defending UGS that leverages self-training to find GLTs that are more resilient and can achieve better performance than plain UGS. © 2024 IEEE.

Next-generation certification processes are expected to be influenced by two dominant trends: customizable certification, as advocated by Overarching Properties (OPs), and the continuous and rapid delivery approach from the coupling of software development and operations (DevOps). In light of these trends, certification processes must adapt to support the ongoing evaluation of assurance while accommodating the emergence of new evidence and evolving safety and security practices, particularly for systems enabled by artificial intelligence (AI). These requirements call for the development of computer-aided evaluation tools that automate repetitive tasks and offer visualization aids to assist evaluators and applicants in making informed decisions. This paper aims to address the challenges associated with assurance evaluation via a survey-based analysis and proposes a user interface that streamlines the evaluation of certification arguments. © 2023 IEEE.

We address the Warehouse Servicing Problem (WSP) in automated warehouses, which use teams of mobile robots to move products from shelves to packaging stations. Given a list of products, the WSP amounts to finding a motion plan which brings every product on the list from a shelf to a packaging station within a given time limit. The WSP consists of four subproblems, namely, deciding where to source and deposit a product (task formulation), who should transport each product (task assignment) and when (scheduling) and how (motion planning). These problems are NP-Hard individually and made more challenging by their interdependence. The difficulty of the WSP is compounded by the scale of automated warehouses, which use teams of hundreds of agents to transport thousands of products. In this paper, we present Contract-based Cyclic Motion Planning (CCMP), a novel contract-based methodology for solving the WSP at scale. CCMP decomposes a warehouse into a set of traffic system components. By assigning each component a contract which describes the traffic flows it can support, CCMP can generate a traffic flow which satisfies a given WSP instance. CCMP then uses a novel motion planner to transform this traffic flow into a motion plan for a team of robots. Evaluation shows that CCMP can solve WSP instances taken from real industrial scenarios with up to 1 million products while outperforming other methodologies for solving the WSP by up to 2.9×. © 2023 IEEE.

We address the problem of modeling, refining, and repairing formal specifications for robotic missions using assume-guarantee contracts. We show how to model mission specifications at various levels of abstraction and implement them using a library of pre-implemented specifications. Suppose the specification cannot be met using components from the library. In that case, we compute a proxy for the best approximation to the specification that can be generated using elements from the library. Afterward, we propose a systematic way to either 1) search for and refine the 'missing part' of the specification that the library cannot meet or 2) repair the current specification such that the existing library can refine it. Our methodology for searching and repairing mission requirements leverages the quotient, separation, composition, and merging operations between contracts. © 2023 IEEE.

We address the warehouse servicing problem (WSP) in automated warehouses, which use teams of mobile agents to bring products from shelves to packing stations. Given a list of products, the WSP amounts to finding a plan for a team of agents which brings every product on the list to a station within a given timeframe. The WSP consists of four subproblems, concerning what tasks to perform (task formulation), who will perform them (task allocation), and when (scheduling) and how (path planning) to perform them. These subproblems are NP-hard individually and are made more challenging by their interdependence. The difficulty of the WSP is compounded by the scale of automated warehouses, which frequently use teams of hundreds of agents. In this paper, we present a methodology that can solve the WSP at such scales. We introduce a novel, contract-based design framework which decomposes an automated warehouse into traffic system components. By assigning each of these components a contract describing the traffic flows it can support, we can syn-thesize a traffic flow satisfying a given WSP instance. Component-wise search-based path planning is then used to transform this traffic flow into a plan for discrete agents in a modular way. Evaluation shows that this methodology can solve WSP instances on real automated warehouses. © 2023 EDAA.

We present a compositional control synthesis method based on assume-guarantee contracts with application to correct-by-construction design of vehicular mission plans. In our approach, a mission-level specification expressed in a fragment of signal temporal logic (STL) is decomposed into formulas whose predicates are defined on non-overlapping time intervals. The STL formulas are then mapped to aggregations of contracts associated with continuously differentiable time-varying control barrier functions. The barrier functions are used to constrain the lower-level control synthesis problem, which is solved via quadratic programming. Our approach can mitigate the conservatism of previous methods for task-driven control based on under-approximations. We illustrate its effectiveness on a case study motivated by vehicular mission planning under safety constraints as well as constraints imposed by traffic regulations under vehicle-to-vehicle and vehicle-to-infrastructure communication. © 2022 IEEE.

We present ARACHNE, a framework for the automated, compositional validation of assurance cases (ACs), i.e., structured arguments about the correctness or safety of a design. ARACHNE leverages assume-guarantee contracts, expressed in a stochastic logic formalism, to formally capture AC claims (guarantees) subject to their contexts (assumptions) as well as the sources of uncertainty associated with them. Given an AC, modeled as a hierarchical network of stochastic contracts, and a library of confidence models, expressed as a set of Bayesian networks, we propose a procedure that coordinates logic and Bayesian reasoning to check that the AC argument is sound and quantify its strength in terms of a confidence measure. The effectiveness of our approach is illustrated on case studies motivated by testing and validation of airborne and automotive system software.