A Formal Verification Approach to the Design of Synthetic Gene Networks

TL;DR

This paper introduces an automated formal verification framework for synthetic gene networks, enabling in silico validation of designs against specifications to reduce experimental costs and improve reliability.

Contribution

It presents a novel method that constructs mathematical models from experimental data and verifies their correctness using model checking techniques, streamlining synthetic biology design processes.

Findings

Successfully verified synthetic gene network designs against specifications

Filtered potential designs to identify those meeting functional criteria

Demonstrated applicability through illustrative examples

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. Illustrative examples of the application of our methods to the design of simple synthetic gene networks are included.