Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2017-07-25

AUTHORS

Marta Kwiatkowska , Gethin Norman , David Parker

ABSTRACT

Probabilistic timed automata are a formalism for modelling systems whose dynamics includes probabilistic, nondeterministic and timed aspects including real-time systems. A variety of techniques have been proposed for the analysis of this formalism and successfully employed to analyse, for example, wireless communication protocols and computer security systems. Augmenting the model with prices (or, equivalently, costs or rewards) provides a means to verify more complex quantitative properties, such as the expected energy usage of a device or the expected number of messages sent during a protocol’s execution. However, the analysis of these properties on probabilistic timed automata currently relies on a technique based on integer discretisation of real-valued clocks, which can be expensive in some cases. In this paper, we propose symbolic techniques for verification and optimal strategy synthesis for priced probabilistic timed automata which avoid this discretisation. We build upon recent work for the special case of expected time properties, using value iteration over a zone-based abstraction of the model. More... »

PAGES

289-309

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-63121-9_15

DOI

http://dx.doi.org/10.1007/978-3-319-63121-9_15

DIMENSIONS

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


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/0802", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computation Theory and Mathematics", 
        "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": "Kwiatkowska", 
        "givenName": "Marta", 
        "id": "sg:person.011375012273.39", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "School of Computing Science, University of Glasgow, Glasgow, UK", 
          "id": "http://www.grid.ac/institutes/grid.8756.c", 
          "name": [
            "School of Computing Science, University of Glasgow, Glasgow, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Norman", 
        "givenName": "Gethin", 
        "id": "sg:person.016323171577.36", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "School of Computer Science, University of Birmingham, Birmingham, UK", 
          "id": "http://www.grid.ac/institutes/grid.6572.6", 
          "name": [
            "School of Computer Science, University of Birmingham, Birmingham, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Parker", 
        "givenName": "David", 
        "id": "sg:person.014007552600.37", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2017-07-25", 
    "datePublishedReg": "2017-07-25", 
    "description": "Probabilistic timed automata are a formalism for modelling systems whose dynamics includes probabilistic, nondeterministic and timed aspects including real-time systems. A variety of techniques have been proposed for the analysis of this formalism and successfully employed to analyse, for example, wireless communication protocols and computer security systems. Augmenting the model with prices (or, equivalently, costs or rewards) provides a means to verify more complex quantitative properties, such as the expected energy usage of a device or the expected number of messages sent during a protocol\u2019s execution. However, the analysis of these properties on probabilistic timed automata currently relies on a technique based on integer discretisation of real-valued clocks, which can be expensive in some cases. In this paper, we propose symbolic techniques for verification and optimal strategy synthesis for priced probabilistic timed automata which avoid this discretisation. We build upon recent work for the special case of expected time properties, using value iteration over a zone-based abstraction of the model.", 
    "editor": [
      {
        "familyName": "Aceto", 
        "givenName": "Luca", 
        "type": "Person"
      }, 
      {
        "familyName": "Bacci", 
        "givenName": "Giorgio", 
        "type": "Person"
      }, 
      {
        "familyName": "Bacci", 
        "givenName": "Giovanni", 
        "type": "Person"
      }, 
      {
        "familyName": "Ing\u00f3lfsd\u00f3ttir", 
        "givenName": "Anna", 
        "type": "Person"
      }, 
      {
        "familyName": "Legay", 
        "givenName": "Axel", 
        "type": "Person"
      }, 
      {
        "familyName": "Mardare", 
        "givenName": "Radu", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-63121-9_15", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-319-63120-2", 
        "978-3-319-63121-9"
      ], 
      "name": "Models, Algorithms, Logics and Tools", 
      "type": "Book"
    }, 
    "keywords": [
      "Probabilistic Timed Automata", 
      "Timed Automata", 
      "real-time systems", 
      "computer security systems", 
      "wireless communication protocols", 
      "strategy synthesis", 
      "number of messages", 
      "symbolic verification", 
      "timed aspects", 
      "communication protocols", 
      "protocol execution", 
      "security system", 
      "symbolic techniques", 
      "time properties", 
      "Optimal Strategy Synthesis", 
      "value iteration", 
      "energy usage", 
      "execution", 
      "automata", 
      "verification", 
      "quantitative properties", 
      "system", 
      "abstraction", 
      "probabilistic", 
      "technique", 
      "variety of techniques", 
      "messages", 
      "iteration", 
      "recent work", 
      "usage", 
      "formalism", 
      "special case", 
      "protocol", 
      "discretisation", 
      "model", 
      "devices", 
      "example", 
      "work", 
      "Linearly", 
      "clock", 
      "aspects", 
      "number", 
      "variety", 
      "analyse", 
      "analysis", 
      "means", 
      "cases", 
      "dynamics", 
      "prices", 
      "properties", 
      "synthesis", 
      "paper", 
      "complex quantitative properties", 
      "integer discretisation", 
      "zone-based abstraction"
    ], 
    "name": "Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata", 
    "pagination": "289-309", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1090880541"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-63121-9_15"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-63121-9_15", 
      "https://app.dimensions.ai/details/publication/pub.1090880541"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-11-01T18:55", 
    "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_30.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-63121-9_15"
  }
]
 

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-63121-9_15'

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-63121-9_15'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-63121-9_15'

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-63121-9_15'


 

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

