Accelerating Parameter Synthesis Using Semi-algebraic Constraints View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2019-11-22

AUTHORS

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

ABSTRACT

We propose a novel approach to parameter synthesis for parametrised Kripke structures and CTL specifications. In our method, we suppose the parametrisations form a semi-algebraic set and we utilise a symbolic representation using the so-called cylindrical algebraic decomposition of corresponding multivariate polynomials. Specifically, we propose a new data structure allowing to compute and efficiently manipulate such representations. The new method is significantly faster than our previous method based on SMT. We apply the method to a set of rational dynamical systems representing complex biological mechanisms with non-linear behaviour. More... »

PAGES

27-45

Book

TITLE

Integrated Formal Methods

ISBN

978-3-030-34967-7
978-3-030-34968-4

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-030-34968-4_2

DOI

http://dx.doi.org/10.1007/978-3-030-34968-4_2

DIMENSIONS

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


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": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, 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": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, 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": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Geletka", 
        "givenName": "Martin", 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, 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": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, 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": "2019-11-22", 
    "datePublishedReg": "2019-11-22", 
    "description": "We propose a novel approach to parameter synthesis for parametrised Kripke structures and CTL specifications. In our method, we suppose the parametrisations form a semi-algebraic set and we utilise a symbolic representation using the so-called cylindrical algebraic decomposition of corresponding multivariate polynomials. Specifically, we propose a new data structure allowing to compute and efficiently manipulate such representations. The new method is significantly faster than our previous method based on SMT. We apply the method to a set of rational dynamical systems representing complex biological mechanisms with non-linear behaviour.", 
    "editor": [
      {
        "familyName": "Ahrendt", 
        "givenName": "Wolfgang", 
        "type": "Person"
      }, 
      {
        "familyName": "Tapia Tarifa", 
        "givenName": "Silvia Lizeth", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-030-34968-4_2", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-030-34967-7", 
        "978-3-030-34968-4"
      ], 
      "name": "Integrated Formal Methods", 
      "type": "Book"
    }, 
    "keywords": [
      "parameter synthesis", 
      "rational dynamical systems", 
      "cylindrical algebraic decomposition", 
      "semi-algebraic constraints", 
      "semi-algebraic sets", 
      "dynamical systems", 
      "algebraic decomposition", 
      "multivariate polynomials", 
      "non-linear behavior", 
      "such representations", 
      "previous methods", 
      "new data structure", 
      "data structure", 
      "new method", 
      "polynomials", 
      "complex biological mechanisms", 
      "representation", 
      "parametrisation", 
      "set", 
      "Kripke structures", 
      "constraints", 
      "symbolic representation", 
      "novel approach", 
      "CTL specifications", 
      "structure", 
      "decomposition", 
      "approach", 
      "system", 
      "behavior", 
      "specification", 
      "SMT", 
      "synthesis", 
      "biological mechanisms", 
      "mechanism", 
      "method"
    ], 
    "name": "Accelerating Parameter Synthesis Using Semi-algebraic Constraints", 
    "pagination": "27-45", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1122795170"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-030-34968-4_2"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-030-34968-4_2", 
      "https://app.dimensions.ai/details/publication/pub.1122795170"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-10T10:41", 
    "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_197.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-030-34968-4_2"
  }
]
 

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-030-34968-4_2'

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-030-34968-4_2'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-030-34968-4_2'

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-030-34968-4_2'


 

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

