Despite the early success stories synthetic biology, the development of larger, more complex synthetic systems necessitates the use of appropriate design methodologies. In particular, the integration of smaller circuits in order to perform complex tasks remains one of the most important challenges faced in synthetic biology. We propose here a methodology to determine the region in the parameter space where a given dynamical model works as desired. It is based on the inverse problem of finding parameter sets that exhibit the specified behavior for a defined topology. The main issue we face is that such inverse mapping is highly expansive and suffers from instability: small changes in the specified dynamic property could lead to large deviations in the parameters for the identified models. To solve this issue, we discuss regularized maps complemented by local analysis. With a stabilized inversion map, small neighborhoods in the property space are mapped to small neighborhoods in the parameter space, thereby finding parameter vectors that are robust to the problem specification. To specify dynamic circuit properties we discuss Linear Temporal Logic (LTL). We apply these concepts to two models of the cyanobacterial circadian oscillation.
