Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-affine Systems View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2016-09-22

AUTHORS

Nikola Beneš , Luboš Brim , Martin Demko , Samuel Pastva , David Šafránek

ABSTRACT

We propose a novel scalable parallel algorithm for synthesis of interdependent parameters from CTL specifications for non-linear dynamical systems. The method employs a symbolic representation of sets of parameter valuations in terms of the first-order theory of the reals. To demonstrate its practicability, we apply the method to a class of piecewise multi-affine dynamical systems representing dynamics of biological systems with complex non-linear behaviour. More... »

PAGES

192-208

Book

TITLE

Automated Technology for Verification and Analysis

ISBN

978-3-319-46519-7
978-3-319-46520-3

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-46520-3_13

DOI

http://dx.doi.org/10.1007/978-3-319-46520-3_13

DIMENSIONS

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


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/01", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Mathematical Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0101", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Pure Mathematics", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Systems Biology Laboratory, Faculty of Informatics, Masaryk University, Botanick\u00e1 68a, 602 00, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Systems Biology Laboratory, Faculty of Informatics, Masaryk University, Botanick\u00e1 68a, 602 00, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Bene\u0161", 
        "givenName": "Nikola", 
        "id": "sg:person.014465763501.21", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014465763501.21"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Systems Biology Laboratory, Faculty of Informatics, Masaryk University, Botanick\u00e1 68a, 602 00, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Systems Biology Laboratory, Faculty of Informatics, Masaryk University, Botanick\u00e1 68a, 602 00, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Brim", 
        "givenName": "Lubo\u0161", 
        "id": "sg:person.0645117057.83", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0645117057.83"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Systems Biology Laboratory, Faculty of Informatics, Masaryk University, Botanick\u00e1 68a, 602 00, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Systems Biology Laboratory, Faculty of Informatics, Masaryk University, Botanick\u00e1 68a, 602 00, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Demko", 
        "givenName": "Martin", 
        "id": "sg:person.016566512611.71", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016566512611.71"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Systems Biology Laboratory, Faculty of Informatics, Masaryk University, Botanick\u00e1 68a, 602 00, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Systems Biology Laboratory, Faculty of Informatics, Masaryk University, Botanick\u00e1 68a, 602 00, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Pastva", 
        "givenName": "Samuel", 
        "id": "sg:person.016130263073.10", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016130263073.10"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Systems Biology Laboratory, Faculty of Informatics, Masaryk University, Botanick\u00e1 68a, 602 00, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Systems Biology Laboratory, Faculty of Informatics, Masaryk University, Botanick\u00e1 68a, 602 00, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "\u0160afr\u00e1nek", 
        "givenName": "David", 
        "id": "sg:person.011410250615.43", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011410250615.43"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2016-09-22", 
    "datePublishedReg": "2016-09-22", 
    "description": "We propose a novel scalable parallel algorithm for synthesis of interdependent parameters from CTL specifications for non-linear dynamical systems. The method employs a symbolic representation of sets of parameter valuations in terms of the first-order theory of the reals. To demonstrate its practicability, we apply the method to a class of piecewise multi-affine dynamical systems representing dynamics of biological systems with complex non-linear behaviour.", 
    "editor": [
      {
        "familyName": "Artho", 
        "givenName": "Cyrille", 
        "type": "Person"
      }, 
      {
        "familyName": "Legay", 
        "givenName": "Axel", 
        "type": "Person"
      }, 
      {
        "familyName": "Peled", 
        "givenName": "Doron", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-46520-3_13", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-319-46519-7", 
        "978-3-319-46520-3"
      ], 
      "name": "Automated Technology for Verification and Analysis", 
      "type": "Book"
    }, 
    "keywords": [
      "dynamical systems", 
      "non-linear dynamical systems", 
      "multi-affine systems", 
      "novel scalable parallel algorithms", 
      "first-order theory", 
      "complex non-linear behaviour", 
      "parameter synthesis", 
      "scalable parallel algorithm", 
      "parallel algorithm", 
      "parameter valuations", 
      "non-linear behavior", 
      "interdependent parameters", 
      "biological systems", 
      "theory", 
      "system", 
      "algorithm", 
      "dynamics", 
      "symbolic representation", 
      "class", 
      "Real", 
      "CTL specifications", 
      "representation", 
      "parameters", 
      "set", 
      "terms", 
      "applications", 
      "practicability", 
      "behavior", 
      "specification", 
      "valuation", 
      "SMT", 
      "synthesis", 
      "method"
    ], 
    "name": "Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-affine Systems", 
    "pagination": "192-208", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1084843823"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-46520-3_13"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-46520-3_13", 
      "https://app.dimensions.ai/details/publication/pub.1084843823"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-10T10:49", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220509/entities/gbq_results/chapter/chapter_378.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-46520-3_13"
  }
]
 

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-46520-3_13'

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-46520-3_13'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-46520-3_13'

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-46520-3_13'


 

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

