Syntax-Guided Optimal Synthesis for Chemical Reaction Networks

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F17%3APU127274" target="_blank" >RIV/00216305:26230/17:PU127274 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-319-63390-9_20" target="_blank" >http://dx.doi.org/10.1007/978-3-319-63390-9_20</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-63390-9_20" target="_blank" >10.1007/978-3-319-63390-9_20</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Syntax-Guided Optimal Synthesis for Chemical Reaction Networks

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Syntax-Guided Optimal Synthesis for Chemical Reaction Networks

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA16-17538S" target="_blank" >GA16-17538S: Přibližná ekvivalence pro aproximativní počítání</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2017

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of the 29th International Conference on Computer Aided Verification

ISBN

978-3-319-63390-9

ISSN

—

e-ISSN

—

Počet stran výsledku

20

Strana od-do

375-395

Název nakladatele

Springer Verlag

Místo vydání

Heidelberg

Místo konání akce

Heidelberg

Datum konání akce

2. 5. 2017

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000431900900020