Assume-Guarantee Verification for Probabilistic Systems View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2010

AUTHORS

Marta Kwiatkowska , Gethin Norman , David Parker , Hongyang Qu

ABSTRACT

We present a compositional verification technique for systems that exhibit both probabilistic and nondeterministic behaviour. We adopt an assume-guarantee approach to verification, where both the assumptions made about system components and the guarantees that they provide are regular safety properties, represented by finite automata. Unlike previous proposals for assume-guarantee reasoning about probabilistic systems, our approach does not require that components interact in a fully synchronous fashion. In addition, the compositional verification method is efficient and fully automated, based on a reduction to the problem of multi-objective probabilistic model checking. We present asymmetric and circular assume-guarantee rules, and show how they can be adapted to form quantitative queries, yielding lower and upper bounds on the actual probabilities that a property is satisfied. Our techniques have been implemented and applied to several large case studies, including instances where conventional probabilistic verification is infeasible. More... »

PAGES

23-37

Book

TITLE

Tools and Algorithms for the Construction and Analysis of Systems

ISBN

978-3-642-12001-5
978-3-642-12002-2

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-12002-2_3

DOI

http://dx.doi.org/10.1007/978-3-642-12002-2_3

DIMENSIONS

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


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": "Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Oxford University Computing Laboratory, Parks Road, 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"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK", 
          "id": "http://www.grid.ac/institutes/grid.8756.c", 
          "name": [
            "Department of Computing Science, University of Glasgow, G12 8RZ, 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": "Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, 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"
      }, 
      {
        "affiliation": {
          "alternateName": "Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Qu", 
        "givenName": "Hongyang", 
        "id": "sg:person.011574463543.04", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011574463543.04"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2010", 
    "datePublishedReg": "2010-01-01", 
    "description": "We present a compositional verification technique for systems that exhibit both probabilistic and nondeterministic behaviour. We adopt an assume-guarantee approach to verification, where both the assumptions made about system components and the guarantees that they provide are regular safety properties, represented by finite automata. Unlike previous proposals for assume-guarantee reasoning about probabilistic systems, our approach does not require that components interact in a fully synchronous fashion. In addition, the compositional verification method is efficient and fully automated, based on a reduction to the problem of multi-objective probabilistic model checking. We present asymmetric and circular assume-guarantee rules, and show how they can be adapted to form quantitative queries, yielding lower and upper bounds on the actual probabilities that a property is satisfied. Our techniques have been implemented and applied to several large case studies, including instances where conventional probabilistic verification is infeasible.", 
    "editor": [
      {
        "familyName": "Esparza", 
        "givenName": "Javier", 
        "type": "Person"
      }, 
      {
        "familyName": "Majumdar", 
        "givenName": "Rupak", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-12002-2_3", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-642-12001-5", 
        "978-3-642-12002-2"
      ], 
      "name": "Tools and Algorithms for the Construction and Analysis of Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "probabilistic systems", 
      "assume-guarantee approach", 
      "compositional verification techniques", 
      "compositional verification method", 
      "assume-guarantee reasoning", 
      "assume-guarantee rule", 
      "probabilistic model checking", 
      "Guarantee Verification", 
      "regular safety properties", 
      "quantitative queries", 
      "verification techniques", 
      "model checking", 
      "large case study", 
      "probabilistic verification", 
      "nondeterministic behavior", 
      "safety properties", 
      "verification method", 
      "system components", 
      "finite automata", 
      "verification", 
      "previous proposals", 
      "synchronous fashion", 
      "queries", 
      "upper bounds", 
      "checking", 
      "case study", 
      "guarantees", 
      "system", 
      "reasoning", 
      "automata", 
      "technique", 
      "instances", 
      "proposal", 
      "rules", 
      "actual probability", 
      "bounds", 
      "components", 
      "method", 
      "fashion", 
      "probability", 
      "assumption", 
      "behavior", 
      "addition", 
      "properties", 
      "reduction", 
      "study", 
      "approach", 
      "problem"
    ], 
    "name": "Assume-Guarantee Verification for Probabilistic Systems", 
    "pagination": "23-37", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1019129445"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-12002-2_3"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-12002-2_3", 
      "https://app.dimensions.ai/details/publication/pub.1019129445"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-10T10:46", 
    "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_300.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-12002-2_3"
  }
]
 

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-12002-2_3'

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-12002-2_3'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-12002-2_3'

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-12002-2_3'


 

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