131 TRIPLES      23 PREDICATES      58 URIs      51 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-46520-3_13 schema:about anzsrc-for:01
2 anzsrc-for:0101
3 schema:author Ndc0d7072a9734b1888de4ff8da3e63e0
4 schema:datePublished 2016-09-22
5 schema:datePublishedReg 2016-09-22
6 schema:description We propose a novel scalable parallel algorithm for synthesis of interdependent parameters from CTL specifications for non-linear dynamical systems. The method employs a symbolic representation of sets of parameter valuations in terms of the first-order theory of the reals. To demonstrate its practicability, we apply the method to a class of piecewise multi-affine dynamical systems representing dynamics of biological systems with complex non-linear behaviour.
7 schema:editor Nc7feb9202d234358a7fcdcc7e807255c
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf Ncd7a91f2f942419fa01746e970bf9646
12 schema:keywords CTL specifications
13 Real
14 SMT
15 algorithm
16 applications
17 behavior
18 biological systems
19 class
20 complex non-linear behaviour
21 dynamical systems
22 dynamics
23 first-order theory
24 interdependent parameters
25 method
26 multi-affine systems
27 non-linear behavior
28 non-linear dynamical systems
29 novel scalable parallel algorithms
30 parallel algorithm
31 parameter synthesis
32 parameter valuations
33 parameters
34 practicability
35 representation
36 scalable parallel algorithm
37 set
38 specification
39 symbolic representation
40 synthesis
41 system
42 terms
43 theory
44 valuation
45 schema:name Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-affine Systems
46 schema:pagination 192-208
47 schema:productId N53a170dbc9344232abdf8e884c1d0788
48 N6e03f29b804047508e4e0def7ae3a4e0
49 schema:publisher Nce5ffd48b4eb4757a96899c85f05e662
50 schema:sameAs https://app.dimensions.ai/details/publication/pub.1084843823
51 https://doi.org/10.1007/978-3-319-46520-3_13
52 schema:sdDatePublished 2022-05-10T10:49
53 schema:sdLicense https://scigraph.springernature.com/explorer/license/
54 schema:sdPublisher N9b277323146a418b8c48f8de622aebab
55 schema:url https://doi.org/10.1007/978-3-319-46520-3_13
56 sgo:license sg:explorer/license/
57 sgo:sdDataset chapters
58 rdf:type schema:Chapter
59 N149773c17b7b4c49a05d37e8dd28cde0 rdf:first N1eeefb4913794534a48e5c06a2677179
60 rdf:rest N249ff4405e3f4044a2985afd118b1676
61 N1eeefb4913794534a48e5c06a2677179 schema:familyName Legay
62 schema:givenName Axel
63 rdf:type schema:Person
64 N249ff4405e3f4044a2985afd118b1676 rdf:first N27a1ff6f6a524ad7bee5a9b46fac748a
65 rdf:rest rdf:nil
66 N27a1ff6f6a524ad7bee5a9b46fac748a schema:familyName Peled
67 schema:givenName Doron
68 rdf:type schema:Person
69 N53a170dbc9344232abdf8e884c1d0788 schema:name dimensions_id
70 schema:value pub.1084843823
71 rdf:type schema:PropertyValue
72 N6e03f29b804047508e4e0def7ae3a4e0 schema:name doi
73 schema:value 10.1007/978-3-319-46520-3_13
74 rdf:type schema:PropertyValue
75 N6e564629f4904ff8b66e95b2bae5cd95 rdf:first sg:person.011410250615.43
76 rdf:rest rdf:nil
77 N8f5b406a1636478994689a93e3d6e93e rdf:first sg:person.0645117057.83
78 rdf:rest Nf685b9e128df48aeb52cb6d99e068add
79 N9b277323146a418b8c48f8de622aebab schema:name Springer Nature - SN SciGraph project
80 rdf:type schema:Organization
81 Nc7feb9202d234358a7fcdcc7e807255c rdf:first Ne1696de0b24e4b99876761c58a4e2da0
82 rdf:rest N149773c17b7b4c49a05d37e8dd28cde0
83 Ncd7a91f2f942419fa01746e970bf9646 schema:isbn 978-3-319-46519-7
84 978-3-319-46520-3
85 schema:name Automated Technology for Verification and Analysis
86 rdf:type schema:Book
87 Nce5ffd48b4eb4757a96899c85f05e662 schema:name Springer Nature
88 rdf:type schema:Organisation
89 Ndc0d7072a9734b1888de4ff8da3e63e0 rdf:first sg:person.014465763501.21
90 rdf:rest N8f5b406a1636478994689a93e3d6e93e
91 Ndcf541caaa144cd980f60e6732be1fb3 rdf:first sg:person.016130263073.10
92 rdf:rest N6e564629f4904ff8b66e95b2bae5cd95
93 Ne1696de0b24e4b99876761c58a4e2da0 schema:familyName Artho
94 schema:givenName Cyrille
95 rdf:type schema:Person
96 Nf685b9e128df48aeb52cb6d99e068add rdf:first sg:person.016566512611.71
97 rdf:rest Ndcf541caaa144cd980f60e6732be1fb3
98 anzsrc-for:01 schema:inDefinedTermSet anzsrc-for:
99 schema:name Mathematical Sciences
100 rdf:type schema:DefinedTerm
101 anzsrc-for:0101 schema:inDefinedTermSet anzsrc-for:
102 schema:name Pure Mathematics
103 rdf:type schema:DefinedTerm
104 sg:person.011410250615.43 schema:affiliation grid-institutes:grid.10267.32
105 schema:familyName Šafránek
106 schema:givenName David
107 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011410250615.43
108 rdf:type schema:Person
109 sg:person.014465763501.21 schema:affiliation grid-institutes:grid.10267.32
110 schema:familyName Beneš
111 schema:givenName Nikola
112 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014465763501.21
113 rdf:type schema:Person
114 sg:person.016130263073.10 schema:affiliation grid-institutes:grid.10267.32
115 schema:familyName Pastva
116 schema:givenName Samuel
117 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016130263073.10
118 rdf:type schema:Person
119 sg:person.016566512611.71 schema:affiliation grid-institutes:grid.10267.32
120 schema:familyName Demko
121 schema:givenName Martin
122 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016566512611.71
123 rdf:type schema:Person
124 sg:person.0645117057.83 schema:affiliation grid-institutes:grid.10267.32
125 schema:familyName Brim
126 schema:givenName Luboš
127 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0645117057.83
128 rdf:type schema:Person
129 grid-institutes:grid.10267.32 schema:alternateName Systems Biology Laboratory, Faculty of Informatics, Masaryk University, Botanická 68a, 602 00, Brno, Czech Republic
130 schema:name Systems Biology Laboratory, Faculty of Informatics, Masaryk University, Botanická 68a, 602 00, Brno, Czech Republic
131 rdf:type schema:Organization
 




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


...