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.

Exploring system architectures that must satisfy a set of heterogeneous requirements while minimizing a cost metric is a computationally challenging task, due to the exponential growth of the design space with the number of architecture parameters and the interdependencies between architecture choices and system properties. We present a compositional architecture exploration methodology that encodes these interdependencies as assume-guarantee contracts expressed by satisfiability modulo convex programming (SMC) formulas. Inspired by the SMC paradigm, our approach coordinates integer programming for architecture selection with convex programming for requirement verification. It then introduces a two-level pruning scheme that leverages irreducible infeasible sets of convex constraints and verification counterexamples to generate infeasibility certificates that can effectively eliminate infeasible design configurations from the search space. Evaluations on representative benchmarks, including aircraft power distribution networks and reconfigurable production lines, show an order-of-magnitude speedup on large problem instances and the solution of problems on which prior methods time out, enabling tractable and scalable compositional design of complex system architectures.

Auto-formalization (AF) translates natural-language reasoning problems into solver-executable programs, enabling symbolic solvers to perform sound logical deduction. In practice, however, AF pipelines are currently brittle: programs may fail to execute, or execute but encode incorrect semantics. While prior work largely mitigates syntactic failures via repairs based on solver feedback, reducing semantics failures remains a major bottleneck. We propose Draft-and-Prune (D P), an inference-time framework that improves AF-based logical reasoning via diversity and verification. D P first drafts multiple natural-language plans and conditions program generation on them. It further prunes executable but contradictory or ambiguous formalizations, and aggregates predictions from surviving paths via majority voting. Across four representative benchmarks (AR-LSAT, ProofWriter, PrOntoQA, LogicalDeduction), D P substantially strengthens AF-based reasoning without extra supervision. On AR-LSAT, in the AF-only setting, D P achieves 78.43

Over the past decade, neural network (NN)-based controllers have demonstrated remarkable efficacy in a variety of decision-making tasks. However, their black-box nature and the risk of unexpected behaviors pose a challenge to their deployment in real-world systems requiring strong guarantees of correctness and safety. We address these limitations by investigating the transformation of NN-based controllers into equivalent soft decision tree (SDT)-based controllers and its impact on verifiability. In contrast to existing work, we focus on discrete-output NN controllers including rectified linear unit (ReLU) activation functions as well as argmax operations. We then devise an exact yet efficient transformation algorithm which automatically prunes redundant branches. We evaluate our approach and demonstrate the practical efficacy of the transformation algorithm using three benchmarks from the OpenAI Gym environment, including an autonomous driving NN controller. Our results indicate that the SDT transformation can benefit formal verification, showing runtime improvements of up to $20\times$, $2\times$, and $20\times$ for the MountainCar-v0, CartPole-v1, and CarRacing-v2 environments, respectively.

Advanced Air Mobility (AAM) operations are expected to significantly increase aerial traffic in urban airspace, requiring autonomous traffic management systems to ensure collision-free operations in highly congested environments. In this paper, we propose a multi-agent coordination framework that uses minimum time-to-reach (TTR) as a unifying metric for priority assignment, temporal separation, and safety filtering. We focus on the problem of coordinating multiple aerial vehicles merging into an air corridor while maintaining safe separation between vehicles. Vehicles are assigned arrival-consistent priority based on TTR, and target TTR values are used to enforce temporal spacing that induces spatial separation. A priority-consistent safety filtering layer based on Hamilton-Jacobi reachability value functions ensures collision avoidance while minimally modifying the reference guidance. Simulation results in a highly congested corridor merging scenario show that the proposed method improves safety, fairness, and efficiency compared to time-optimal guidance and priority-agnostic safety filtering.

Simulation-based design space exploration (DSE) aims to efficiently optimize high-dimensional structured designs under complex constraints and expensive evaluation costs. Existing approaches, including heuristic and multi-step reinforcement learning (RL) methods, struggle to balance sampling efficiency and constraint satisfaction due to sparse, delayed feedback, and large hybrid action spaces. In this paper, we introduce CORE, a constraint-aware, one-step RL method for simulationguided DSE. In CORE, the policy agent learns to sample design configurations by defining a structured distribution over them, incorporating dependencies via a scaling-graph-based decoder, and by reward shaping to penalize invalid designs based on the feedback obtained from simulation. CORE updates the policy using a surrogate objective that compares the rewards of designs within a sampled batch, without learning a value function. This critic-free formulation enables efficient learning by encouraging the selection of higher-reward designs. We instantiate CORE for hardware-mapping co-design of neural network accelerators, demonstrating that it significantly improves sample efficiency and achieves better accelerator configurations compared to state-of-the-art baselines. Our approach is general and applicable to a broad class of discrete-continuous constrained design problems.

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.

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 O-similar to (H-2.5 root vertical bar S-2 vertical bar A vertical bar K) upper bound on the Bayesian objective regret along with a bounded, i.e., O-similar to (1) constraint-violation regret over K episodes for an vertical bar S vertical bar -state, vertical bar A vertical bar action, and horizon H CMDP, which improves over state-of-the-art algorithms for the same setting.

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.

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

