PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2016-04-09

AUTHORS

Milan Češka , Petr Pilař , Nicola Paoletti , Luboš Brim , Marta Kwiatkowska

ABSTRACT

In this paper we present PRISM-PSY, a novel tool that performs precise GPU-accelerated parameter synthesis for continuous-time Markov chains and time-bounded temporal logic specifications. We redesign, in terms of matrix-vector operations, the recently formulated algorithms for precise parameter synthesis in order to enable effective data-parallel processing, which results in significant acceleration on many-core architectures. High hardware utilisation, essential for performance and scalability, is achieved by state space and parameter space parallelisation: the former leverages a compact sparse-matrix representation, and the latter is based on an iterative decomposition of the parameter space. Our experiments on several biological and engineering case studies demonstrate an overall speedup of up to 31-fold on a single GPU compared to the sequential implementation. More... »

PAGES

367-384

Book

TITLE

Tools and Algorithms for the Construction and Analysis of Systems

ISBN

978-3-662-49673-2
978-3-662-49674-9

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-662-49674-9_21

DOI

http://dx.doi.org/10.1007/978-3-662-49674-9_21

DIMENSIONS

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


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/0803", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computer Software", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "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": "\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": "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": "Pila\u0159", 
        "givenName": "Petr", 
        "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": "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": "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": "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"
      }
    ], 
    "datePublished": "2016-04-09", 
    "datePublishedReg": "2016-04-09", 
    "description": "In this paper we present PRISM-PSY, a novel tool that performs precise GPU-accelerated parameter synthesis for continuous-time Markov chains and time-bounded temporal logic specifications. We redesign, in terms of matrix-vector operations, the recently formulated algorithms for precise parameter synthesis in order to enable effective data-parallel processing, which results in significant acceleration on many-core architectures. High hardware utilisation, essential for performance and scalability, is achieved by state space and parameter space parallelisation: the former leverages a compact sparse-matrix representation, and the latter is based on an iterative decomposition of the parameter space. Our experiments on several biological and engineering case studies demonstrate an overall speedup of up\u00a0to 31-fold on a single GPU compared to the sequential implementation.", 
    "editor": [
      {
        "familyName": "Chechik", 
        "givenName": "Marsha", 
        "type": "Person"
      }, 
      {
        "familyName": "Raskin", 
        "givenName": "Jean-Fran\u00e7ois", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-662-49674-9_21", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-662-49673-2", 
        "978-3-662-49674-9"
      ], 
      "name": "Tools and Algorithms for the Construction and Analysis of Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "engineering case study", 
      "Precise Parameter Synthesis", 
      "parameter synthesis", 
      "former leverages", 
      "iterative decomposition", 
      "acceleration", 
      "operation", 
      "data-parallel processing", 
      "hardware utilisation", 
      "matrix-vector operations", 
      "performance", 
      "processing", 
      "case study", 
      "significant acceleration", 
      "parameter space", 
      "sparse-matrix representation", 
      "decomposition", 
      "experiments", 
      "GPU", 
      "system", 
      "order", 
      "specification", 
      "utilisation", 
      "space", 
      "algorithm", 
      "parallelisation", 
      "synthesis", 
      "state space", 
      "sequential implementation", 
      "implementation", 
      "terms", 
      "architecture", 
      "latter", 
      "tool", 
      "stochastic systems", 
      "scalability", 
      "novel tool", 
      "overall speedup", 
      "single GPU", 
      "core architectures", 
      "temporal logic specifications", 
      "study", 
      "chain", 
      "representation", 
      "logic specifications", 
      "speedup", 
      "Markov chain", 
      "continuous-time Markov chain", 
      "leverage", 
      "paper", 
      "PRISM-PSY", 
      "precise GPU", 
      "time-bounded temporal logic specifications", 
      "effective data-parallel processing", 
      "High hardware utilisation", 
      "parameter space parallelisation", 
      "space parallelisation", 
      "compact sparse-matrix representation", 
      "Precise GPU-Accelerated Parameter Synthesis", 
      "GPU-Accelerated Parameter Synthesis"
    ], 
    "name": "PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems", 
    "pagination": "367-384", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1045143257"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-662-49674-9_21"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-662-49674-9_21", 
      "https://app.dimensions.ai/details/publication/pub.1045143257"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-12-01T20:12", 
    "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_90.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-662-49674-9_21"
  }
]
 

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-662-49674-9_21'

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-662-49674-9_21'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-662-49674-9_21'

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-662-49674-9_21'


 

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