127 TRIPLES      23 PREDICATES      60 URIs      53 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-030-34968-4_2 schema:about anzsrc-for:01
2 anzsrc-for:0101
3 schema:author N103ba3c4c48042ae854de8f16696bfe3
4 schema:datePublished 2019-11-22
5 schema:datePublishedReg 2019-11-22
6 schema:description We propose a novel approach to parameter synthesis for parametrised Kripke structures and CTL specifications. In our method, we suppose the parametrisations form a semi-algebraic set and we utilise a symbolic representation using the so-called cylindrical algebraic decomposition of corresponding multivariate polynomials. Specifically, we propose a new data structure allowing to compute and efficiently manipulate such representations. The new method is significantly faster than our previous method based on SMT. We apply the method to a set of rational dynamical systems representing complex biological mechanisms with non-linear behaviour.
7 schema:editor Nc1227e413ce7466293ad19d042a2471f
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf N7bfb0a8241444e77afcd58b0e9c15486
12 schema:keywords CTL specifications
13 Kripke structures
14 SMT
15 algebraic decomposition
16 approach
17 behavior
18 biological mechanisms
19 complex biological mechanisms
20 constraints
21 cylindrical algebraic decomposition
22 data structure
23 decomposition
24 dynamical systems
25 mechanism
26 method
27 multivariate polynomials
28 new data structure
29 new method
30 non-linear behavior
31 novel approach
32 parameter synthesis
33 parametrisation
34 polynomials
35 previous methods
36 rational dynamical systems
37 representation
38 semi-algebraic constraints
39 semi-algebraic sets
40 set
41 specification
42 structure
43 such representations
44 symbolic representation
45 synthesis
46 system
47 schema:name Accelerating Parameter Synthesis Using Semi-algebraic Constraints
48 schema:pagination 27-45
49 schema:productId N906b6f581126458bbe7269298a6ec58f
50 Na6c927948d0e4d2091c462acb7754729
51 schema:publisher Nbc8034e90a3242c49b919178c6312f0f
52 schema:sameAs https://app.dimensions.ai/details/publication/pub.1122795170
53 https://doi.org/10.1007/978-3-030-34968-4_2
54 schema:sdDatePublished 2022-05-10T10:41
55 schema:sdLicense https://scigraph.springernature.com/explorer/license/
56 schema:sdPublisher N20a4024ea6a3443ea3d656c4540f897e
57 schema:url https://doi.org/10.1007/978-3-030-34968-4_2
58 sgo:license sg:explorer/license/
59 sgo:sdDataset chapters
60 rdf:type schema:Chapter
61 N103ba3c4c48042ae854de8f16696bfe3 rdf:first sg:person.014465763501.21
62 rdf:rest Nf5f3084908634789ae7169b981385741
63 N20a4024ea6a3443ea3d656c4540f897e schema:name Springer Nature - SN SciGraph project
64 rdf:type schema:Organization
65 N41d67c7ba8e04d4480f7c7ca8693a75e schema:familyName Tapia Tarifa
66 schema:givenName Silvia Lizeth
67 rdf:type schema:Person
68 N4e93ceda0e2949d6aef013130b13e7aa rdf:first sg:person.016130263073.10
69 rdf:rest N82e466568a284d289207e173c4df655d
70 N72c5fa5492b54ae5a811e1e9f1ce89da rdf:first N41d67c7ba8e04d4480f7c7ca8693a75e
71 rdf:rest rdf:nil
72 N7bfb0a8241444e77afcd58b0e9c15486 schema:isbn 978-3-030-34967-7
73 978-3-030-34968-4
74 schema:name Integrated Formal Methods
75 rdf:type schema:Book
76 N82e466568a284d289207e173c4df655d rdf:first sg:person.011410250615.43
77 rdf:rest rdf:nil
78 N906b6f581126458bbe7269298a6ec58f schema:name doi
79 schema:value 10.1007/978-3-030-34968-4_2
80 rdf:type schema:PropertyValue
81 Na6c927948d0e4d2091c462acb7754729 schema:name dimensions_id
82 schema:value pub.1122795170
83 rdf:type schema:PropertyValue
84 Nbc8034e90a3242c49b919178c6312f0f schema:name Springer Nature
85 rdf:type schema:Organisation
86 Nbd31e754a7114ba590081519b5c568f0 schema:affiliation grid-institutes:grid.10267.32
87 schema:familyName Geletka
88 schema:givenName Martin
89 rdf:type schema:Person
90 Nc1227e413ce7466293ad19d042a2471f rdf:first Nd8bf1de93d30427f816002d93c0625e7
91 rdf:rest N72c5fa5492b54ae5a811e1e9f1ce89da
92 Nce020c3981ce4fa599e98bd363f6629d rdf:first Nbd31e754a7114ba590081519b5c568f0
93 rdf:rest N4e93ceda0e2949d6aef013130b13e7aa
94 Nd8bf1de93d30427f816002d93c0625e7 schema:familyName Ahrendt
95 schema:givenName Wolfgang
96 rdf:type schema:Person
97 Nf5f3084908634789ae7169b981385741 rdf:first sg:person.0645117057.83
98 rdf:rest Nce020c3981ce4fa599e98bd363f6629d
99 anzsrc-for:01 schema:inDefinedTermSet anzsrc-for:
100 schema:name Mathematical Sciences
101 rdf:type schema:DefinedTerm
102 anzsrc-for:0101 schema:inDefinedTermSet anzsrc-for:
103 schema:name Pure Mathematics
104 rdf:type schema:DefinedTerm
105 sg:person.011410250615.43 schema:affiliation grid-institutes:grid.10267.32
106 schema:familyName Šafránek
107 schema:givenName David
108 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011410250615.43
109 rdf:type schema:Person
110 sg:person.014465763501.21 schema:affiliation grid-institutes:grid.10267.32
111 schema:familyName Beneš
112 schema:givenName Nikola
113 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014465763501.21
114 rdf:type schema:Person
115 sg:person.016130263073.10 schema:affiliation grid-institutes:grid.10267.32
116 schema:familyName Pastva
117 schema:givenName Samuel
118 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016130263073.10
119 rdf:type schema:Person
120 sg:person.0645117057.83 schema:affiliation grid-institutes:grid.10267.32
121 schema:familyName Brim
122 schema:givenName Luboš
123 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0645117057.83
124 rdf:type schema:Person
125 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
126 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
127 rdf:type schema:Organization
 




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


...