160 TRIPLES      23 PREDICATES      80 URIs      73 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-63121-9_15 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author Nc89334ced5a7418ca8b67b35972ac41c
4 schema:datePublished 2017-07-25
5 schema:datePublishedReg 2017-07-25
6 schema:description Probabilistic timed automata are a formalism for modelling systems whose dynamics includes probabilistic, nondeterministic and timed aspects including real-time systems. A variety of techniques have been proposed for the analysis of this formalism and successfully employed to analyse, for example, wireless communication protocols and computer security systems. Augmenting the model with prices (or, equivalently, costs or rewards) provides a means to verify more complex quantitative properties, such as the expected energy usage of a device or the expected number of messages sent during a protocol’s execution. However, the analysis of these properties on probabilistic timed automata currently relies on a technique based on integer discretisation of real-valued clocks, which can be expensive in some cases. In this paper, we propose symbolic techniques for verification and optimal strategy synthesis for priced probabilistic timed automata which avoid this discretisation. We build upon recent work for the special case of expected time properties, using value iteration over a zone-based abstraction of the model.
7 schema:editor N354996ea3127457793b5314100bc35d9
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf Nd0b8582afb3f43c4a6ac88e0f085c216
12 schema:keywords Linearly
13 Optimal Strategy Synthesis
14 Probabilistic Timed Automata
15 Timed Automata
16 abstraction
17 analyse
18 analysis
19 aspects
20 automata
21 cases
22 clock
23 communication protocols
24 complex quantitative properties
25 computer security systems
26 devices
27 discretisation
28 dynamics
29 energy usage
30 example
31 execution
32 formalism
33 integer discretisation
34 iteration
35 means
36 messages
37 model
38 number
39 number of messages
40 paper
41 prices
42 probabilistic
43 properties
44 protocol
45 protocol execution
46 quantitative properties
47 real-time systems
48 recent work
49 security system
50 special case
51 strategy synthesis
52 symbolic techniques
53 symbolic verification
54 synthesis
55 system
56 technique
57 time properties
58 timed aspects
59 usage
60 value iteration
61 variety
62 variety of techniques
63 verification
64 wireless communication protocols
65 work
66 zone-based abstraction
67 schema:name Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata
68 schema:pagination 289-309
69 schema:productId N09142d9f01724b3fad25442ac6b6f3c7
70 Ne5960678060e4410b03e35ea922829c6
71 schema:publisher N02e7c973080f4035a6eeda579b13ef32
72 schema:sameAs https://app.dimensions.ai/details/publication/pub.1090880541
73 https://doi.org/10.1007/978-3-319-63121-9_15
74 schema:sdDatePublished 2021-11-01T18:55
75 schema:sdLicense https://scigraph.springernature.com/explorer/license/
76 schema:sdPublisher N66049ee58b664df29e180668c82cfd88
77 schema:url https://doi.org/10.1007/978-3-319-63121-9_15
78 sgo:license sg:explorer/license/
79 sgo:sdDataset chapters
80 rdf:type schema:Chapter
81 N002c6281e98044349e6517981f9ac572 rdf:first sg:person.014007552600.37
82 rdf:rest rdf:nil
83 N008bc3c8324a4459a05061880ab36a56 rdf:first N6e1b7a801f284ae8a298b4db8026acd8
84 rdf:rest N48b21e8222d54c5181ffb9c8f948f555
85 N02e7c973080f4035a6eeda579b13ef32 schema:name Springer Nature
86 rdf:type schema:Organisation
87 N09142d9f01724b3fad25442ac6b6f3c7 schema:name doi
88 schema:value 10.1007/978-3-319-63121-9_15
89 rdf:type schema:PropertyValue
90 N092d82299e0149a6a703eca82bec9fce schema:familyName Ingólfsdóttir
91 schema:givenName Anna
92 rdf:type schema:Person
93 N354996ea3127457793b5314100bc35d9 rdf:first N561f12b113c640f8a42ab080e1ba4f89
94 rdf:rest N008bc3c8324a4459a05061880ab36a56
95 N488be98046034a799a5689e675ce71d5 schema:familyName Bacci
96 schema:givenName Giovanni
97 rdf:type schema:Person
98 N48b21e8222d54c5181ffb9c8f948f555 rdf:first N488be98046034a799a5689e675ce71d5
99 rdf:rest Nca02f0ffc0ff46439bebf3787124124c
100 N561f12b113c640f8a42ab080e1ba4f89 schema:familyName Aceto
101 schema:givenName Luca
102 rdf:type schema:Person
103 N59b93a4baeb349119ec1ca7c20531c5b rdf:first N75cb0a657d5e416dba122a317624ea47
104 rdf:rest N8cb9051af1c1469eb29df387ff28e9de
105 N66049ee58b664df29e180668c82cfd88 schema:name Springer Nature - SN SciGraph project
106 rdf:type schema:Organization
107 N6e1b7a801f284ae8a298b4db8026acd8 schema:familyName Bacci
108 schema:givenName Giorgio
109 rdf:type schema:Person
110 N75cb0a657d5e416dba122a317624ea47 schema:familyName Legay
111 schema:givenName Axel
112 rdf:type schema:Person
113 N8cb9051af1c1469eb29df387ff28e9de rdf:first Nac153c4daa214e79b559cded9a3fe168
114 rdf:rest rdf:nil
115 Nac153c4daa214e79b559cded9a3fe168 schema:familyName Mardare
116 schema:givenName Radu
117 rdf:type schema:Person
118 Nc89334ced5a7418ca8b67b35972ac41c rdf:first sg:person.011375012273.39
119 rdf:rest Ncc85a1e165d5491d838274174ef9a57c
120 Nca02f0ffc0ff46439bebf3787124124c rdf:first N092d82299e0149a6a703eca82bec9fce
121 rdf:rest N59b93a4baeb349119ec1ca7c20531c5b
122 Ncc85a1e165d5491d838274174ef9a57c rdf:first sg:person.016323171577.36
123 rdf:rest N002c6281e98044349e6517981f9ac572
124 Nd0b8582afb3f43c4a6ac88e0f085c216 schema:isbn 978-3-319-63120-2
125 978-3-319-63121-9
126 schema:name Models, Algorithms, Logics and Tools
127 rdf:type schema:Book
128 Ne5960678060e4410b03e35ea922829c6 schema:name dimensions_id
129 schema:value pub.1090880541
130 rdf:type schema:PropertyValue
131 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
132 schema:name Information and Computing Sciences
133 rdf:type schema:DefinedTerm
134 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
135 schema:name Computation Theory and Mathematics
136 rdf:type schema:DefinedTerm
137 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
138 schema:familyName Kwiatkowska
139 schema:givenName Marta
140 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
141 rdf:type schema:Person
142 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.6572.6
143 schema:familyName Parker
144 schema:givenName David
145 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
146 rdf:type schema:Person
147 sg:person.016323171577.36 schema:affiliation grid-institutes:grid.8756.c
148 schema:familyName Norman
149 schema:givenName Gethin
150 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36
151 rdf:type schema:Person
152 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, Oxford, UK
153 schema:name Department of Computer Science, University of Oxford, Oxford, UK
154 rdf:type schema:Organization
155 grid-institutes:grid.6572.6 schema:alternateName School of Computer Science, University of Birmingham, Birmingham, UK
156 schema:name School of Computer Science, University of Birmingham, Birmingham, UK
157 rdf:type schema:Organization
158 grid-institutes:grid.8756.c schema:alternateName School of Computing Science, University of Glasgow, Glasgow, UK
159 schema:name School of Computing Science, University of Glasgow, Glasgow, UK
160 rdf:type schema:Organization
 




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


...