We present the algebra of assume-guarantee (AG) contracts. We define contracts, provide new as well as known operations, and show how these operations are related. Contracts are functorial: any Boolean algebra has an associated contract algebra. We study monoid and semiring structures in contract algebra -- and the mappings between such structures. We discuss the actions of a Boolean algebra on its contract algebra.

Large Language models (LLMs) have shown promise as generators of symbolic control policies, producing interpretable program-like representations through iterative search. However, these models are not capable of separating the functional structure of a policy from the numerical values it is parametrized by, thus making the search process slow and inefficient. We propose a hybrid approach that decouples structural synthesis from parameter optimization by introducing an additional optimization layer for local parameter search. In our method, the numerical parameters of LLM-generated programs are extracted and optimized numerically to maximize task performance. With this integration, an LLM iterates over the functional structure of programs, while a separate optimization loop is used to find a locally optimal set of parameters accompanying candidate programs. We evaluate our method on a set of control tasks, showing that it achieves higher returns and improved sample efficiency compared to purely LLM-guided search. We show that combining symbolic program synthesis with numerical optimization yields interpretable yet high-performing policies, bridging the gap between language-model-guided design and classical control tuning. Our code is available at https://sites.google.com/berkeley.edu/colmo.

Contract-based design is a method to facilitate modular design of systems. While there has been substantial progress on the theory of contracts, there has been less progress on practical algorithms for the algebraic operations in the theory. In this article, we present (1) principles to implement a contract-based design tool at scale and (2) Pacti, a tool that can efficiently compute these operations. We illustrate the use of Pacti in a variety of case studies.

The highly pathogenic avian influenza A(H5N1) virus threatens animal and human health globally. Innovative strategies are crucial for mitigating risks associated with airborne transmission and preventing outbreaks. In this study, we sought to investigate the efficacy of microwave inactivation against aerosolized A(H5N1) virus by identifying the optimal frequency band for a 10-min exposure and evaluating the impact of varying exposure times on virus inactivation. A(H5N1) was aerosolized and exposed to various microwave frequencies ranging from 8 to 16 GHz for a duration of 10 min. Viral titers were quantified using TCID50, and inactivation was assessed by comparing irradiated samples to controls. The 11–13 GHz band yielded the highest inactivation, with an average 89% mean reduction in A(H5N1) titer, particularly within the 11–12 GHz range, which exhibited peak efficacy. Based on the overall results, the optimal frequency band (8–12 GHz) was further tested with exposure durations of 1, 3, and 5 min. Inactivation was time-dependent, with a 5-minute exposure resulting in a 94% mean reduction, compared to 58% and 48% for 3- and 1-minute exposures, respectively. We conclude that optimized microwave emitters in high-risk environments like poultry farms and veterinary clinics could offer a novel, non-chemical approach to mitigating avian influenza spread and outbreaks.

The highly pathogenic avian influenza A(H5N1) virus threatens animal and human health globally. Innovative strategies are needed to reduce airborne transmission and prevent outbreaks. This study investigated the efficacy of microwave inactivation against aerosolized A(H5N1) by (1) identifying the optimal frequency band in 10 min of exposure and (2) evaluating the effect of exposure time. A(H5N1) was aerosolized and exposed to various microwave frequencies (between 8 and 16 GHz with different ranges) for 10 minutes. Viral titers were quantified using TCID50, and inactivation was assessed by comparing irradiated samples to controls. The 11−13 GHz band resulted in the highest inactivation, with an average of 89% mean reduction in A(H5N1) titer in particular in the range of 11-12 GHZ (pick of efficacy). Considering the overall tests and results, the optimal band (8-12 GHZ) was further tested with 1, 3, and 5-minute exposures. Inactivation was time-dependent, with 5-minute exposure yielding a 94% mean reduction, compared to 58% and 48% for 3 and 1-minute exposures, respectively. Optimized microwave emitters in high-risk environments like poultry farms and veterinary clinics could offer a novel, non-chemical approach to mitigating avian influenza spread and outbreaks.

A chiplet is an integrated circuit that encompasses a well-defined subset of an overall system's functionality. In contrast to traditional monolithic system-on-chips (SoCs), chiplet-based architecture can reduce costs and increase reusability, representing a promising avenue for continuing Moore's Law. Despite the advantages of multi-chiplet architectures, floorplan design in a chiplet-based architecture has received limited attention. Conflicts between cost and performance necessitate a trade-off in chiplet floorplan design since additional latency introduced by advanced packaging can decrease performance. Consequently, balancing power, performance, cost, area, and reliability is of paramount importance. To address this challenge, we propose Floorplet, a framework comprising simulation tools for performance reporting and comprehensive models for cost and reliability optimization. Our framework employs the open-source Gem5 simulator to establish the relationship between performance and floorplan for the first time, guiding the floorplan optimization of multi-chiplet architecture. The experimental results show that our framework decreases inter-chiplet communication costs by 24.81%.

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.