Ensuring fairness is essential for ethical decision-making in various domains. Informally, a neural network is considered fair if and only 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 neuron level, FaVeR minimizes the impact of neural network repair on the overall performance. Experimental evaluations on common fairness datasets show that FaVeR achieves a 100% fairness repair rate across all models, with accuracy reduction of less than 2.27%. Moreover, its significantly lower average runtime makes it suitable for practical applications.

We present a systematic approach for evaluating the quality of knowledge graph repairs with respect to constraint violations defined in shapes constraint language (SHACL). Current evaluation methods rely on ad hoc datasets, which limits the rigorous analysis of repair systems in more general settings. Our method addresses this gap by systematically generating violations using a novel mechanism, termed violation-inducing operations (VIOs). We use the proposed evaluation framework to assess a range of repair systems which we build using large language models. We analyze the performance of these systems across different prompting strategies. Results indicate that concise prompts containing both the relevant violated SHACL constraints and key contextual information from the knowledge graph yield the best performance.

We present a methodology for scalable exploration of cyber-physical system architectures.We propose a mathematical formulation of the architecture exploration problem as an optimized mapping problem that includes joint selection of system topologies and components taken from pre-defined libraries.Using a graph-based representation of an architecture, we introduce novel compact encodings of mapping constraints and path constraints that significantly improve the scalability of the formulation.We use the new encodings to instantiate design requirements, such as interconnection, routing, timing, and energy constraints, on the architecture model.We implement our methods in an extensible architecture exploration toolbox, and provide a pattern-based language for formal, yet flexible, requirement specification.Numerical evaluations on a set of design problems from wireless sensor networks, reconfigurable manufacturing systems, and electrical power systems demonstrate the effectiveness of our approach.

Designing control policies for large, distributed systems is challenging, especially in the context of critical, temporal logic based specifications (e.g., safety) that must be met with high probability. Compositional methods for such problems are needed for scalability, yet relying on worst-case assumptions for decomposition tends to be overly conservative. In this work, we use the framework of Constrained Markov Decision Processes (CMDPs) to provide an assume-guarantee based decomposition for synthesizing decentralized control policies, subject to logical constraints in a multi-agent setting. The returned policies are guaranteed to satisfy the constraints with high probability and provide a lower bound on the achieved objective reward. We empirically find the returned policies to achieve near-optimal rewards while enjoying an order of magnitude reduction in problem size and execution time.

We present ContrArc, a methodology for the exploration of cyber-physical system architectures aiming to minimize a cost function while adhering to a set of heterogeneous constraints. We assume a system topology, defined as a graph, where components (nodes) are selected from an implementation library, and connections between components (edges) are drawn from a finite set of possible connection choices. ContrArc uses assume-guarantee contracts to formalize different viewpoints in the system requirements, such as timing and power consumption, as well as the interface of different components, and translate the exploration problem into a mixed integer linear programming problem. It then searches for efficient solutions by relying on contract decompositions and a method based on sub graph isomorphism to iteratively prune infeasible architectures out of the search space. Experiments on a reconfigurable production line and an aircraft power distribution network show up to two orders of magnitude acceleration in architectural exploration with respect to comparable approaches.

In this paper, we introduce the constrained best mixed arm identification (CBMAI) problem with a fixed budget. This is a pure exploration problem in a stochastic finite armed bandit model. Each arm is associated with a reward and multiple types of costs from unknown distributions. Unlike the unconstrained best arm identification problem, the optimal solution for the CBMAI problem may be a randomized mixture of multiple arms. The goal thus is to find the best mixed arm that maximizes the expected reward subject to constraints on the expected costs with a given learning budget $N$. We propose a novel, parameter-free algorithm, called the Score Function-based Successive Reject (SFSR) algorithm, that combines the classical successive reject framework with a novel score-function-based rejection criteria based on linear programming theory to identify the optimal support. We provide a theoretical upper bound on the mis-identification (of the the support of the best mixed arm) probability and show that it decays exponentially in the budget $N$ and some constants that characterize the hardness of the problem instance. We also develop an information theoretic lower bound on the error probability that shows that these constants appropriately characterize the problem difficulty. We validate this empirically on a number of average and hard instances.

Graph lottery tickets (GLTs), comprising a sparse graph neural network (GNN) and a sparse input graph adjacency matrix, can significantly reduce the computing footprint of inference tasks compared to their dense counterparts. However, their performance against adversarial attacks remains to be fully explored. In this paper, we first investigate the resilience of GLTs against different {poisoning attacks based on structure perturbations} and observe that they are vulnerable and show a large drop in classification accuracy. We then present an \emph{adversarially robust graph sparsification (ARGS)} framework that prunes the adjacency matrix and the GNN weights by minimizing a novel loss function capturing the graph homophily property and information associated with the true labels of the train nodes and the pseudo labels of the test nodes. By iteratively applying ARGS to prune both the perturbed graph adjacency matrix and the GNN model weights, we can find graph lottery tickets that are highly sparse yet achieve competitive performance under different training-time (poisoning) structure-perturbation attacks. Evaluations conducted on various benchmarks, considering {attacks} such as PGD, MetaAttack, PR-BCD, GR-BCD, and adaptive attack, demonstrate that ARGS can significantly improve the robustness of the generated GLTs, even when subjected to high levels of sparsity.

The design of complex mission-critical systems often follows a layered approach, which may lead to complicated, multilevel, multiviewpoint 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 article, 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 multiagent autonomous lunar rover mission.

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.