137 TRIPLES      23 PREDICATES      74 URIs      67 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-12002-2_3 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N9ac46f2781da4c3eaefbb69516fb9b9a
4 schema:datePublished 2010
5 schema:datePublishedReg 2010-01-01
6 schema:description We present a compositional verification technique for systems that exhibit both probabilistic and nondeterministic behaviour. We adopt an assume-guarantee approach to verification, where both the assumptions made about system components and the guarantees that they provide are regular safety properties, represented by finite automata. Unlike previous proposals for assume-guarantee reasoning about probabilistic systems, our approach does not require that components interact in a fully synchronous fashion. In addition, the compositional verification method is efficient and fully automated, based on a reduction to the problem of multi-objective probabilistic model checking. We present asymmetric and circular assume-guarantee rules, and show how they can be adapted to form quantitative queries, yielding lower and upper bounds on the actual probabilities that a property is satisfied. Our techniques have been implemented and applied to several large case studies, including instances where conventional probabilistic verification is infeasible.
7 schema:editor Na3835d2cf1f14832b5ae97cbd490198a
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N530ebca163ee48709cb45f59135c96fa
12 schema:keywords Guarantee Verification
13 actual probability
14 addition
15 approach
16 assume-guarantee approach
17 assume-guarantee reasoning
18 assume-guarantee rule
19 assumption
20 automata
21 behavior
22 bounds
23 case study
24 checking
25 components
26 compositional verification method
27 compositional verification techniques
28 fashion
29 finite automata
30 guarantees
31 instances
32 large case study
33 method
34 model checking
35 nondeterministic behavior
36 previous proposals
37 probabilistic model checking
38 probabilistic systems
39 probabilistic verification
40 probability
41 problem
42 properties
43 proposal
44 quantitative queries
45 queries
46 reasoning
47 reduction
48 regular safety properties
49 rules
50 safety properties
51 study
52 synchronous fashion
53 system
54 system components
55 technique
56 upper bounds
57 verification
58 verification method
59 verification techniques
60 schema:name Assume-Guarantee Verification for Probabilistic Systems
61 schema:pagination 23-37
62 schema:productId Nabf754684ce34b409ad8d354e5d98cf5
63 Ndb89aea2a3524fc48bc3b17137ab2939
64 schema:publisher N72e9cb0d0ed64886adb0dd05b8373bc5
65 schema:sameAs https://app.dimensions.ai/details/publication/pub.1019129445
66 https://doi.org/10.1007/978-3-642-12002-2_3
67 schema:sdDatePublished 2022-05-10T10:46
68 schema:sdLicense https://scigraph.springernature.com/explorer/license/
69 schema:sdPublisher N020d9457a7a740e18906276c78bfa9ba
70 schema:url https://doi.org/10.1007/978-3-642-12002-2_3
71 sgo:license sg:explorer/license/
72 sgo:sdDataset chapters
73 rdf:type schema:Chapter
74 N020d9457a7a740e18906276c78bfa9ba schema:name Springer Nature - SN SciGraph project
75 rdf:type schema:Organization
76 N2126524a67a84fa49e95c5a25cff1da4 schema:familyName Majumdar
77 schema:givenName Rupak
78 rdf:type schema:Person
79 N31859ea013aa4adc908c3a790e66a56d rdf:first sg:person.014007552600.37
80 rdf:rest Nae39ed8bb5f24bf5a9bc40efcf25af8b
81 N530ebca163ee48709cb45f59135c96fa schema:isbn 978-3-642-12001-5
82 978-3-642-12002-2
83 schema:name Tools and Algorithms for the Construction and Analysis of Systems
84 rdf:type schema:Book
85 N6e317623873f4fce9391c366c2a3e824 rdf:first sg:person.016323171577.36
86 rdf:rest N31859ea013aa4adc908c3a790e66a56d
87 N72e9cb0d0ed64886adb0dd05b8373bc5 schema:name Springer Nature
88 rdf:type schema:Organisation
89 N9528fc432e0143ba997ae3f7df6d3971 schema:familyName Esparza
90 schema:givenName Javier
91 rdf:type schema:Person
92 N9ac46f2781da4c3eaefbb69516fb9b9a rdf:first sg:person.011375012273.39
93 rdf:rest N6e317623873f4fce9391c366c2a3e824
94 Na3835d2cf1f14832b5ae97cbd490198a rdf:first N9528fc432e0143ba997ae3f7df6d3971
95 rdf:rest Nafef41c3a33e47c48ec8abf2544a8824
96 Nabf754684ce34b409ad8d354e5d98cf5 schema:name doi
97 schema:value 10.1007/978-3-642-12002-2_3
98 rdf:type schema:PropertyValue
99 Nae39ed8bb5f24bf5a9bc40efcf25af8b rdf:first sg:person.011574463543.04
100 rdf:rest rdf:nil
101 Nafef41c3a33e47c48ec8abf2544a8824 rdf:first N2126524a67a84fa49e95c5a25cff1da4
102 rdf:rest rdf:nil
103 Ndb89aea2a3524fc48bc3b17137ab2939 schema:name dimensions_id
104 schema:value pub.1019129445
105 rdf:type schema:PropertyValue
106 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
107 schema:name Information and Computing Sciences
108 rdf:type schema:DefinedTerm
109 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
110 schema:name Computation Theory and Mathematics
111 rdf:type schema:DefinedTerm
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 sg:person.011574463543.04 schema:affiliation grid-institutes:grid.4991.5
118 schema:familyName Qu
119 schema:givenName Hongyang
120 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011574463543.04
121 rdf:type schema:Person
122 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.4991.5
123 schema:familyName Parker
124 schema:givenName David
125 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
126 rdf:type schema:Person
127 sg:person.016323171577.36 schema:affiliation grid-institutes:grid.8756.c
128 schema:familyName Norman
129 schema:givenName Gethin
130 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36
131 rdf:type schema:Person
132 grid-institutes:grid.4991.5 schema:alternateName Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, UK
133 schema:name Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, UK
134 rdf:type schema:Organization
135 grid-institutes:grid.8756.c schema:alternateName Department of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK
136 schema:name Department of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK
137 rdf:type schema:Organization
 




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


...