Pierluigi Nuzzo

Shromona Ghosh, Dorsa Sadigh, Pierluigi Nuzzo et al.

We address the problem of diagnosing and repairing specifications for hybrid systems formalized in signal temporal logic (STL). Our focus is on the setting of automatic synthesis of controllers in a model predictive control (MPC) framework. We build on recent approaches that reduce the controller synthesis problem to solving one or more mixed integer linear programs (MILPs), where infeasibility of a MILP usually indicates unrealizability of the controller synthesis problem. Given an infeasible STL synthesis problem, we present algorithms that provide feedback on the reasons for unrealizability, and suggestions for making it realizable. Our algorithms are sound and complete, i.e., they provide a correct diagnosis, and always terminate with a non-trivial specification that is feasible using the chosen synthesis method, when such a solution exists. We demonstrate the effectiveness of our approach on the synthesis of controllers for various cyber-physical systems, including an autonomous driving application and an aircraft electric power system.

Krishna C Kalagarla, Rahul Jain, Pierluigi Nuzzo

Constrained Markov decision processes (CMDPs) model scenarios of sequential decision making with multiple objectives that are increasingly important in many applications. However, the model is often unknown and must be learned online while still ensuring the constraint is met, or at least the violation is bounded with time. Some recent papers have made progress on this very challenging problem but either need unsatisfactory assumptions such as knowledge of a safe policy, or have 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 achieves an efficient tradeoff between exploration and exploitation by use of the posterior sampling principle, and provably suffers only bounded constraint violation by leveraging the idea of pessimism. Our approach is based on a primal-dual approach. We establish a sub-linear $\tilde{\mathcal{ O}}\left(H^{2.5} \sqrt{|\mathcal{S}|^2 |\mathcal{A}| K} \right)$ upper bound on the Bayesian reward objective regret along with a bounded, i.e., $\tilde{\mathcal{O}}\left(1\right)$ constraint violation regret over $K$ episodes for an $|\mathcal{S}|$-state, $|\mathcal{A}|$-action and horizon $H$ CMDP.

Dengwang Tang, Dongze Ye, Rahul Jain et al.

Learning in POMDPs is known to be significantly harder than in MDPs. In this paper, we consider the online learning problem for episodic POMDPs with unknown transition and observation models. We propose a Posterior Sampling-based reinforcement learning algorithm for POMDPs (PS4POMDPs), which is much simpler and more implementable compared to state-of-the-art optimism-based online learning algorithms for POMDPs. We show that the Bayesian regret of the proposed algorithm scales as the square root of the number of episodes and is polynomial in the other parameters. In a general setting, the regret scales exponentially in the horizon length $H$, and we show that this is inevitable by providing a lower bound. However, when the POMDP is undercomplete and weakly revealing (a common assumption in the recent literature), we establish a polynomial Bayesian regret bound. We finally propose a posterior sampling algorithm for multi-agent POMDPs, and show it too has sublinear regret.

Kevin Chang, Nathan Dahlin, Rahul Jain et al.

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 first demonstrate the practical efficacy of the transformation algorithm applied to an autonomous driving NN controller within OpenAI Gym's CarRacing environment. Subsequently, we evaluate our approach using two benchmarks from the OpenAI Gym environment. Our results indicate that the SDT transformation can benefit formal verification, showing runtime improvements of up to $21 \times$ and $2 \times$ for MountainCar-v0 and CartPole-v1, respectively.

Matthew Low, Jasmine Jerry Aloor, Victoria Marie Tuck et al.

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.

Zhiyu Ni, Zheng Liang, Liangcheng Song et al.

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% accuracy with GPT-4 and 78.00% accuracy with GPT-4o, significantly outperforming the strongest AF baselines MAD-LOGIC and CLOVER. D&P then attains near-ceiling performance on the other benchmarks, including 100% on PrOntoQA and LogicalDeduction.

Shubhendra Pal Singhal, Sandeep Gupta, Pierluigi Nuzzo