For cyber-physical systems, including robotics and autonomous vehicles, mass deployment has been hindered by fatal errors that occur when operating in rare events. To better understand failure modes, companies meticulously recreate rare crash events in simulation, but current methods do not easily allow for exploring ”what if” scenarios which could reveal how accidents might have been avoided. We present ScenicNL, an AI system that generates probabilistic scenario programs from natural language. Given the abundance of documented failures of autonomous vehicles due to regulatory requirements, we apply ScenicNL to police crash reports, providing a data-driven approach to capturing and understanding these failures. By using a probabilistic language such as Scenic, we can clearly and concisely represent such scenarios of interest and easily ask “what if” questions. We demonstrate how commonplace prompting techniques with Large Language Models are incapable of generating code for low-resource languages such as Scenic. We propose an AI system via the composition of several prompting techniques to extract the reasoning abilities needed to model probability distributions around the uncertainty in the crash events. Our system then uses Constrained Decoding and tools such as a compiler and simulator to produce scenario programs in this low-resource setting. We evaluate our system on publicly available autonomous vehicle crash reports in California from the last five years and share insights into how we generate code that is both semantically meaningful and syntactically correct. Finally, we release our code and a collection of over 500 crash reports from the California Department of Motor Vehicles.

Simulation-based falsification has proved to be an effective verification method for cyber-physical systems. Traditional approaches to falsification take as input a single or a set of temporal properties that must be satisfied by the system at all times. In this paper, we consider falsification of a more complex specification with two dimensions: multiple objectives with relative priorities and the evolution of these objectives characterized by time-varying priorities. We introduce the concept of dynamic rulebooks as a way to specify a prioritized multi-objective specification and its evolution over time. We develop a novel algorithm for falsifying a dynamic rulebook specification on a cyber-physical system. To evaluate our approach, we define scenarios and dynamic rulebook specifications for the domains of autonomous driving and human-robot interaction. Our experiments demonstrate that integrating dynamic rulebooks allows us to capture counterexamples more accurately and efficiently than when using static rulebooks. Moreover, our falsification framework identifies more numerous and more significant counterexamples as compared to previous approaches.

We provide a method to synthesize an LTL Assume/Guarantee (A/G) specification, or contract, as an interconnection of elements from a library, each of which is also represented by an LTL A/G contract. Our approach, based on counterexample-guided inductive synthesis, leverages an off-the-shelf model checker to reason about infinite-length counterexamples and guarantee correctness. To increase scalability, we also introduce a novel concept of specification decomposition, based on contract projections; we show how it can be used to break down our synthesis problem into several simpler tasks, without reducing the size of the solution space. We test our technique on three industry-relevant case studies.

Deep reinforcement learning (DRL) has had success across various domains, but applying it to environments with constraints remains challenging due to poor sample efficiency and slow convergence. Recent literature explored incorporating model knowledge to mitigate these problems, particularly through the use of models that assess the feasibility of proposed actions. However, integrating feasibility models efficiently into DRL pipelines in environments with continuous action spaces is non-trivial. We propose a novel DRL training strategy utilizing action mapping that leverages feasibility models to streamline the learning process. By decoupling the learning of feasible actions from policy optimization, action mapping allows DRL agents to focus on selecting the optimal action from a reduced feasible action set. We demonstrate through experiments that action mapping significantly improves training performance in constrained environments with continuous action spaces, especially with imperfect feasibility models.

In reinforcement learning (RL), exploiting environmental symmetries can significantly enhance efficiency, robustness, and performance. However, ensuring that the deep RL policy and value networks are respectively equivariant and invariant to exploit these symmetries is a substantial challenge. Related works try to design networks that are equivariant and invariant by construction, limiting them to a very restricted library of components, which in turn hampers the expressiveness of the networks. This paper proposes a method to construct equivariant policies and invariant value functions without specialized neural network components, which we term equivariant ensembles. We further add a regularization term for adding inductive bias during training. In a map-based path planning case study, we show how equivariant ensembles and regularization benefit sample efficiency and performance.

We propose a context-sensitive grammar for the systematic exploration of the design space of the topology of 3D robots, particularly unmanned aerial vehicles. It defines production rules for adding components to an incomplete design topology modeled over a 3D grid. The rules are local. The grammar is simple, yet capable of modeling most existing UAVs as well as novel ones. It can be easily generalized to other robotic platforms. It can be thought of as a building block for any design exploration and optimization algorithm.