155 TRIPLES      23 PREDICATES      85 URIs      78 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-662-49674-9_21 schema:about anzsrc-for:08
2 anzsrc-for:0803
3 schema:author N7d4a5a72ef294dca90b3992f2600f3a5
4 schema:datePublished 2016-04-09
5 schema:datePublishedReg 2016-04-09
6 schema:description In this paper we present PRISM-PSY, a novel tool that performs precise GPU-accelerated parameter synthesis for continuous-time Markov chains and time-bounded temporal logic specifications. We redesign, in terms of matrix-vector operations, the recently formulated algorithms for precise parameter synthesis in order to enable effective data-parallel processing, which results in significant acceleration on many-core architectures. High hardware utilisation, essential for performance and scalability, is achieved by state space and parameter space parallelisation: the former leverages a compact sparse-matrix representation, and the latter is based on an iterative decomposition of the parameter space. Our experiments on several biological and engineering case studies demonstrate an overall speedup of up to 31-fold on a single GPU compared to the sequential implementation.
7 schema:editor N9cd259aa105e4cf0b0df7c25c73bb472
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf Nc43f6ff14a1a448dbba490c8a5d61b79
12 schema:keywords GPU
13 GPU-Accelerated Parameter Synthesis
14 High hardware utilisation
15 Markov chain
16 PRISM-PSY
17 Precise GPU-Accelerated Parameter Synthesis
18 Precise Parameter Synthesis
19 acceleration
20 algorithm
21 architecture
22 case study
23 chain
24 compact sparse-matrix representation
25 continuous-time Markov chain
26 core architectures
27 data-parallel processing
28 decomposition
29 effective data-parallel processing
30 engineering case study
31 experiments
32 former leverages
33 hardware utilisation
34 implementation
35 iterative decomposition
36 latter
37 leverage
38 logic specifications
39 matrix-vector operations
40 novel tool
41 operation
42 order
43 overall speedup
44 paper
45 parallelisation
46 parameter space
47 parameter space parallelisation
48 parameter synthesis
49 performance
50 precise GPU
51 processing
52 representation
53 scalability
54 sequential implementation
55 significant acceleration
56 single GPU
57 space
58 space parallelisation
59 sparse-matrix representation
60 specification
61 speedup
62 state space
63 stochastic systems
64 study
65 synthesis
66 system
67 temporal logic specifications
68 terms
69 time-bounded temporal logic specifications
70 tool
71 utilisation
72 schema:name PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems
73 schema:pagination 367-384
74 schema:productId N0d62425fcc8d4063b538ddc7df802e8c
75 Nd088a28a236e4fd5857507ad0879527e
76 schema:publisher Nc53bb1acb7474e32ac2685849a01eb89
77 schema:sameAs https://app.dimensions.ai/details/publication/pub.1045143257
78 https://doi.org/10.1007/978-3-662-49674-9_21
79 schema:sdDatePublished 2021-12-01T20:12
80 schema:sdLicense https://scigraph.springernature.com/explorer/license/
81 schema:sdPublisher Nd4b25369f8024cd1b44edf9dc53876ff
82 schema:url https://doi.org/10.1007/978-3-662-49674-9_21
83 sgo:license sg:explorer/license/
84 sgo:sdDataset chapters
85 rdf:type schema:Chapter
86 N0d62425fcc8d4063b538ddc7df802e8c schema:name doi
87 schema:value 10.1007/978-3-662-49674-9_21
88 rdf:type schema:PropertyValue
89 N6361cbe8c1f14c8ab68e4959e40a6849 rdf:first sg:person.011375012273.39
90 rdf:rest rdf:nil
91 N7d4a5a72ef294dca90b3992f2600f3a5 rdf:first sg:person.016652663056.36
92 rdf:rest Na2c8a26745fc4847a84138ad1dbfb6f0
93 N9cd259aa105e4cf0b0df7c25c73bb472 rdf:first Neaa8fb7a249747e6b0acda6aeb9dba66
94 rdf:rest Na9f996c6883546df8e33706414916d0c
95 Na2c8a26745fc4847a84138ad1dbfb6f0 rdf:first Ne27e58b6264748618d561113e7244ccf
96 rdf:rest Nb70bc3e96f7a4544a4d58ba2d8138d14
97 Na99ad61539a544d79e1e65cfeb9e6695 rdf:first sg:person.0645117057.83
98 rdf:rest N6361cbe8c1f14c8ab68e4959e40a6849
99 Na9f996c6883546df8e33706414916d0c rdf:first Ndd483938e63348dc839f50dff462abf7
100 rdf:rest rdf:nil
101 Nb70bc3e96f7a4544a4d58ba2d8138d14 rdf:first sg:person.014036566653.01
102 rdf:rest Na99ad61539a544d79e1e65cfeb9e6695
103 Nc43f6ff14a1a448dbba490c8a5d61b79 schema:isbn 978-3-662-49673-2
104 978-3-662-49674-9
105 schema:name Tools and Algorithms for the Construction and Analysis of Systems
106 rdf:type schema:Book
107 Nc53bb1acb7474e32ac2685849a01eb89 schema:name Springer Nature
108 rdf:type schema:Organisation
109 Nd088a28a236e4fd5857507ad0879527e schema:name dimensions_id
110 schema:value pub.1045143257
111 rdf:type schema:PropertyValue
112 Nd4b25369f8024cd1b44edf9dc53876ff schema:name Springer Nature - SN SciGraph project
113 rdf:type schema:Organization
114 Ndd483938e63348dc839f50dff462abf7 schema:familyName Raskin
115 schema:givenName Jean-François
116 rdf:type schema:Person
117 Ne27e58b6264748618d561113e7244ccf schema:affiliation grid-institutes:grid.10267.32
118 schema:familyName Pilař
119 schema:givenName Petr
120 rdf:type schema:Person
121 Neaa8fb7a249747e6b0acda6aeb9dba66 schema:familyName Chechik
122 schema:givenName Marsha
123 rdf:type schema:Person
124 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
125 schema:name Information and Computing Sciences
126 rdf:type schema:DefinedTerm
127 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
128 schema:name Computer Software
129 rdf:type schema:DefinedTerm
130 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
131 schema:familyName Kwiatkowska
132 schema:givenName Marta
133 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
134 rdf:type schema:Person
135 sg:person.014036566653.01 schema:affiliation grid-institutes:grid.4991.5
136 schema:familyName Paoletti
137 schema:givenName Nicola
138 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014036566653.01
139 rdf:type schema:Person
140 sg:person.016652663056.36 schema:affiliation grid-institutes:grid.4991.5
141 schema:familyName Češka
142 schema:givenName Milan
143 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016652663056.36
144 rdf:type schema:Person
145 sg:person.0645117057.83 schema:affiliation grid-institutes:grid.10267.32
146 schema:familyName Brim
147 schema:givenName Luboš
148 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0645117057.83
149 rdf:type schema:Person
150 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
151 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
152 rdf:type schema:Organization
153 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, Oxford, UK
154 schema:name Department of Computer Science, University of Oxford, Oxford, UK
155 rdf:type schema:Organization
 




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


...