This paper focuses on the explanation of the architecture of profilers particularly gprof and how to profile a program according to the user defined input of execution time . Gprof is a profiler available open source in the package of binutils. Gprof records the flow of the program including the callee and caller information and their respective execution time. This information is represented in the form of a call graph. Profilers at the time of execution creates a call graph file which indicates the full flow of the program including the individual execution time as well. This paper aims at providing a better understanding of the data structure used to store the information and how is a profiler(gprof) actually using this data structure to give user a readable format. The next section of this paper solves one of the limitation of gprof i.e. edit the time of block of code without understanding the call graph. Any changes in the execution time of a particular block of code would affect the total execution time. So if we edit the gprof in such a way that its consistent and platform independent, then it can yield various results like testing execution time after parallelism, before even designing it by replacing the values with theoretical/emulated ones and see if the total execution time is getting reduced by a desired number or not? Gprof edit can help us figure out that what section of code can be parallelized or which part of code is taking the most time and which call or part can be changed to reduce the execution time. The last section of the paper walks through the application of gprof in minisat and how gprof helps in the hardware acceleration in minisat by suggesting which part to be parallelised and how does it affect the total percentage.

Subhajit Dutta Chowdhury, Zhiyu Ni, Qingyuan Peng et al.

Graph Lottery Tickets (GLTs), comprising a sparse adjacency matrix and a sparse graph neural network (GNN), can significantly reduce the inference latency and compute footprint compared to their dense counterparts. Despite these benefits, their performance against adversarial structure perturbations remains to be fully explored. In this work, we first investigate the resilience of GLTs against different structure perturbation attacks and observe that they are highly vulnerable and show a large drop in classification accuracy. Based on this observation, we then present an adversarially robust graph sparsification (ARGS) framework that prunes the adjacency matrix and the GNN weights by optimizing a novel loss function capturing the graph homophily property and information associated with both 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 adversarially robust graph lottery tickets that are highly sparse yet achieve competitive performance under different untargeted training-time structure attacks. Evaluations conducted on various benchmarks, considering different poisoning structure attacks, namely, PGD, MetaAttack, Meta-PGD, and PR-BCD demonstrate that the GLTs generated by ARGS can significantly improve the robustness, even when subjected to high levels of sparsity.

Dengwang Tang, Rahul Jain, Ashutosh Nayyar et al.

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.

