A temporal logic approach to modular design of synthetic biological circuits

TL;DR

This paper introduces a novel method for designing synthetic biological circuits using signal temporal logic (STL) to specify and verify module behaviors, enabling systematic parameter space analysis and robustness assessment.

Contribution

It presents a new STL-based framework for modular biological circuit design, characterizing modules, constraining parameters, and synthesizing implementations like a half-adder.

Findings

Characterized biological modules with STL formulae

Identified parameter regions satisfying specifications

Synthesized a biological half-adder implementation

Abstract

We present a new approach for the design of a synthetic biological circuit whose behaviour is specified in terms of signal temporal logic (STL) formulae. We first show how to characterise with STL formulae the input/output behaviour of biological modules miming the classical logical gates (AND, NOT, OR). Hence, we provide the regions of the parameter space for which these specifications are satisfied. Given a STL specification of the target circuit to be designed and the networks of its constituent components, we propose a methodology to constrain the behaviour of each module, then identifying the subset of the parameter space in which those constraints are satisfied, providing also a measure of the robustness for the target circuit design. This approach, which leverages recent results on the quantitative semantics of Signal Temporal Logic, is illustrated by synthesising a biological implementation of an half-adder.