Recent work has pioneered the use of system-theoretic passivity to study equilibrium stability for the dynamics of noncooperative strategic interactions in large populations of learning agents. In this and related works, the stability analysis leverages knowledge that certain "canonical" classes of learning rules used to model the agents’ strategic behaviors satisfy a passivity condition known as δ-passivity. In this paper, we consider that agents exhibit learning behaviors that do not align with a canonical class. Specifically, we focus on characterizing δ-passivity for hybrid learning rules that combine elements from canonical classes. Our analysis also introduces and uses a more general version of δ-passivity, which, for the first time, can handle discontinuous learning rules, including those showing best response behaviors. We state and prove theorems establishing δ-passivity for two broad convex cones of hybrid learning rules. These cones can merge into a larger one preserving δ-passivity in scenarios limited to two strategies. In our proofs, we establish intermediate facts that are significant on their own and could potentially be used to further generalize our work. We illustrate the applicability of our results through numerical examples. © 2026 The Author(s)

The design of complex cyber-physical system architectures is often hierarchical. System specifications are mapped to an implementation layer via a stepwise refinement process involving multiple intermediate layers. These layers may capture different functionalities, and the orchestration of a variety of heterogeneous techniques suited to each layer may be required to achieve the overall design objectives. Due to their heterogeneity, ensuring traceability and verifiability of such architectures is a challenging problem. In this article, we present a correct-by-construction methodology for designing heterogeneous layered architectures. We capture the specifications at each layer with assume-guarantee contracts, a specification paradigm which can encompass a variety of modeling formalisms. We then use the notion of contract embeddings to define specification refinement, rigorously and traceably mapping specifications across layers modeled with heterogeneous formalisms. We instantiate our methodology on the design of layered control architectures (LCAs), resulting in a novel approach that can verifiably orchestrate domain-specific techniques to satisfy both global planning and local safety requirements. In the context of LCAs, we derive necessary conditions for correct specification refinement and results for compositional realization of control safety specifications. We illustrate our design methodology on a motivating example and a case study derived from robotic mission planning and control.

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).

The effectiveness of reachability analysis often depends on choosing appropriate values for a set of tool-specific properties which need to be manually tailored to the specific system involved and the reachable set to be evolved. Such property tuning is a time-consuming task, especially when dealing with nonlinear systems. In this paper, we propose, instead, a methodology to automatically and dynamically choose property values for reachability analysis along the system evolution, based on the actual verification objective, i.e., the verification or falsification of a set of constraints. By leveraging an initial solution to the reachable set, we estimate bounds on the numerical accuracy required from each integration step to provide a definite answer to the satisfaction of the constraints. Based on these accuracy bounds, we design a cost function which we use, after mapping the property space to an integer space, to search for locally optimal property values that yield the desired accuracy. Results from the application of our methodology to the nonlinear reachability analysis tool ARIADNE show that the frequency of correct answers to constraint satisfaction problems increases significantly with respect to a manual approach. © 2024 The Authors

Autonomous systems often have logical constraints arising, for example, from safety, operational, or regulatory requirements. Such constraints can be expressed using temporal logic specifications. The system state is often partially observable. Moreover, it could encompass a team of multiple agents with a common objective but disparate information structures and constraints. In this paper, we first introduce an optimal control theory for partially observable Markov decision processes (POMDPs) with finite linear temporal logic ($\boldsymbol{LTL}_{\bf f}$) constraints. We provide a structured methodology for synthesizing policies that maximize a cumulative reward while ensuring that the probability of satisfying a temporal logic constraint is sufficiently high. Our approach comes with guarantees on approximate reward optimality and constraint satisfaction. We then build on this approach to design an optimal control framework for logically constrained multi-agent settings with information asymmetry. We illustrate the effectiveness of our approach by implementing it on several case studies. IEEE

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.

The design of complex mission-critical systems often follows a layered approach, which may lead to complicated, multi-level, multi-viewpoint requirement hierarchies. This heterogeneity makes it challenging to guarantee the traceability of the requirements across levels of abstraction and, consequently, the satisfaction of the requirements by a system implementation, especially when requirements at different abstraction levels are expressed using different mathematical formalisms and modeling languages. In this paper, we address this challenge by introducing heterogeneous hierarchical contract networks (HHCNs), a formal model based on a graph of assume-guarantee contracts, for capturing and analyzing heterogeneous requirement hierarchies. We formulate the requirement traceability validation problem in terms of contract refinement relations between nodes in an HHCN. We then define contract embeddings to enable reasoning about refinements across levels of abstraction in the HHCN that are expressed using heterogeneous formalisms. Contract embeddings leverage the notion of conservative approximation to rigorously map contracts across levels of abstraction while ensuring that refinement is preserved independently of the formalism to which the contracts are mapped. We illustrate their effectiveness on a case study motivated by a multi-agent autonomous lunar rover mission. © 1982-2012 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.