Oxford logo
[CCF+17] L. Cardelli, M. Ceska, M. Fraenzle, M. Kwiatkowska, L. Laurenti, N. Paoletti and M. Whitby. Syntax-Guided Optimal Synthesis for Chemical Reaction Networks. In Proc. 29th International Conference on Computer Aided Verification (CAV), Springer. To appear. 2017. [pdf] [bib]
Downloads:  pdf pdf (412 KB)  bib bib
Notes: The original publication is available at link.springer.com.
Abstract. We study the problem of optimal syntax-guided synthesis of stochastic Chemical Reaction Networks (CRNs) that plays a fundamental role in design automation of molecular devices and in the construction of predictive biochemical models. We propose a sketching language for CRNs that concisely captures syntactic constraints on the network topology and allows its under-specifi cation. Given a sketch, a correctness specifi cation, and a cost function defi ned over the CRN syntax, our goal is to fi nd a CRN that simultaneously meets the constraints, satisfi es the specifi cation and minimizes the cost function. To ensure computational feasibility of the synthesis process, we employ the Linear Noise Approximation allowing us to encode the synthesis problem as a satis fiability modulo theories problem over a set of parametric Ordinary Differential Equations (ODEs). We design and implement a novel algorithm for the optimal synthesis of CRNs that employs almost complete refutation procedure for SMT over reals and ODEs, and exploits a meta-sketching abstraction controlling the search strategy. Through relevant case studies we demonstrate that our approach signifi cantly improves the capability of existing methods for synthesis of biochemical systems and paves the way towards their automated and provably-correct design.