Formal Reasoning about Synthetic Biology using Higher-order-logic Theorem Proving

Abstract

Synthetic biology is an interdisciplinary field that applies well-established engineering principles — electrical, control, and computer systems — to analyze biological systems such as circuits, enzymes, pathways, and controllers. Controllers play a pivotal role in regulating genetic circuits and other biological organisms, but are traditionally analyzed using paper-and-pencil proofs and computer simulations, which suffer from human error-proneness, round-off errors, and unverified underlying algorithms.

We propose higher-order-logic theorem proving as a complementary technique: modeling the continuous dynamics of genetic circuits and controllers with differential equations derived from reaction-based models, deriving transfer functions from block-diagram representations, and performing Laplace-transform-based stability analysis. We illustrate the framework on genetic circuits of activated and repressed protein expression, autoactivation, and phase lag/lead controllers.

People