Publication Details

Syntax-Guided Optimal Synthesis for Chemical Reaction Networks

CARDELLI Luca, ČEŠKA Milan, FRANZLE Martin, KWIATKOWSKA Marta, LAURENTI Luca, PAOLETTI Nicola and WHITBY Max. Syntax-Guided Optimal Synthesis for Chemical Reaction Networks. In: Proceedings of the 29th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 10427. Heidelberg: Springer Verlag, 2017, pp. 375-395. ISBN 978-3-319-63390-9.
Czech title
Syntéza biochemických reakčních sítí
Type
conference paper
Language
english
Authors
Cardelli Luca (MSR)
Češka Milan, doc. RNDr., Ph.D. (DITS FIT BUT)
Franzle Martin (UO)
Kwiatkowska Marta (UOx)
Laurenti Luca (UOx)
Paoletti Nicola (UOx)
Whitby Max (UOx)
Keywords

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

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-specification. 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 meta-sketching 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 provably-correct design.

Published
2017
Pages
375-395
Proceedings
Proceedings of the 29th International Conference on Computer Aided Verification
Series
Lecture Notes in Computer Science
Volume
10427
Conference
29th International Conference on Computer Aided Verification, Heidelberg, DE
ISBN
978-3-319-63390-9
Publisher
Springer Verlag
Place
Heidelberg, DE
DOI
UT WoS
000431900900020
EID Scopus
BibTeX
@INPROCEEDINGS{FITPUB11432,
   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 = "Syntax-Guided Optimal Synthesis for Chemical Reaction Networks",
   pages = "375--395",
   booktitle = "Proceedings of the 29th International Conference on Computer Aided Verification",
   series = "Lecture Notes in Computer Science",
   volume = 10427,
   year = 2017,
   location = "Heidelberg, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-319-63390-9",
   doi = "10.1007/978-3-319-63390-9\_20",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11432"
}
Back to top