Tung-Wei Lin, Gabe Fierro, Han Li et al.

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 \emph{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.

Yifeng Xiao, Yurong Xu, Ning Yan et al.

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.

Krishna C. Kalagarla, Dhruva Kartik, Dongming Shen et al.

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.

Yuke Zhang, Yinghua Hu, Pierluigi Nuzzo et al.

Sequential logic locking has been studied over the last decade as a method to protect sequential circuits from reverse engineering. However, most of the existing sequential logic locking techniques are threatened by increasingly more sophisticated SAT-based attacks, efficiently using input queries to a SAT solver to rule out incorrect keys, as well as removal attacks based on structural analysis. In this paper, we propose TriLock, a sequential logic locking method that simultaneously addresses these vulnerabilities. TriLock can achieve high, tunable functional corruptibility while still guaranteeing exponential queries to the SAT solver in a SAT-based attack. Further, it adopts a state re-encoding method to obscure the boundary between the original state registers and those inserted by the locking method, thus making it more difficult to detect and remove the locking-related components.

Subhajit Dutta Chowdhury, Kaixin Yang, Pierluigi Nuzzo

Reverse engineering an integrated circuit netlist is a powerful tool to help detect malicious logic and counteract design piracy. A critical challenge in this domain is the correct classification of data-path and control-logic registers in a design. We present ReIGNN, a novel learning-based register classification methodology that combines graph neural networks (GNNs) with structural analysis to classify the registers in a circuit with high accuracy and generalize well across different designs. GNNs are particularly effective in processing circuit netlists in terms of graphs and leveraging properties of the nodes and their neighborhoods to learn to efficiently discriminate between different types of nodes. Structural analysis can further rectify any registers misclassified as state registers by the GNN by analyzing strongly connected components in the netlist graph. Numerical results on a set of benchmarks show that ReIGNN can achieve, on average, 96.5% balanced accuracy and 97.7% sensitivity across different designs.

Krishna C. Kalagarla, Rahul Jain, Pierluigi Nuzzo

We present a model-free reinforcement learning algorithm to find an optimal policy for a finite-horizon Markov decision process while guaranteeing a desired lower bound on the probability of satisfying a signal temporal logic (STL) specification. We propose a method to effectively augment the MDP state space to capture the required state history and express the STL objective as a reachability objective. The planning problem can then be formulated as a finite-horizon constrained Markov decision process (CMDP). For a general finite horizon CMDP problem with unknown transition probability, we develop a reinforcement learning scheme that can leverage any model-free RL algorithm to provide an approximately optimal policy out of the general space of non-stationary randomized policies. We illustrate the effectiveness of our approach in the context of robotic motion planning for complex missions under uncertainty and performance objectives.

Yinghua Hu, Yuke Zhang, Kaixin Yang et al.

The SAT attack has shown to be efficient against most combinational logic encryption methods. It can be extended to attack sequential logic encryption techniques by leveraging circuit unrolling and model checking methods. However, with no guidance on the number of times that a circuit needs to be unrolled to find the correct key, the attack tends to solve many time-consuming Boolean satisfiability (SAT) and model checking problems, which can significantly hamper its efficiency. In this paper, we introduce Fun-SAT, a functional corruptibility-guided SAT-based attack that can significantly decrease the SAT solving and model checking time of a SAT-based attack on sequential encryption by efficiently estimating the minimum required number of circuit unrollings. Fun-SAT relies on a notion of functional corruptibility for encrypted sequential circuits and its relationship with the required number of circuit unrollings in a SAT-based attack. Numerical results show that Fun-SAT can be, on average, 90x faster than previous attacks against state-of-the-art encryption methods, when both attacks successfully complete before a one-day time-out. Moreover, Fun-SAT completes before the time-out on many more circuits.

Nathan Dahlin, Krishna Chaitanya Kalagarla, Nikhil Naik et al.

In an ever expanding set of research and application areas, deep neural networks (DNNs) set the bar for algorithm performance. However, depending upon additional constraints such as processing power and execution time limits, or requirements such as verifiable safety guarantees, it may not be feasible to actually use such high-performing DNNs in practice. Many techniques have been developed in recent years to compress or distill complex DNNs into smaller, faster or more understandable models and controllers. This work seeks to identify reduced models that not only preserve a desired performance level, but also, for example, succinctly explain the latent knowledge represented by a DNN. We illustrate the effectiveness of the proposed approach on the evaluation of decision tree variants and kernel machines in the context of benchmark reinforcement learning tasks.

Yinghua Hu, Kaixin Yang, Shahin Nazarian et al.

We propose SANSCrypt, a novel sequential logic encryption scheme to protect integrated circuits against reverse engineering. Previous sequential encryption methods focus on modifying the circuit state machine such that the correct functionality can be accessed by applying the correct key sequence only once. Considering the risk associated with one-time authentication, SANSCrypt adopts a new temporal dimension to logic encryption, by requiring the user to sporadically perform multiple authentications according to a protocol based on pseudo-random number generation. Analysis and validation results on a set of benchmark circuits show that SANSCrypt offers a substantial output corruptibility if the key sequences are applied incorrectly. Moreover, it exhibits an exponential resilience to existing attacks, including SAT-based attacks, while maintaining a reasonably low overhead.

Krishna C. Kalagarla, Rahul Jain, Pierluigi Nuzzo

Constrained Markov Decision Processes (CMDPs) formalize sequential decision-making problems whose objective is to minimize a cost function while satisfying constraints on various cost functions. In this paper, we consider the setting of episodic fixed-horizon CMDPs. We propose an online algorithm which leverages the linear programming formulation of finite-horizon CMDP for repeated optimistic planning to provide a probably approximately correct (PAC) guarantee on the number of episodes needed to ensure an $ε$-optimal policy, i.e., with resulting objective value within $ε$ of the optimal value and satisfying the constraints within $ε$-tolerance, with probability at least $1-δ$. The number of episodes needed is shown to be of the order $\tilde{\mathcal{O}}\big(\frac{|S||A|C^{2}H^{2}}{ε^{2}}\log\frac{1}δ\big)$, where $C$ is the upper bound on the number of possible successor states for a state-action pair. Therefore, if $C \ll |S|$, the number of episodes needed have a linear dependence on the state and action space sizes $|S|$ and $|A|$, respectively, and quadratic dependence on the time horizon $H$.

Yinghua Hu, Vivek V. Menon, Andrew Schmidt et al.

Research in logic encryption over the last decade has resulted in various techniques to prevent different security threats such as Trojan insertion, intellectual property leakage, and reverse engineering. However, there is little agreement on a uniform set of metrics and models to efficiently assess the achieved security level and the trade-offs between security and overhead. This paper addresses the above challenges by relying on a general logic encryption model that can encompass all the existing techniques, and a uniform set of metrics that can capture multiple, possibly conflicting, security concerns. We apply our modeling approach to four state-of-the-art encryption techniques, showing that it enables fast and accurate evaluation of design trade-offs, average prediction errors that are at least 2X smaller than previous approaches, and the evaluation of compound encryption methods.

Jiwei Li, Pierluigi Nuzzo, Alberto Sangiovanni-Vincentelli et al.

We develop an assume-guarantee contract framework for the design of cyber-physical systems, modeled as closed-loop control systems, under probabilistic requirements. We use a variant of signal temporal logic, namely, Stochastic Signal Temporal Logic (StSTL) to specify system behaviors as well as contract assumptions and guarantees, thus enabling automatic reasoning about requirements of stochastic systems. Given a stochastic linear system representation and a set of requirements captured by bounded StSTL contracts, we propose algorithms that can check contract compatibility, consistency, and refinement, and generate a controller to guarantee that a contract is satisfied, following a stochastic model predictive control approach. Our algorithms leverage encodings of the verification and control synthesis tasks into mixed integer optimization problems, and conservative approximations of probabilistic constraints that produce both sound and tractable problem formulations. We illustrate the effectiveness of our approach on a few examples, including the design of embedded controllers for aircraft power distribution networks.

Yasser Shoukry, Pierluigi Nuzzo, Nicola Bezzo et al.

We address the problem of estimating the state of a differentially flat system from measurements that may be corrupted by an adversarial attack. In cyber-physical systems, malicious attacks can directly compromise the system's sensors or manipulate the communication between sensors and controllers. We consider attacks that only corrupt a subset of sensor measurements. We show that the possibility of reconstructing the state under such attacks is characterized by a suitable generalization of the notion of s-sparse observability, previously introduced by some of the authors in the linear case. We also extend our previous work on the use of Satisfiability Modulo Theory solvers to estimate the state under sensor attacks to the context of differentially flat systems. The effectiveness of our approach is illustrated on the problem of controlling a quadrotor under sensor attacks.

Yasser Shoukry, Pierluigi Nuzzo, Alberto Puggelli et al.

We address the problem of detecting and mitigating the effect of malicious attacks to the sensors of a linear dynamical system. We develop a novel, efficient algorithm that uses a Satisfiability-Modulo-Theory approach to isolate the compromised sensors and estimate the system state despite the presence of the attack, thus harnessing the intrinsic combinatorial complexity of the problem. By leveraging results from formal methods over real numbers, we provide guarantees on the soundness and completeness of our algorithm. We then report simulation results to compare its runtime performance with alternative techniques. Finally, we demonstrate its application to the problem of controlling an unmanned ground vehicle.

Pierluigi Nuzzo, John Finn, Mohammad Mozumdar et al.

In an aircraft electric power system (EPS), a supervisory control unit must actuate a set of switches to distribute power from generators to loads, while satisfying safety, reliability and real-time performance requirements. To reduce expensive re-design steps in current design methodologies, such a control problem is generally addressed based on minor incremental changes on top of consolidated solutions, since it is difficult to estimate the impact of earlier design decisions on the final implementation. In this paper, we introduce a methodology for the design space exploration and virtual prototyping of EPS supervisory control protocols, following the platform-based design (PBD) paradigm. Moreover, we describe the modeling infrastructure that supports the methodology. In PBD, design space exploration is carried out as a sequence of refinement steps from the initial specification towards a final implementation, by mapping higher-level behavioral models into a set of library components at a lower level of abstraction. In our flow, the system specification is captured using SysML requirement and structure diagrams. State-machine diagrams enable verification of the control protocol at a high level of abstraction, while lowerlevel hybrid models, implemented in Simulink, are used to verify properties related to physical quantities, such as time, voltage and current values. The effectiveness of our approach is illustrated on a prototype EPS control protocol design.