A formal verification approach to the design of synthetic gene networks
Files
Accepted manuscript
Date
2011-01-01
Authors
Yordanov, Boyan
Belta, Calin
Version
OA Version
Citation
Boyan Yordanov, Calin Belta. 2011. "A Formal Verification Approach to the Design of Synthetic Gene Networks." 2011 50th IEEE Conference on Decision and Control and European Control Conference (CDC-ECC), pp. 4873 - 4878 (6).
Abstract
The design of genetic networks with specific functions is one of the major goals of synthetic biology. However, constructing biological devices that work “as required” remains challenging, while the cost of uncovering flawed designs experimentally is large. To address this issue, we propose a fully automated framework that allows the correctness of synthetic gene networks to be formally verified in silico from rich, high level functional specifications. Given a device, we automatically construct a mathematical model from experimental data characterizing the parts it is composed of. The specific model structure guarantees that all experimental observations are captured and allows us to construct finite abstractions through polyhedral operations. The correctness of the model with respect to temporal logic specifications can then be verified automatically using methods inspired by model checking. Overall, our procedure is conservative but it can filter through a large number of potential device designs and select few that satisfy the specification, to be implemented and tested further experimentally. As illustration, our methods are applied to the design of a simple synthetic gene network.