Complexity and heterogeneity are fundamental challenges for system design, as they prolong the design process and increase its cost. Independent design is a promising design flow to address these challenges whereby a supplier can develop its component without exchanging system-level information with other suppliers. Recent research on assume-guarantee contracts and contract-based design has focused on algebraic concepts, such as refinement and composition, to achieve independent design. However, the conventional definition of assume-guarantee contracts may result in implementations that may not operate correctly in the targeted environment of the system, thus hindering independent design. In this paper, we introduce the concept of contract replaceability, a binary relation on contracts that prevents this problem. We then extend the requirements to include receptiveness as a constraint on assume-guarantee contracts to ensure strong replaceability. The properties derived from the constraints ensure that strong replaceability is satisfied under contract refinement and cascade composition. Thus any assume-guarantee contract that satisfies this constraint permits independent design

Microelectronics has been the center of renewed interest worldwide due to production shortage that caused major problems to the electronics industry and other sectors such as automotive. Design of semiconductors has become increasingly challenging for the lack of designers and of the difficulties inherent in the development of products involving billions of transistors. The advent of chiplets has created further complexities in the design process. It is also clear that the overall issue is the design of integrated SYSTEM design where sensors, actuators, communication and computing elements have to be considered holistically. Given that these components may be best implemented with different technologies, decisions about integrated versus multi-chip solutions are critical. Among the computing elements, there has been an increasing interest in AI components. Tradeoffs between analog and digital solutions to AI chips are also becoming critical. I will review the general directions of integrated system design and of AI computing blocks.

Deriving system-level specifications from component specifications usually involves the elimination of variables that are not part of the interface of the top-level system. This paper presents algorithms for eliminating variables from formulas by computing refinements or relaxations of these formulas in a context. We discuss a connection between this problem and optimization and give efficient algorithms to compute refinements and relaxations of linear inequality constraints.

Defossilization of the current energy system is a major requirement to decelerate anthropogenic climate change. However, a defossilized energy system is vastly more complex than current fossil-based energy systems: The integration of distributed energy resources and sector-coupling increases connectivity, demands interdisciplinary workflows, and creates a need for more sophisticated design processes. Inspired by the semiconductor and automotive industries, digitalization of the design process using platform-based design (PBD), coupled with the energy hub concept, can improve cost-effective energy systems design and accelerate the industry's contributions to achieving net-zero emissions. PBD is an efficient and effective methodology to manage and de-risk the complexity of integrated energy system design, leading to affordable and reliable solutions due to the inherent techno-economic analysis underlying the decision-making process. Combining the PBD framework with the energy hub concepts establishes a powerful design workflow for developing holistic energy systems from a single building up to the district and city scales. The fundamental tenets of this workflow, as discussed in this paper, are (1) the separation of functions from architectures, (2) the identification of abstraction levels at which systems can be analyzed and optimized, and (3) the ability to repurpose components at all levels of abstraction to aid design reuse and allow performance feedback at every stage of the process. We argue that PBD can become the next frontier in energy system design. PBD, as presented in this paper, is not limited to the energy sector, and it can also be a sub-process of an even more holistic infrastructure design. Spatial planning, architecture, and civil engineering can all be further integrated with the PBD concept, allowing societies to reach ambitious sustainability goals faster, at lower cost, and with greater resilience.

Deep neural networks (DNNs) are vulnerable to backdoor attack, which does not affect the network's performance on clean data but would manipulate the network behavior once a trigger pattern is added. Existing defense methods have greatly reduced attack success rate, but their prediction accuracy on clean data still lags behind a clean model by a large margin. Inspired by the stealthiness and effectiveness of backdoor attack, we propose a simple but highly effective defense framework which injects non-adversarial backdoors targeting poisoned samples. Following the general steps in backdoor attack, we detect a small set of suspected samples and then apply a poisoning strategy to them. The non-adversarial backdoor, once triggered, suppresses the attacker's backdoor on poisoned data, but has limited influence on clean data. The defense can be carried out during data preprocessing, without any modification to the standard end-to-end training pipeline. We conduct extensive experiments on multiple benchmarks with different architectures and representative attacks. Results demonstrate that our method achieves state-of-the-art defense effectiveness with by far the lowest performance drop on clean data. Considering the surprising defense ability displayed by our framework, we call for more attention to utilizing backdoor for backdoor defense. Code is available at https://github.com/damianliumin/non-adversarial_backdoor.

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.