SMT-Based Analysis of Biological Computation

In order to understand the functioning of organisms on the molecular level, we need to know which genes are expressed, when and where in the organism, and to which extent. The regulation of gene expression is achieved through genetic regulatory systems structured by networks of interactions between DNA, RNA, proteins, and small molecules. As most genetic regulatory networks of interest involve many components connected through interlocking positive and negative feedback loops, an intuitive understanding of their dynamics is hard to obtain. As a consequence, formal methods and computer tools for the modeling and simulation of genetic regulatory networks will be indispensable. This paper reviews formalisms that have been employed in mathematical biology and bioinformatics to describe genetic regulatory systems, in particular directed graphs, Bayesian networks, Boolean networks and their generalizations, ordinary and partial differential equations, qualitative differential equations, stochastic equations, and rule-based formalisms. In addition, the paper discusses how these formalisms have been used in the simulation of the behavior of actual regulatory systems.

Biological organisms perform complex information processing and control tasks using sophisticated biochemical circuits, yet the engineering of such circuits remains ineffective compared with that of electronic circuits. To systematically create complex yet reliable circuits, electrical engineers use digital logic, wherein gates and subcircuits are composed modularly and signal restoration prevents signal degradation. We report the design and experimental implementation of DNA-based digital logic circuits. We demonstrate AND, OR, and NOT gates, signal restoration, amplification, feedback, and cascading. Gate design and circuit construction is modular. The gates use single-stranded nucleic acids as inputs and outputs, and the mechanism relies exclusively on sequence recognition and strand displacement. Biological nucleic acids such as microRNAs can serve as inputs, suggesting applications in biotechnology and bioengineering.