The design-build-test-learn workflow is pivotal in synthetic biology as it seeks to broaden access to diverse levels of expertise and enhance circuit complexity through recent advancements in automation. The design of complex circuits depends on developing precise models and parameter values for predicting the circuit performance and noise resilience. However, obtaining characterized parameters under diverse experimental conditions is a significant challenge, often requiring substantial time, funding, and expertise. This work compares five computational models of three different genetic circuit implementations of the same logic function to evaluate their relative predictive capabilities. The primary focus is on determining whether simpler models can yield conclusions similar to those of more complex ones and whether certain models offer greater analytical benefits. These models explore the influence of noise, parametrization, and model complexity on predictions of synthetic circuit performance through simulation. The findings suggest that when developing a new circuit without characterized parts or an existing design, any model can effectively predict the optimal implementation by facilitating qualitative comparison of designs' failure probabilities (e.g., higher or lower). However, when characterized parts are available and accurate quantitative differences in failure probabilities are desired, employing a more precise model with characterized parts becomes necessary, albeit requiring additional effort.

This work introduces an open-source hardware and software expansion for digital microfluidics (DMF) devices that integrates programmatic temperature and magnetic control. Our aim was to create a versatile, modular, extension that may aid in biomedical applications and has proven potential for use in bacteriophage research. To achieve this, we developed an accessible DMF device extension called PhageBox. PhageBox incorporates temperature and magnetic control modules at the hardware level. At the software level, it is controlled by embedded software that includes a unique model for bio-protocol programming and a graphical user interface for visual feedback and operation of the device. We evaluated PhageBox's effectiveness in biomedical applications using functional testing and validated the temperature control using thermography, achieving a range of +/-0.2 Celsius. The electromagnets produced a magnetic force of 15 milliTesla, which precisely immobilized magnetic beads. Furthermore, we demonstrate the potential of PhageBox in bacteriophage research through three initial proof of principle protocols: (1) a universal framework for PCR, (2) T7 bacteriophage restriction enzyme digestion, and (3) the concentration of PhiX174 RF genomic DNA. Overall, our study presents an open-source solution for DMF devices to integrate temperature regulation and magnetism, facilitating various applications in biomedical research and bacteriophage studies. (GitHub: https://github.com/Dreycey/PhageBox)

Probabilistic Model Checking (PMC) is a valuable tool for automated analysis of systems exhibiting stochastic behavior. However, the effectiveness of PMC algorithms is limited to systems that can be modeled by a finite state-space. Chemical Reaction Networks (CRNs) are commonly used to describe biochemical systems. Since there are usually no upper-bounds on the population of species in a CRN, they can only be modeled as an infinite-state stochastic model. This paper proposes a new approach that can analyze infinite-state CRNs by bounding their state-space. For a property indicating that the probability of the event of interest is less than a certain threshold value, the objective is to generate a bounded range on the population of each species in the CRN such that this bounded CRN already retains sufficient probability to refute the property under investigation. The effectiveness of this approach is demonstrated by analyzing rare-event properties on a number of biochemical systems.

Improving the scalability of probabilistic model checking (PMC) tools is crucial to the verification of real-world system designs. The Stamina infinite-state PMC tool achieves scalability by iteratively constructing a partial state space for an unbounded continuous-time Markov chain model, where a majority of the probability mass resides. It then performs time-bounded transient PMC. It can efficiently produce an accurate probability bound to the property under verification. We present a new software architecture design and the C++ implementation of the Stamina 2.0 algorithm, integrated with the Storm model checker. This open-source Stamina implementation offers a high degree of modularity and provides significant optimizations to the Stamina 2.0 algorithm. Performance improvements are demonstrated on multiple challenging benchmark examples, including hazard analysis of infinite-state combinational genetic circuits, over the previous Stamina implementation. Additionally, its design allows for future customizations and optimizations to the Stamina algorithm.

