Conference paperCARDELLI Luca, ČEŠKA Milan, FRANZLE Martin, KWIATKOWSKA Marta, LAURENTI Luca, PAOLETTI Nicola and WHITBY Max. SyntaxGuided Optimal Synthesis for Chemical Reaction Networks. In: Proceedings of the 29th International Conference on Computer Aided Verification. Heidelberg: Springer Verlag, 2017, pp. 375395. ISBN 9783319633909.  Publication language:  english 

Original title:  SyntaxGuided Optimal Synthesis for Chemical Reaction Networks 

Title (cs):  Syntéza biochemických reakčních sítí 

Pages:  375395 

Proceedings:  Proceedings of the 29th International Conference on Computer Aided Verification 

Conference:  29th International Conference on Computer Aided Verification 

Series:  LNCS 10427 

Place:  Heidelberg, DE 

Year:  2017 

ISBN:  9783319633909 

Publisher:  Springer Verlag 

Keywords 

chemical reaction network design automation optimal synthesis Linear Noise Approximation SMT solvers temporal logic 
Annotation 

We study the problem of optimal syntaxguided 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 underspecification. Given a sketch, a correctness specification, and a cost function defined over the CRN syntax, our goal is to find a CRN that simultaneously meets the constraints, satisfies the specification 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 satisfiability 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 metasketching abstraction controlling the search strategy. Through relevant case studies we demonstrate that our approach significantly improves the capability of existing methods for synthesis of biochemical systems and paves the way towards their automated and provablycorrect design. 
BibTeX: 

@INPROCEEDINGS{
author = {Luca Cardelli and Milan {\v{C}}e{\v{s}}ka and Martin Franzle
and Marta Kwiatkowska and Luca Laurenti and Nicola Paoletti
and Max Whitby},
title = {SyntaxGuided Optimal Synthesis for Chemical Reaction
Networks},
pages = {375395},
booktitle = {Proceedings of the 29th International Conference on Computer
Aided Verification},
series = {LNCS 10427},
year = {2017},
location = {Heidelberg, DE},
publisher = {Springer Verlag},
ISBN = {9783319633909},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php?id=11432}
} 
