Syntax-Guided Optimal Synthesis for Chemical Reaction Networks View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2017-07-13

AUTHORS

Luca Cardelli , Milan Češka , Martin Fränzle , Marta Kwiatkowska , Luca Laurenti , Nicola Paoletti , Max Whitby

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. More... »

PAGES

375-395

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-63390-9_20

DOI

http://dx.doi.org/10.1007/978-3-319-63390-9_20

DIMENSIONS

https://app.dimensions.ai/details/publication/pub.1090658108


Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
Incoming Citations Browse incoming citations for this publication using opencitations.net

JSON-LD is the canonical representation for SciGraph data.

TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

[
  {
    "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
    "about": [
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information and Computing Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0802", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computation Theory and Mathematics", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Microsoft Research Cambridge, Cambridge, UK", 
            "Department of Computer Science, University of Oxford, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Cardelli", 
        "givenName": "Luca", 
        "id": "sg:person.013522516217.56", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013522516217.56"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Information Technology, Brno University of Technology, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.4994.0", 
          "name": [
            "Faculty of Information Technology, Brno University of Technology, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "\u010ce\u0161ka", 
        "givenName": "Milan", 
        "id": "sg:person.016652663056.36", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016652663056.36"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, Carl von Ossietzky Universit\u00e4t Oldenburg, Oldenburg, Germany", 
          "id": "http://www.grid.ac/institutes/grid.5560.6", 
          "name": [
            "Department of Computer Science, Carl von Ossietzky Universit\u00e4t Oldenburg, Oldenburg, Germany"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Fr\u00e4nzle", 
        "givenName": "Martin", 
        "id": "sg:person.014144524353.44", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014144524353.44"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Kwiatkowska", 
        "givenName": "Marta", 
        "id": "sg:person.011375012273.39", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Laurenti", 
        "givenName": "Luca", 
        "id": "sg:person.011532541500.46", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011532541500.46"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, Stony Brook University, Stony Brook, USA", 
          "id": "http://www.grid.ac/institutes/grid.36425.36", 
          "name": [
            "Department of Computer Science, Stony Brook University, Stony Brook, USA"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Paoletti", 
        "givenName": "Nicola", 
        "id": "sg:person.014036566653.01", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014036566653.01"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Whitby", 
        "givenName": "Max", 
        "id": "sg:person.016314474526.42", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016314474526.42"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2017-07-13", 
    "datePublishedReg": "2017-07-13", 
    "description": "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.", 
    "editor": [
      {
        "familyName": "Majumdar", 
        "givenName": "Rupak", 
        "type": "Person"
      }, 
      {
        "familyName": "Kun\u010dak", 
        "givenName": "Viktor", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-63390-9_20", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-319-63389-3", 
        "978-3-319-63390-9"
      ], 
      "name": "Computer Aided Verification", 
      "type": "Book"
    }, 
    "keywords": [
      "syntax-guided synthesis", 
      "Satisfiability Modulo Theories (SMT) problem", 
      "cost function", 
      "complete refutation procedure", 
      "correctness specification", 
      "network topology", 
      "novel algorithm", 
      "design automation", 
      "refutation procedure", 
      "computational feasibility", 
      "chemical reaction networks", 
      "theory problems", 
      "search strategy", 
      "syntactic constraints", 
      "network", 
      "syntax", 
      "synthesis problem", 
      "relevant case studies", 
      "specification", 
      "correct design", 
      "stochastic chemical reaction networks", 
      "constraints", 
      "parametric ordinary differential equations", 
      "automation", 
      "algorithm", 
      "case study", 
      "reaction networks", 
      "abstraction", 
      "language", 
      "SMT", 
      "optimal synthesis", 
      "topology", 
      "capability", 
      "sketch", 
      "set", 
      "biochemical systems", 
      "Real", 
      "system", 
      "devices", 
      "design", 
      "goal", 
      "linear noise approximation", 
      "feasibility", 
      "biochemical model", 
      "way", 
      "construction", 
      "synthesis process", 
      "method", 
      "model", 
      "fundamental role", 
      "noise approximation", 
      "strategies", 
      "process", 
      "ordinary differential equations", 
      "approximation", 
      "function", 
      "differential equations", 
      "procedure", 
      "equations", 
      "role", 
      "study", 
      "synthesis", 
      "problem", 
      "molecular devices", 
      "approach", 
      "optimal syntax-guided synthesis", 
      "predictive biochemical models", 
      "sketching language", 
      "CRN syntax", 
      "modulo theories problem", 
      "meta-sketching abstraction"
    ], 
    "name": "Syntax-Guided Optimal Synthesis for Chemical Reaction Networks", 
    "pagination": "375-395", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1090658108"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-63390-9_20"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-63390-9_20", 
      "https://app.dimensions.ai/details/publication/pub.1090658108"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-12-01T20:02", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20211201/entities/gbq_results/chapter/chapter_267.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-63390-9_20"
  }
]
 

Download the RDF metadata as:  json-ld nt turtle xml License info

HOW TO GET THIS DATA PROGRAMMATICALLY:

JSON-LD is a popular format for linked data which is fully compatible with JSON.

curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-63390-9_20'

N-Triples is a line-based linked data format ideal for batch operations.

curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-63390-9_20'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-63390-9_20'

RDF/XML is a standard XML format for linked data.

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-63390-9_20'


 

This table displays all metadata directly associated to this object as RDF triples.

188 TRIPLES      23 PREDICATES      96 URIs      89 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-63390-9_20 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N6abced46863e4d5eb5467646abf3fe59
4 schema:datePublished 2017-07-13
5 schema:datePublishedReg 2017-07-13
6 schema:description 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.
7 schema:editor N7dc98ff906d54796837c662d95baabb4
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf Nceff921e15ec412890ab60dd8da42cec
12 schema:keywords CRN syntax
13 Real
14 SMT
15 Satisfiability Modulo Theories (SMT) problem
16 abstraction
17 algorithm
18 approach
19 approximation
20 automation
21 biochemical model
22 biochemical systems
23 capability
24 case study
25 chemical reaction networks
26 complete refutation procedure
27 computational feasibility
28 constraints
29 construction
30 correct design
31 correctness specification
32 cost function
33 design
34 design automation
35 devices
36 differential equations
37 equations
38 feasibility
39 function
40 fundamental role
41 goal
42 language
43 linear noise approximation
44 meta-sketching abstraction
45 method
46 model
47 modulo theories problem
48 molecular devices
49 network
50 network topology
51 noise approximation
52 novel algorithm
53 optimal syntax-guided synthesis
54 optimal synthesis
55 ordinary differential equations
56 parametric ordinary differential equations
57 predictive biochemical models
58 problem
59 procedure
60 process
61 reaction networks
62 refutation procedure
63 relevant case studies
64 role
65 search strategy
66 set
67 sketch
68 sketching language
69 specification
70 stochastic chemical reaction networks
71 strategies
72 study
73 syntactic constraints
74 syntax
75 syntax-guided synthesis
76 synthesis
77 synthesis problem
78 synthesis process
79 system
80 theory problems
81 topology
82 way
83 schema:name Syntax-Guided Optimal Synthesis for Chemical Reaction Networks
84 schema:pagination 375-395
85 schema:productId N1044d32465e64124a304eccdd228d3db
86 N426c8182be6d4ff99106af781bc86bf3
87 schema:publisher N7027180b2393408cb14f54563c92e0d5
88 schema:sameAs https://app.dimensions.ai/details/publication/pub.1090658108
89 https://doi.org/10.1007/978-3-319-63390-9_20
90 schema:sdDatePublished 2021-12-01T20:02
91 schema:sdLicense https://scigraph.springernature.com/explorer/license/
92 schema:sdPublisher N39181a3df7fc43149c531ad0ba535f40
93 schema:url https://doi.org/10.1007/978-3-319-63390-9_20
94 sgo:license sg:explorer/license/
95 sgo:sdDataset chapters
96 rdf:type schema:Chapter
97 N082602e0fabd45f4a3d974b630d93e07 schema:familyName Kunčak
98 schema:givenName Viktor
99 rdf:type schema:Person
100 N1044d32465e64124a304eccdd228d3db schema:name dimensions_id
101 schema:value pub.1090658108
102 rdf:type schema:PropertyValue
103 N2eb717707c684c34a2aa6a0f7f57fcaa rdf:first sg:person.014144524353.44
104 rdf:rest N85506645710241d8b2dcfaba33660a70
105 N2ec327b2b3854f069de2781ca8496045 rdf:first sg:person.011532541500.46
106 rdf:rest Ndeee333b40544bb89e405509759e7c9d
107 N39181a3df7fc43149c531ad0ba535f40 schema:name Springer Nature - SN SciGraph project
108 rdf:type schema:Organization
109 N426c8182be6d4ff99106af781bc86bf3 schema:name doi
110 schema:value 10.1007/978-3-319-63390-9_20
111 rdf:type schema:PropertyValue
112 N6abced46863e4d5eb5467646abf3fe59 rdf:first sg:person.013522516217.56
113 rdf:rest Na01e5b4e33a24efe843cb71008a9aee1
114 N6c1cc577743d4b9cb0a63db7a962a6d1 rdf:first N082602e0fabd45f4a3d974b630d93e07
115 rdf:rest rdf:nil
116 N7027180b2393408cb14f54563c92e0d5 schema:name Springer Nature
117 rdf:type schema:Organisation
118 N7dc98ff906d54796837c662d95baabb4 rdf:first Nfafb4f85d7e648078ce27c30172a713e
119 rdf:rest N6c1cc577743d4b9cb0a63db7a962a6d1
120 N80f12bb4b6f848618f97ec50ae312604 rdf:first sg:person.016314474526.42
121 rdf:rest rdf:nil
122 N85506645710241d8b2dcfaba33660a70 rdf:first sg:person.011375012273.39
123 rdf:rest N2ec327b2b3854f069de2781ca8496045
124 Na01e5b4e33a24efe843cb71008a9aee1 rdf:first sg:person.016652663056.36
125 rdf:rest N2eb717707c684c34a2aa6a0f7f57fcaa
126 Nceff921e15ec412890ab60dd8da42cec schema:isbn 978-3-319-63389-3
127 978-3-319-63390-9
128 schema:name Computer Aided Verification
129 rdf:type schema:Book
130 Ndeee333b40544bb89e405509759e7c9d rdf:first sg:person.014036566653.01
131 rdf:rest N80f12bb4b6f848618f97ec50ae312604
132 Nfafb4f85d7e648078ce27c30172a713e schema:familyName Majumdar
133 schema:givenName Rupak
134 rdf:type schema:Person
135 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
136 schema:name Information and Computing Sciences
137 rdf:type schema:DefinedTerm
138 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
139 schema:name Computation Theory and Mathematics
140 rdf:type schema:DefinedTerm
141 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
142 schema:familyName Kwiatkowska
143 schema:givenName Marta
144 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
145 rdf:type schema:Person
146 sg:person.011532541500.46 schema:affiliation grid-institutes:grid.4991.5
147 schema:familyName Laurenti
148 schema:givenName Luca
149 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011532541500.46
150 rdf:type schema:Person
151 sg:person.013522516217.56 schema:affiliation grid-institutes:grid.4991.5
152 schema:familyName Cardelli
153 schema:givenName Luca
154 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013522516217.56
155 rdf:type schema:Person
156 sg:person.014036566653.01 schema:affiliation grid-institutes:grid.36425.36
157 schema:familyName Paoletti
158 schema:givenName Nicola
159 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014036566653.01
160 rdf:type schema:Person
161 sg:person.014144524353.44 schema:affiliation grid-institutes:grid.5560.6
162 schema:familyName Fränzle
163 schema:givenName Martin
164 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014144524353.44
165 rdf:type schema:Person
166 sg:person.016314474526.42 schema:affiliation grid-institutes:grid.4991.5
167 schema:familyName Whitby
168 schema:givenName Max
169 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016314474526.42
170 rdf:type schema:Person
171 sg:person.016652663056.36 schema:affiliation grid-institutes:grid.4994.0
172 schema:familyName Češka
173 schema:givenName Milan
174 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016652663056.36
175 rdf:type schema:Person
176 grid-institutes:grid.36425.36 schema:alternateName Department of Computer Science, Stony Brook University, Stony Brook, USA
177 schema:name Department of Computer Science, Stony Brook University, Stony Brook, USA
178 rdf:type schema:Organization
179 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, Oxford, UK
180 schema:name Department of Computer Science, University of Oxford, Oxford, UK
181 Microsoft Research Cambridge, Cambridge, UK
182 rdf:type schema:Organization
183 grid-institutes:grid.4994.0 schema:alternateName Faculty of Information Technology, Brno University of Technology, Brno, Czech Republic
184 schema:name Faculty of Information Technology, Brno University of Technology, Brno, Czech Republic
185 rdf:type schema:Organization
186 grid-institutes:grid.5560.6 schema:alternateName Department of Computer Science, Carl von Ossietzky Universität Oldenburg, Oldenburg, Germany
187 schema:name Department of Computer Science, Carl von Ossietzky Universität Oldenburg, Oldenburg, Germany
188 rdf:type schema:Organization
 




Preview window. Press ESC to close (or click here)


...