Ontology type: schema:Chapter Open Access: True
2011
AUTHORSVojtěch Forejt , Marta Kwiatkowska , Gethin Norman , David Parker , Hongyang Qu
ABSTRACTWe 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... »
PAGES112-127
Tools and Algorithms for the Construction and Analysis of Systems
ISBN
978-3-642-19834-2
978-3-642-19835-9
http://scigraph.springernature.com/pub.10.1007/978-3-642-19835-9_11
DOIhttp://dx.doi.org/10.1007/978-3-642-19835-9_11
DIMENSIONShttps://app.dimensions.ai/details/publication/pub.1002062315
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
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