Quantitative Multi-objective Verification for Probabilistic Systems View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2011

AUTHORS

Vojtěch Forejt , Marta Kwiatkowska , Gethin Norman , David Parker , Hongyang Qu

ABSTRACT

We present a verification framework for analysing multiple quantitative objectives of systems that exhibit both nondeterministic and stochastic behaviour. These systems are modelled as probabilistic automata, enriched with cost or reward structures that capture, for example, energy usage or performance metrics. Quantitative properties of these models are expressed in a specification language that incorporates probabilistic safety and liveness properties, expected total cost or reward, and supports multiple objectives of these types. We propose and implement an efficient verification framework for such properties and then present two distinct applications of it: firstly, controller synthesis subject to multiple quantitative objectives; and, secondly, quantitative compositional verification. The practical applicability of both approaches is illustrated with experimental results from several large case studies. More... »

PAGES

112-127

Book

TITLE

Tools and Algorithms for the Construction and Analysis of Systems

ISBN

978-3-642-19834-2
978-3-642-19835-9

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-19835-9_11

DOI

http://dx.doi.org/10.1007/978-3-642-19835-9_11

DIMENSIONS

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


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": "Computing Laboratory, Oxford University, Parks Road, OX1 3QD, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Computing Laboratory, Oxford University, Parks Road, OX1 3QD, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Forejt", 
        "givenName": "Vojt\u011bch", 
        "id": "sg:person.012103627631.41", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012103627631.41"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Computing Laboratory, Oxford University, Parks Road, OX1 3QD, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Computing Laboratory, Oxford University, 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": "School of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK", 
          "id": "http://www.grid.ac/institutes/grid.8756.c", 
          "name": [
            "School 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": "Computing Laboratory, Oxford University, Parks Road, OX1 3QD, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Computing Laboratory, Oxford University, 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": "Computing Laboratory, Oxford University, Parks Road, OX1 3QD, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Computing Laboratory, Oxford University, 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": "2011", 
    "datePublishedReg": "2011-01-01", 
    "description": "We present a verification framework for analysing multiple quantitative objectives of systems that exhibit both nondeterministic and stochastic behaviour. These systems are modelled as probabilistic automata, enriched with cost or reward structures that capture, for example, energy usage or performance metrics. Quantitative properties of these models are expressed in a specification language that incorporates probabilistic safety and liveness properties, expected total cost or reward, and supports multiple objectives of these types. We propose and implement an efficient verification framework for such properties and then present two distinct applications of it: firstly, controller synthesis subject to multiple quantitative objectives; and, secondly, quantitative compositional verification. The practical applicability of both approaches is illustrated with experimental results from several large case studies.", 
    "editor": [
      {
        "familyName": "Abdulla", 
        "givenName": "Parosh Aziz", 
        "type": "Person"
      }, 
      {
        "familyName": "Leino", 
        "givenName": "K. Rustan M.", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-19835-9_11", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-642-19834-2", 
        "978-3-642-19835-9"
      ], 
      "name": "Tools and Algorithms for the Construction and Analysis of Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "quantitative objectives", 
      "controller synthesis", 
      "stochastic behavior", 
      "multiple objectives", 
      "probabilistic systems", 
      "probabilistic automata", 
      "quantitative properties", 
      "practical applicability", 
      "performance metrics", 
      "such properties", 
      "distinct applications", 
      "large case study", 
      "probabilistic safety", 
      "experimental results", 
      "properties", 
      "system", 
      "framework", 
      "automata", 
      "total cost", 
      "applicability", 
      "metrics", 
      "verification", 
      "model", 
      "liveness properties", 
      "reward structure", 
      "applications", 
      "approach", 
      "case study", 
      "cost", 
      "verification framework", 
      "structure", 
      "objective", 
      "behavior", 
      "results", 
      "energy usage", 
      "types", 
      "usage", 
      "capture", 
      "specification language", 
      "compositional verification", 
      "study", 
      "language", 
      "synthesis", 
      "reward", 
      "safety", 
      "example"
    ], 
    "name": "Quantitative Multi-objective Verification for Probabilistic Systems", 
    "pagination": "112-127", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1002062315"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-19835-9_11"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-19835-9_11", 
      "https://app.dimensions.ai/details/publication/pub.1002062315"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-10T10:37", 
    "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_124.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-19835-9_11"
  }
]
 

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-19835-9_11'

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-19835-9_11'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-19835-9_11'

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-19835-9_11'


 

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

