Experimentally driven verification of synthetic biological circuits

Download
2012-04-03
Yordanov, Boyan
Appleton, Evan
Ganguly, Rishi
Aydın Göl, Ebru
Carr, Swati B
Bhatia, Swapnil
Haddock, Traci
Belta, Calin
Densmore, Douglas
We present a framework that allows us to construct and formally analyze the behavior of synthetic gene circuits from specifications in a high level language used in describing electronic circuits. Our back-end synthesis tool automatically generates genetic-regulatory network (GRN) topology realizing the specifications with assigned biological "parts" from a database. We describe experimental procedures to acquire characterization data for the assigned parts and construct mathematical models capturing all possible behaviors of the generated GRN. We delineate algorithms to create finite abstractions of these models, and novel analysis techniques inspired from model-checking to verify behavioral specifications using Linear Temporal Logic (LTL) formulae.