AF: Small: Verification Complexities of Self-Assembly Systems

Self-assembly is the natural process of small, unorganized components coming together to form complex structures. Some systems, such as DNA self-assembly, are powerful enough to simulate general-purpose computation during the self-assembly process. This type of "Algorithmic Self-Assembly" is fundamental to the functioning of living organisms. Moreover, understanding and harnessing the power of algorithmic self-assembly systems promises to allow for the algorithmic manipulation of matter, i.e., the ability to rearrange matter at the nanoscale in a fashion similar to the way a computer is programmed. Thus, a solid theoretical understanding of algorithmic self-assembly is fundamentally important for future nanotechnologies. Towards this goal, this project focuses on specific problems related to "verifying" the correctness of self-assembly systems under a number of experimentally motivated models. By designing algorithms for efficient verification, or categorizing the complexity of such problems, this project will provide important theoretical foundations for understanding algorithmic self-assembly and construction techniques that will be key to advancing the state of the field. In detail, this project focuses on a number of self-assembly models broadly broken up as being either "passive," in which system components attract or repel based on static surface chemistry, or "active" in which system components dynamically change state based on interactions. The project further classifies models based on whether a system is "geometric" (utilizing shape to allow or prevent attachment between components) or "non-geometric" (combination is based solely on bonding domains). The different models represent common implementation techniques such as DNA attachments, molecule bonding, or even laboratory procedures such as mixing and staging reactions. Within the categories, specific verification problems are considered, such as "Unique Assembly Verification" in which the problem is to determine if a given system uniquely assembles into a target assembly, and "Reachability," which asks if it is possible for a given system to reach a certain state or configuration. To solve these problems, the project investigators will apply their prior expertise within the models considered, as well as their expertise in relevant tools such as "Covert Computation," a cryptographic tool introduced by the investigators that has proven effective in resolving long-standing open problems related to verification in self-assembly. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.