142 TRIPLES      23 PREDICATES      72 URIs      65 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-19835-9_11 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author Nb737a2a8912a456b86159595d7bb4837
4 schema:datePublished 2011
5 schema:datePublishedReg 2011-01-01
6 schema:description We present a verification framework for analysing multiple quantitative objectives of systems that exhibit both nondeterministic and stochastic behaviour. These systems are modelled as probabilistic automata, enriched with cost or reward structures that capture, for example, energy usage or performance metrics. Quantitative properties of these models are expressed in a specification language that incorporates probabilistic safety and liveness properties, expected total cost or reward, and supports multiple objectives of these types. We propose and implement an efficient verification framework for such properties and then present two distinct applications of it: firstly, controller synthesis subject to multiple quantitative objectives; and, secondly, quantitative compositional verification. The practical applicability of both approaches is illustrated with experimental results from several large case studies.
7 schema:editor Nf3ce95b43eff46138227dd3f04347684
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N9d49d0984482436598afeaf33d778fec
12 schema:keywords applicability
13 applications
14 approach
15 automata
16 behavior
17 capture
18 case study
19 compositional verification
20 controller synthesis
21 cost
22 distinct applications
23 energy usage
24 example
25 experimental results
26 framework
27 language
28 large case study
29 liveness properties
30 metrics
31 model
32 multiple objectives
33 objective
34 performance metrics
35 practical applicability
36 probabilistic automata
37 probabilistic safety
38 probabilistic systems
39 properties
40 quantitative objectives
41 quantitative properties
42 results
43 reward
44 reward structure
45 safety
46 specification language
47 stochastic behavior
48 structure
49 study
50 such properties
51 synthesis
52 system
53 total cost
54 types
55 usage
56 verification
57 verification framework
58 schema:name Quantitative Multi-objective Verification for Probabilistic Systems
59 schema:pagination 112-127
60 schema:productId N089005b619e94c40b8490aec54a02e36
61 N83b19a9883974ca0b7bc60939d933956
62 schema:publisher N750590d2be6c44df9d3c75dc6f5e408d
63 schema:sameAs https://app.dimensions.ai/details/publication/pub.1002062315
64 https://doi.org/10.1007/978-3-642-19835-9_11
65 schema:sdDatePublished 2022-05-10T10:37
66 schema:sdLicense https://scigraph.springernature.com/explorer/license/
67 schema:sdPublisher N9eb3513531e140bdacbc40864cebf3bc
68 schema:url https://doi.org/10.1007/978-3-642-19835-9_11
69 sgo:license sg:explorer/license/
70 sgo:sdDataset chapters
71 rdf:type schema:Chapter
72 N089005b619e94c40b8490aec54a02e36 schema:name dimensions_id
73 schema:value pub.1002062315
74 rdf:type schema:PropertyValue
75 N112f8141b02547fd827bd04df270ea40 rdf:first sg:person.014007552600.37
76 rdf:rest Nd727e613259645d08408a3896b6cb74e
77 N32d4a6933f90447795069f562e39da87 rdf:first N3560ad135f1e43dea802e721353445a9
78 rdf:rest rdf:nil
79 N3560ad135f1e43dea802e721353445a9 schema:familyName Leino
80 schema:givenName K. Rustan M.
81 rdf:type schema:Person
82 N750590d2be6c44df9d3c75dc6f5e408d schema:name Springer Nature
83 rdf:type schema:Organisation
84 N83b19a9883974ca0b7bc60939d933956 schema:name doi
85 schema:value 10.1007/978-3-642-19835-9_11
86 rdf:type schema:PropertyValue
87 N9d49d0984482436598afeaf33d778fec schema:isbn 978-3-642-19834-2
88 978-3-642-19835-9
89 schema:name Tools and Algorithms for the Construction and Analysis of Systems
90 rdf:type schema:Book
91 N9eb3513531e140bdacbc40864cebf3bc schema:name Springer Nature - SN SciGraph project
92 rdf:type schema:Organization
93 Na32353795fdd4ccf8b3744311c1ca380 rdf:first sg:person.016323171577.36
94 rdf:rest N112f8141b02547fd827bd04df270ea40
95 Nb737a2a8912a456b86159595d7bb4837 rdf:first sg:person.012103627631.41
96 rdf:rest Ncb1ee73783b947068c6327fce8c1844b
97 Ncb1ee73783b947068c6327fce8c1844b rdf:first sg:person.011375012273.39
98 rdf:rest Na32353795fdd4ccf8b3744311c1ca380
99 Nd727e613259645d08408a3896b6cb74e rdf:first sg:person.011574463543.04
100 rdf:rest rdf:nil
101 Need8d6091b1a47968df76e8df9771048 schema:familyName Abdulla
102 schema:givenName Parosh Aziz
103 rdf:type schema:Person
104 Nf3ce95b43eff46138227dd3f04347684 rdf:first Need8d6091b1a47968df76e8df9771048
105 rdf:rest N32d4a6933f90447795069f562e39da87
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.012103627631.41 schema:affiliation grid-institutes:grid.4991.5
123 schema:familyName Forejt
124 schema:givenName Vojtěch
125 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012103627631.41
126 rdf:type schema:Person
127 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.4991.5
128 schema:familyName Parker
129 schema:givenName David
130 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
131 rdf:type schema:Person
132 sg:person.016323171577.36 schema:affiliation grid-institutes:grid.8756.c
133 schema:familyName Norman
134 schema:givenName Gethin
135 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36
136 rdf:type schema:Person
137 grid-institutes:grid.4991.5 schema:alternateName Computing Laboratory, Oxford University, Parks Road, OX1 3QD, Oxford, UK
138 schema:name Computing Laboratory, Oxford University, Parks Road, OX1 3QD, Oxford, UK
139 rdf:type schema:Organization
140 grid-institutes:grid.8756.c schema:alternateName School of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK
141 schema:name School of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK
142 rdf:type schema:Organization
 




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


...