Parameter Synthesis for Probabilistic Timed Automata Using Stochastic Game Abstractions View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2014

AUTHORS

Aleksandra Jovanović , Marta Kwiatkowska

ABSTRACT

We propose a method to synthesise optimal values of timing parameters for probabilistic timed automata, in the sense that the probability of reaching some set of states is either maximised or minimised. Our first algorithm, based on forward exploration of the symbolic states, can only guarantee parameter values that correspond to upper (resp. lower) bounds on maximum (resp. minimum) reachability probability. To ensure precise reachability probabilities, we adapt the game-based abstraction refinement method. In the parametric setting, our method is able to determine all the possible maximum (or minimum) reachability probabilities that arise for different values of timing parameters, and yields optimal valuations represented as a set of symbolic constraints between parameters. More... »

PAGES

176-189

Book

TITLE

Reachability Problems

ISBN

978-3-319-11438-5
978-3-319-11439-2

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-11439-2_14

DOI

http://dx.doi.org/10.1007/978-3-319-11439-2_14

DIMENSIONS

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


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/0104", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Statistics", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, OX1 3QD, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, OX1 3QD, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Jovanovi\u0107", 
        "givenName": "Aleksandra", 
        "id": "sg:person.010047304050.07", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010047304050.07"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, OX1 3QD, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, OX1 3QD, 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": "2014", 
    "datePublishedReg": "2014-01-01", 
    "description": "We propose a method to synthesise optimal values of timing parameters for probabilistic timed automata, in the sense that the probability of reaching some set of states is either maximised or minimised. Our first algorithm, based on forward exploration of the symbolic states, can only guarantee parameter values that correspond to upper (resp. lower) bounds on maximum (resp. minimum) reachability probability. To ensure precise reachability probabilities, we adapt the game-based abstraction refinement method. In the parametric setting, our method is able to determine all the possible maximum (or minimum) reachability probabilities that arise for different values of timing parameters, and yields optimal valuations represented as a set of symbolic constraints between parameters.", 
    "editor": [
      {
        "familyName": "Ouaknine", 
        "givenName": "Jo\u00ebl", 
        "type": "Person"
      }, 
      {
        "familyName": "Potapov", 
        "givenName": "Igor", 
        "type": "Person"
      }, 
      {
        "familyName": "Worrell", 
        "givenName": "James", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-11439-2_14", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-319-11438-5", 
        "978-3-319-11439-2"
      ], 
      "name": "Reachability Problems", 
      "type": "Book"
    }, 
    "keywords": [
      "reachability probabilities", 
      "set of states", 
      "optimal value", 
      "upper bounds", 
      "parametric settings", 
      "parameter synthesis", 
      "first algorithm", 
      "parameter values", 
      "optimal valuation", 
      "timing parameters", 
      "probability", 
      "forward exploration", 
      "refinement method", 
      "symbolic constraints", 
      "parameters", 
      "automata", 
      "set", 
      "symbolic states", 
      "bounds", 
      "reachability", 
      "different values", 
      "algorithm", 
      "valuation", 
      "constraints", 
      "Probabilistic Timed Automata", 
      "Timed Automata", 
      "sense", 
      "values", 
      "state", 
      "abstraction", 
      "setting", 
      "method", 
      "exploration", 
      "synthesis", 
      "maximum (resp. minimum) reachability probability", 
      "precise reachability probabilities", 
      "game-based abstraction refinement method", 
      "abstraction refinement method", 
      "possible maximum (or minimum) reachability", 
      "maximum reachability", 
      "Stochastic Game Abstractions", 
      "Game Abstractions"
    ], 
    "name": "Parameter Synthesis for Probabilistic Timed Automata Using Stochastic Game Abstractions", 
    "pagination": "176-189", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1042124042"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-11439-2_14"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-11439-2_14", 
      "https://app.dimensions.ai/details/publication/pub.1042124042"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-11-01T18:54", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20211101/entities/gbq_results/chapter/chapter_287.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-11439-2_14"
  }
]
 

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-11439-2_14'

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-11439-2_14'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-11439-2_14'

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-11439-2_14'


 

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

