Stochastic Games for Verification of Probabilistic Timed Automata View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2009

AUTHORS

Marta Kwiatkowska , Gethin Norman , David Parker

ABSTRACT

Probabilistic timed automata (PTAs) are used for formal modelling and verification of systems with probabilistic, nondeterministic and real-time behaviour. For non-probabilistic timed automata, forwards reachability is the analysis method of choice, since it can be implemented extremely efficiently. However, for PTAs, such techniques are only able to compute upper bounds on maximum reachability probabilities. In this paper, we propose a new approach to the analysis of PTAs using abstraction and stochastic games. We show how efficient forwards reachability techniques can be extended to yield both lower and upper bounds on maximum (and minimum) reachability probabilities. We also present abstraction-refinement techniques that are guaranteed to improve the precision of these probability bounds, providing a fully automatic method for computing the exact values. We have implemented these techniques and applied them to a set of large case studies. We show that, in comparison to alternative approaches to verifying PTAs, such as backwards reachability and digital clocks, our techniques exhibit superior performance and scalability. More... »

PAGES

212-227

Book

TITLE

Formal Modeling and Analysis of Timed Systems

ISBN

978-3-642-04367-3
978-3-642-04368-0

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-04368-0_17

DOI

http://dx.doi.org/10.1007/978-3-642-04368-0_17

DIMENSIONS

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


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/0801", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Artificial Intelligence and Image Processing", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Computing Laboratory, Oxford University, Parks Road, OX1 3QD, Oxford", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Computing Laboratory, Oxford University, Parks Road, OX1 3QD, Oxford"
          ], 
          "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": "Computing Laboratory, Oxford University, Parks Road, OX1 3QD, Oxford", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Computing Laboratory, Oxford University, Parks Road, OX1 3QD, Oxford"
          ], 
          "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": "Computing Laboratory, Oxford University, Parks Road, OX1 3QD, Oxford", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Computing Laboratory, Oxford University, Parks Road, OX1 3QD, Oxford"
          ], 
          "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": "2009", 
    "datePublishedReg": "2009-01-01", 
    "description": "Probabilistic timed automata (PTAs) are used for formal modelling and verification of systems with probabilistic, nondeterministic and real-time behaviour. For non-probabilistic timed automata, forwards reachability is the analysis method of choice, since it can be implemented extremely efficiently. However, for PTAs, such techniques are only able to compute upper bounds on maximum reachability probabilities. In this paper, we propose a new approach to the analysis of PTAs using abstraction and stochastic games. We show how efficient forwards reachability techniques can be extended to yield both lower and upper bounds on maximum (and minimum) reachability probabilities. We also present abstraction-refinement techniques that are guaranteed to improve the precision of these probability bounds, providing a fully automatic method for computing the exact values. We have implemented these techniques and applied them to a set of large case studies. We show that, in comparison to alternative approaches to verifying PTAs, such as backwards reachability and digital clocks, our techniques exhibit superior performance and scalability.", 
    "editor": [
      {
        "familyName": "Ouaknine", 
        "givenName": "Jo\u00ebl", 
        "type": "Person"
      }, 
      {
        "familyName": "Vaandrager", 
        "givenName": "Frits W.", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-04368-0_17", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-642-04367-3", 
        "978-3-642-04368-0"
      ], 
      "name": "Formal Modeling and Analysis of Timed Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "abstraction refinement technique", 
      "verification of systems", 
      "real-time behavior", 
      "Probabilistic Timed Automata", 
      "reachability probabilities", 
      "stochastic games", 
      "formal modelling", 
      "large case study", 
      "Timed Automata", 
      "automatic method", 
      "reachability techniques", 
      "upper bounds", 
      "such techniques", 
      "superior performance", 
      "automata", 
      "reachability", 
      "verification", 
      "new approach", 
      "game", 
      "digital clock", 
      "probability bounds", 
      "scalability", 
      "case study", 
      "abstraction", 
      "bounds", 
      "technique", 
      "analysis method", 
      "alternative approach", 
      "set", 
      "performance", 
      "method", 
      "system", 
      "exact values", 
      "probability", 
      "precision", 
      "modelling", 
      "clock", 
      "choice", 
      "PTA", 
      "behavior", 
      "analysis", 
      "comparison", 
      "values", 
      "study", 
      "approach", 
      "paper"
    ], 
    "name": "Stochastic Games for Verification of Probabilistic Timed Automata", 
    "pagination": "212-227", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1027948650"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-04368-0_17"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-04368-0_17", 
      "https://app.dimensions.ai/details/publication/pub.1027948650"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-10T10:48", 
    "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_337.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-04368-0_17"
  }
]
 

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-642-04368-0_17'

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-642-04368-0_17'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-04368-0_17'

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-642-04368-0_17'


 

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