Synthetic biology builds upon genetics, molecular biology, and metabolic engineering by applying engineering principles to the design of biological systems. When designing a synthetic system, synthetic biologists need to exchange information about multiple types of molecules, the intended behavior of the system, and actual experimental measurements. The Synthetic Biology Open Language (SBOL) has been developed as a standard to support the specification and exchange of biological design information in synthetic biology, following an open community process involving both wet bench scientists and dry scientific modelers and software developers, across academia, industry, and other institutions. This document describes SBOL 3.0.0, which condenses and simplifies previous versions of SBOL based on experiences in deployment across a variety of scientific and industrial settings. In particular, SBOL 3.0.0, (1) separates sequence features from part/sub-part relationships, (2) renames Component Definition/Component to Component/Sub-Component, (3) merges Component and Module classes, (4) ensures consistency between data model and ontology terms, (5) extends the means to define and reference Sub-Components, (6) refines requirements on object URIs, (7) enables graph-based serialization, (8) moves Systems Biology Ontology (SBO) for Component types, (9) makes all sequence associations explicit, (10) makes interfaces explicit, (11) generalizes Sequence Constraints into a general structural Constraint class, and (12) expands the set of allowed constraints.

Rare events are of particular interest in synthetic biology because rare biochemical events may be catastrophic to a biological system by, for example, triggering irreversible events such as off-target drug delivery. To estimate the probability of rare events efficiently, several weighted stochastic simulation methods have been developed. Under optimal parameters and model conditions, these methods can greatly improve simulation efficiency in comparison to traditional stochastic simulation. Unfortunately, the optimal parameters and conditions cannot be deduced a priori. This paper presents a critical survey of weighted stochastic simulation methods. It shows that the methods considered here cannot consistently, efficiently, and exactly accomplish the task of rare event simulation without resorting to a computationally expensive calibration procedure, which undermines their overall efficiency. The results suggest that further development is needed before these methods can be deployed for general use in biological simulations.

Synthetic biology research has led to the development of many software tools for designing, constructing, editing, simulating, and sharing genetic parts and circuits. Among these tools are SBOLCanvas, iBioSim, and SynBioHub, which can be used in conjunction to create a genetic circuit design following the design–build–test–learn process. However, although automation works within these tools, most of these software tools are not integrated, and the process of transferring information between them is a very manual, error-prone process. To address this problem, this work automates some of these processes and presents SynBioSuite, a cloud-based tool that eliminates many of the drawbacks of the current approach by automating the setup and reception of results for simulating a designed genetic circuit via an application programming interface.

Stochastic model checking (SMC) is a formal verification technique for the analysis of systems with probabilistic behavior. Scalability has been a major limiting factor for SMC tools to analyze real-world systems with large or infinite state spaces. The infinite-state Continuous-time Markov Chain (CTMC) model checker, STAMINA, tackles this problem by selectively exploring only a portion of a model's state space, where a majority of the probability mass resides, to efficiently give an accurate probability bound to properties under verification. In this paper, we present two major improvements to STAMINA, namely, a method of calculating and distributing estimated state reachability probabilities that improves state space truncation efficiency and combination of the previous two CTMC analyses into one for generating the probability bound. Demonstration of the improvements on several benchmark examples, including hazard analysis of infinite-state combinational genetic circuits, yield significant savings in both run-time and state space size (and hence memory), compared to both the previous version of STAMINA and the infinite-state CTMC model checker INFAMY. The improved STAMINA demonstrates significant scalability to allow for the verification of complex real-world infinite-state systems.

Synthetic biology (SynBio) is a field at the intersection of biology and engineering. Inspired by engineering principles, researchers use defined parts to build functionally defined biological circuits. Genetic design automation (GDA) allows scientists to design, model, and analyze their genetic circuits in silico before building them in the lab, saving time, and resources in the process. Establishing SynBio???s future is dependent on GDA, since the computational approach opens the field to a broad, interdisciplinary community. However, challenges with part libraries, standards, and software tools are currently stalling progress in the field. This review first covers recent advancements in GDA, followed by an assessment of the challenges ahead, and a proposed automated genetic design workflow for the future.

In synthetic biology, combinational circuits are used to program cells for various new applications like biosensors, drug delivery systems, and biofuels. Similar to asynchronous electronic circuits, some combinational genetic circuits may show unwanted switching variations (glitches) caused by multiple input changes. Depending on the biological circuit, glitches can cause irreversible effects and jeopardize the circuit's functionality. This paper presents a stochastic analysis to predict glitch propensities for three implementations of a genetic circuit with known glitching behavior. The analysis uses STochastic Approximate Model-checker for INfinite-state Analysis (STAMINA), a tool for stochastic verification. The STAMINA results were validated by comparison to stochastic simulation in iBioSim resulting in further improvements of STAMINA. This paper demonstrates that stochastic verification can be utilized by genetic designers to evaluate design choices and input restrictions to achieve a desired reliability of operation.