119 TRIPLES      23 PREDICATES      68 URIs      61 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-11439-2_14 schema:about anzsrc-for:01
2 anzsrc-for:0104
3 schema:author N601a480204304cf29aa837cd7e4be3e7
4 schema:datePublished 2014
5 schema:datePublishedReg 2014-01-01
6 schema:description We propose a method to synthesise optimal values of timing parameters for probabilistic timed automata, in the sense that the probability of reaching some set of states is either maximised or minimised. Our first algorithm, based on forward exploration of the symbolic states, can only guarantee parameter values that correspond to upper (resp. lower) bounds on maximum (resp. minimum) reachability probability. To ensure precise reachability probabilities, we adapt the game-based abstraction refinement method. In the parametric setting, our method is able to determine all the possible maximum (or minimum) reachability probabilities that arise for different values of timing parameters, and yields optimal valuations represented as a set of symbolic constraints between parameters.
7 schema:editor N1f4bd63374494cb3a0f26d27c39bb8dd
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf Nfd72635f853847419eb57f01cf962a92
12 schema:keywords Game Abstractions
13 Probabilistic Timed Automata
14 Stochastic Game Abstractions
15 Timed Automata
16 abstraction
17 abstraction refinement method
18 algorithm
19 automata
20 bounds
21 constraints
22 different values
23 exploration
24 first algorithm
25 forward exploration
26 game-based abstraction refinement method
27 maximum (resp. minimum) reachability probability
28 maximum reachability
29 method
30 optimal valuation
31 optimal value
32 parameter synthesis
33 parameter values
34 parameters
35 parametric settings
36 possible maximum (or minimum) reachability
37 precise reachability probabilities
38 probability
39 reachability
40 reachability probabilities
41 refinement method
42 sense
43 set
44 set of states
45 setting
46 state
47 symbolic constraints
48 symbolic states
49 synthesis
50 timing parameters
51 upper bounds
52 valuation
53 values
54 schema:name Parameter Synthesis for Probabilistic Timed Automata Using Stochastic Game Abstractions
55 schema:pagination 176-189
56 schema:productId N2777fc4073b7428b8a506faff8d35544
57 N92e1332ddb8d44e28daac6755a232361
58 schema:publisher N70facff665a641ab81e87b7778f16529
59 schema:sameAs https://app.dimensions.ai/details/publication/pub.1042124042
60 https://doi.org/10.1007/978-3-319-11439-2_14
61 schema:sdDatePublished 2021-11-01T18:54
62 schema:sdLicense https://scigraph.springernature.com/explorer/license/
63 schema:sdPublisher N02d6efb77751425b8de91a2674b7bc44
64 schema:url https://doi.org/10.1007/978-3-319-11439-2_14
65 sgo:license sg:explorer/license/
66 sgo:sdDataset chapters
67 rdf:type schema:Chapter
68 N02d6efb77751425b8de91a2674b7bc44 schema:name Springer Nature - SN SciGraph project
69 rdf:type schema:Organization
70 N1f4bd63374494cb3a0f26d27c39bb8dd rdf:first Ne5a774f830ef4322b66f3ebbf1ee495f
71 rdf:rest Ne670fab0ce0e432da6117fa544a26085
72 N2777fc4073b7428b8a506faff8d35544 schema:name doi
73 schema:value 10.1007/978-3-319-11439-2_14
74 rdf:type schema:PropertyValue
75 N3a7679200df844b4836fbafcfe0bb361 schema:familyName Worrell
76 schema:givenName James
77 rdf:type schema:Person
78 N5ae91b700f1e4980aa829a941b6e43dd schema:familyName Potapov
79 schema:givenName Igor
80 rdf:type schema:Person
81 N601a480204304cf29aa837cd7e4be3e7 rdf:first sg:person.010047304050.07
82 rdf:rest Ne297d556c70745a9a958ecb150178d67
83 N70facff665a641ab81e87b7778f16529 schema:name Springer Nature
84 rdf:type schema:Organisation
85 N92e1332ddb8d44e28daac6755a232361 schema:name dimensions_id
86 schema:value pub.1042124042
87 rdf:type schema:PropertyValue
88 Ne297d556c70745a9a958ecb150178d67 rdf:first sg:person.011375012273.39
89 rdf:rest rdf:nil
90 Ne5a774f830ef4322b66f3ebbf1ee495f schema:familyName Ouaknine
91 schema:givenName Joël
92 rdf:type schema:Person
93 Ne670fab0ce0e432da6117fa544a26085 rdf:first N5ae91b700f1e4980aa829a941b6e43dd
94 rdf:rest Nfb76fbfaee7d46ce9b436120f8bcbda8
95 Nfb76fbfaee7d46ce9b436120f8bcbda8 rdf:first N3a7679200df844b4836fbafcfe0bb361
96 rdf:rest rdf:nil
97 Nfd72635f853847419eb57f01cf962a92 schema:isbn 978-3-319-11438-5
98 978-3-319-11439-2
99 schema:name Reachability Problems
100 rdf:type schema:Book
101 anzsrc-for:01 schema:inDefinedTermSet anzsrc-for:
102 schema:name Mathematical Sciences
103 rdf:type schema:DefinedTerm
104 anzsrc-for:0104 schema:inDefinedTermSet anzsrc-for:
105 schema:name Statistics
106 rdf:type schema:DefinedTerm
107 sg:person.010047304050.07 schema:affiliation grid-institutes:grid.4991.5
108 schema:familyName Jovanović
109 schema:givenName Aleksandra
110 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010047304050.07
111 rdf:type schema:Person
112 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
113 schema:familyName Kwiatkowska
114 schema:givenName Marta
115 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
116 rdf:type schema:Person
117 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, OX1 3QD, Oxford, UK
118 schema:name Department of Computer Science, University of Oxford, OX1 3QD, Oxford, UK
119 rdf:type schema:Organization
 




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


...