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": "2022-01-01T19:28", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220101/entities/gbq_results/chapter/chapter_94.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 N8b920c317a41435c9be9bd5b022f319d
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 N81e43ae1c6be4fe0b0f510832c12a414
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf N0c40e071d7954e5abbaeedb76067d5e0
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 Na079547cabd049bb96d6e6a8dd716a9b
75 Nc42f3d5b6eb247469bd4a8d5555a9d55
76 schema:publisher N0333486e692445e08b39e66be0cbbfe6
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 2022-01-01T19:28
80 schema:sdLicense https://scigraph.springernature.com/explorer/license/
81 schema:sdPublisher N82b1c7b10d474092afc2a25f650ba9d6
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 N022080936cf24cf0b0ee963b761aa680 rdf:first sg:person.011375012273.39
87 rdf:rest rdf:nil
88 N0333486e692445e08b39e66be0cbbfe6 schema:name Springer Nature
89 rdf:type schema:Organisation
90 N0c40e071d7954e5abbaeedb76067d5e0 schema:isbn 978-3-662-49673-2
91 978-3-662-49674-9
92 schema:name Tools and Algorithms for the Construction and Analysis of Systems
93 rdf:type schema:Book
94 N0dc71c7b1a674ea0869ce0edea26e354 rdf:first N855e4a5c9e8e44cabff2b7d1224d0ff4
95 rdf:rest rdf:nil
96 N374c5132d58049d6a13d84677a664993 rdf:first sg:person.0645117057.83
97 rdf:rest N022080936cf24cf0b0ee963b761aa680
98 N448f1e7bf3784fdd86b76b61d9d2ca94 schema:affiliation grid-institutes:grid.10267.32
99 schema:familyName Pilař
100 schema:givenName Petr
101 rdf:type schema:Person
102 N81e43ae1c6be4fe0b0f510832c12a414 rdf:first N9631403384324c51b801aafd67e9d553
103 rdf:rest N0dc71c7b1a674ea0869ce0edea26e354
104 N82b1c7b10d474092afc2a25f650ba9d6 schema:name Springer Nature - SN SciGraph project
105 rdf:type schema:Organization
106 N855e4a5c9e8e44cabff2b7d1224d0ff4 schema:familyName Raskin
107 schema:givenName Jean-François
108 rdf:type schema:Person
109 N8b920c317a41435c9be9bd5b022f319d rdf:first sg:person.016652663056.36
110 rdf:rest Neba84f995ac54a7fbc1dca8440725436
111 N9631403384324c51b801aafd67e9d553 schema:familyName Chechik
112 schema:givenName Marsha
113 rdf:type schema:Person
114 Na079547cabd049bb96d6e6a8dd716a9b schema:name dimensions_id
115 schema:value pub.1045143257
116 rdf:type schema:PropertyValue
117 Nc42f3d5b6eb247469bd4a8d5555a9d55 schema:name doi
118 schema:value 10.1007/978-3-662-49674-9_21
119 rdf:type schema:PropertyValue
120 Neba84f995ac54a7fbc1dca8440725436 rdf:first N448f1e7bf3784fdd86b76b61d9d2ca94
121 rdf:rest Nfb7a705cb2b143e9a163d079598466f2
122 Nfb7a705cb2b143e9a163d079598466f2 rdf:first sg:person.014036566653.01
123 rdf:rest N374c5132d58049d6a13d84677a664993
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)


...