125 TRIPLES      23 PREDICATES      72 URIs      65 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-04368-0_17 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 schema:author N2d10107e4fb54df1b94b4f27eaa5d1b1
4 schema:datePublished 2009
5 schema:datePublishedReg 2009-01-01
6 schema:description Probabilistic timed automata (PTAs) are used for formal modelling and verification of systems with probabilistic, nondeterministic and real-time behaviour. For non-probabilistic timed automata, forwards reachability is the analysis method of choice, since it can be implemented extremely efficiently. However, for PTAs, such techniques are only able to compute upper bounds on maximum reachability probabilities. In this paper, we propose a new approach to the analysis of PTAs using abstraction and stochastic games. We show how efficient forwards reachability techniques can be extended to yield both lower and upper bounds on maximum (and minimum) reachability probabilities. We also present abstraction-refinement techniques that are guaranteed to improve the precision of these probability bounds, providing a fully automatic method for computing the exact values. We have implemented these techniques and applied them to a set of large case studies. We show that, in comparison to alternative approaches to verifying PTAs, such as backwards reachability and digital clocks, our techniques exhibit superior performance and scalability.
7 schema:editor Nca2a1aad65c445b7a8c5d1ab6af39d92
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N58c83b015f4047a7a61e86531158cfae
12 schema:keywords PTA
13 Probabilistic Timed Automata
14 Timed Automata
15 abstraction
16 abstraction refinement technique
17 alternative approach
18 analysis
19 analysis method
20 approach
21 automata
22 automatic method
23 behavior
24 bounds
25 case study
26 choice
27 clock
28 comparison
29 digital clock
30 exact values
31 formal modelling
32 game
33 large case study
34 method
35 modelling
36 new approach
37 paper
38 performance
39 precision
40 probability
41 probability bounds
42 reachability
43 reachability probabilities
44 reachability techniques
45 real-time behavior
46 scalability
47 set
48 stochastic games
49 study
50 such techniques
51 superior performance
52 system
53 technique
54 upper bounds
55 values
56 verification
57 verification of systems
58 schema:name Stochastic Games for Verification of Probabilistic Timed Automata
59 schema:pagination 212-227
60 schema:productId N191aa39719a54bb7b8e135cea539bf79
61 N8e1e82bb952b4fe09fe64af11c97b902
62 schema:publisher N312c923ea9f84a288828cf37257581f4
63 schema:sameAs https://app.dimensions.ai/details/publication/pub.1027948650
64 https://doi.org/10.1007/978-3-642-04368-0_17
65 schema:sdDatePublished 2022-05-10T10:48
66 schema:sdLicense https://scigraph.springernature.com/explorer/license/
67 schema:sdPublisher N509421d519354f4e89677df3a5e78803
68 schema:url https://doi.org/10.1007/978-3-642-04368-0_17
69 sgo:license sg:explorer/license/
70 sgo:sdDataset chapters
71 rdf:type schema:Chapter
72 N191aa39719a54bb7b8e135cea539bf79 schema:name doi
73 schema:value 10.1007/978-3-642-04368-0_17
74 rdf:type schema:PropertyValue
75 N2d10107e4fb54df1b94b4f27eaa5d1b1 rdf:first sg:person.011375012273.39
76 rdf:rest Nc038a38a57e84109aa8fc236de30aacd
77 N312c923ea9f84a288828cf37257581f4 schema:name Springer Nature
78 rdf:type schema:Organisation
79 N509421d519354f4e89677df3a5e78803 schema:name Springer Nature - SN SciGraph project
80 rdf:type schema:Organization
81 N58c83b015f4047a7a61e86531158cfae schema:isbn 978-3-642-04367-3
82 978-3-642-04368-0
83 schema:name Formal Modeling and Analysis of Timed Systems
84 rdf:type schema:Book
85 N8e1e82bb952b4fe09fe64af11c97b902 schema:name dimensions_id
86 schema:value pub.1027948650
87 rdf:type schema:PropertyValue
88 N90c5880d2806411f8a090dd60e2c0fd1 rdf:first sg:person.014007552600.37
89 rdf:rest rdf:nil
90 Nbf240e93a0d34798beb5d90afceda5b1 rdf:first Ndbea168cf2e74236bf0e2d3f02900fd9
91 rdf:rest rdf:nil
92 Nc038a38a57e84109aa8fc236de30aacd rdf:first sg:person.016323171577.36
93 rdf:rest N90c5880d2806411f8a090dd60e2c0fd1
94 Nca2a1aad65c445b7a8c5d1ab6af39d92 rdf:first Nd293eddceec24e659749200b1ab5a6aa
95 rdf:rest Nbf240e93a0d34798beb5d90afceda5b1
96 Nd293eddceec24e659749200b1ab5a6aa schema:familyName Ouaknine
97 schema:givenName Joël
98 rdf:type schema:Person
99 Ndbea168cf2e74236bf0e2d3f02900fd9 schema:familyName Vaandrager
100 schema:givenName Frits W.
101 rdf:type schema:Person
102 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
103 schema:name Information and Computing Sciences
104 rdf:type schema:DefinedTerm
105 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
106 schema:name Artificial Intelligence and Image Processing
107 rdf:type schema:DefinedTerm
108 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
109 schema:familyName Kwiatkowska
110 schema:givenName Marta
111 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
112 rdf:type schema:Person
113 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.4991.5
114 schema:familyName Parker
115 schema:givenName David
116 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
117 rdf:type schema:Person
118 sg:person.016323171577.36 schema:affiliation grid-institutes:grid.4991.5
119 schema:familyName Norman
120 schema:givenName Gethin
121 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36
122 rdf:type schema:Person
123 grid-institutes:grid.4991.5 schema:alternateName Computing Laboratory, Oxford University, Parks Road, OX1 3QD, Oxford
124 schema:name Computing Laboratory, Oxford University, Parks Road, OX1 3QD, Oxford
125 rdf:type schema:Organization
 




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


...