Model Checking Probabilistic Systems View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2018-05-19

AUTHORS

Christel Baier , Luca de Alfaro , Vojtěch Forejt , Marta Kwiatkowska

ABSTRACT

The model-checking approach was originally formulated for verifying qualitative properties of systems, for example safety and liveness (see Chap. 10.1007/978-3-319-10575-8_2), and subsequently extended to also handle quantitative features, such as real time (see Chap. 10.1007/978-3-319-10575-8_29), continuous flows (see Chap. 10.1007/978-3-319-10575-8_30), as well as stochastic phenomena, where system evolution is governed by a given probability distribution. Probabilistic model checking aims to establish the correctness of probabilistic system models against quantitative probabilistic specifications, such as those capable of expressing, for example, the probability of an unsafe event occurring, expected time to termination, or expected power consumption in the start-up phase. In this chapter, we present the foundations of probabilistic model checking, focusing on finite-state Markov decision processes as models and quantitative properties expressed in probabilistic temporal logic. Markov decision processes can be thought of as a probabilistic variant of labelled transition systems in the following sense: transitions are labelled with actions, which can be chosen nondeterministically, and successor states for the chosen action are specified by means of discrete probabilistic distributions, thus specifying the probability of transiting to each successor state. To reason about expectations, we additionally annotate Markov decision processes with quantitative costs, which are incurred upon taking the selected action from a given state. Quantitative properties are expressed as formulas of the probabilistic computation tree logic (PCTL) or using linear temporal logic (LTL). We summarise the main model-checking algorithms for both PCTL and LTL, and illustrate their working through examples. The chapter ends with a brief overview of extensions to more expressive models and temporal logics, existing probabilistic model-checking tool support, and main application domains. More... »

PAGES

963-999

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-10575-8_28

DOI

http://dx.doi.org/10.1007/978-3-319-10575-8_28

DIMENSIONS

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


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": "Technische Universit\u00e4t Dresden, Dresden, Germany", 
          "id": "http://www.grid.ac/institutes/grid.4488.0", 
          "name": [
            "Technische Universit\u00e4t Dresden, Dresden, Germany"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Baier", 
        "givenName": "Christel", 
        "id": "sg:person.014160444244.72", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014160444244.72"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "University of California, Santa Cruz, Santa Cruz, CA, USA", 
          "id": "http://www.grid.ac/institutes/grid.205975.c", 
          "name": [
            "University of California, Santa Cruz, Santa Cruz, CA, USA"
          ], 
          "type": "Organization"
        }, 
        "familyName": "de Alfaro", 
        "givenName": "Luca", 
        "id": "sg:person.016435306053.10", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016435306053.10"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "University of Oxford, 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": "University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "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"
      }
    ], 
    "datePublished": "2018-05-19", 
    "datePublishedReg": "2018-05-19", 
    "description": "The model-checking approach was originally formulated for verifying qualitative properties of systems, for example safety and liveness (see Chap.\u00a010.1007/978-3-319-10575-8_2), and subsequently extended to also handle quantitative features, such as real time (see Chap.\u00a010.1007/978-3-319-10575-8_29), continuous flows (see Chap.\u00a010.1007/978-3-319-10575-8_30), as well as stochastic phenomena, where system evolution is governed by a given probability distribution. Probabilistic model checking aims to establish the correctness of probabilistic system models against quantitative probabilistic specifications, such as those capable of expressing, for example, the probability of an unsafe event occurring, expected time to termination, or expected power consumption in the start-up phase. In this chapter, we present the foundations of probabilistic model checking, focusing on finite-state Markov decision processes as models and quantitative properties expressed in probabilistic temporal logic. Markov decision processes can be thought of as a probabilistic variant of labelled transition systems in the following sense: transitions are labelled with actions, which can be chosen nondeterministically, and successor states for the chosen action are specified by means of discrete probabilistic distributions, thus specifying the probability of transiting to each successor state. To reason about expectations, we additionally annotate Markov decision processes with quantitative costs, which are incurred upon taking the selected action from a given state. Quantitative properties are expressed as formulas of the probabilistic computation tree logic (PCTL) or using linear temporal logic (LTL). We summarise the main model-checking algorithms for both PCTL and LTL, and illustrate their working through examples. The chapter ends with a brief overview of extensions to more expressive models and temporal logics, existing probabilistic model-checking tool support, and main application domains.", 
    "editor": [
      {
        "familyName": "Clarke", 
        "givenName": "Edmund M.", 
        "type": "Person"
      }, 
      {
        "familyName": "Henzinger", 
        "givenName": "Thomas A.", 
        "type": "Person"
      }, 
      {
        "familyName": "Veith", 
        "givenName": "Helmut", 
        "type": "Person"
      }, 
      {
        "familyName": "Bloem", 
        "givenName": "Roderick", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-10575-8_28", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-319-10574-1", 
        "978-3-319-10575-8"
      ], 
      "name": "Handbook of Model Checking", 
      "type": "Book"
    }, 
    "keywords": [
      "probabilistic computation tree logic", 
      "linear temporal logic", 
      "probabilistic model checking", 
      "Markov decision process", 
      "temporal logic", 
      "model checking", 
      "model-checking approach", 
      "model-checking algorithm", 
      "decision process", 
      "Computation Tree Logic", 
      "main application domains", 
      "probabilistic temporal logic", 
      "probabilistic system model", 
      "tool support", 
      "application domains", 
      "tree logic", 
      "expressive model", 
      "probabilistic variant", 
      "probabilistic systems", 
      "quantitative properties", 
      "transition systems", 
      "probabilistic specifications", 
      "real time", 
      "example safety", 
      "quantitative cost", 
      "checking", 
      "system model", 
      "power consumption", 
      "logic", 
      "system evolution", 
      "unsafe events", 
      "probabilistic distribution", 
      "algorithm", 
      "liveness", 
      "probability distribution", 
      "correctness", 
      "system", 
      "quantitative features", 
      "specification", 
      "finite-state Markov decision processes", 
      "model", 
      "brief overview", 
      "example", 
      "probability", 
      "cost", 
      "features", 
      "process", 
      "domain", 
      "extension", 
      "time", 
      "foundation", 
      "state", 
      "support", 
      "overview", 
      "qualitative properties", 
      "consumption", 
      "chapter", 
      "working", 
      "stochastic phenomena", 
      "sense", 
      "means", 
      "variants", 
      "action", 
      "safety", 
      "continuous flow", 
      "reasons", 
      "successor states", 
      "expectations", 
      "evolution", 
      "distribution", 
      "properties", 
      "formula", 
      "flow", 
      "events", 
      "phase", 
      "termination", 
      "phenomenon", 
      "transition", 
      "approach", 
      "quantitative probabilistic specifications", 
      "discrete probabilistic distributions", 
      "main model-checking algorithms", 
      "probabilistic model-checking tool support", 
      "model-checking tool support"
    ], 
    "name": "Model Checking Probabilistic Systems", 
    "pagination": "963-999", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1104120204"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-10575-8_28"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-10575-8_28", 
      "https://app.dimensions.ai/details/publication/pub.1104120204"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-11-01T18:56", 
    "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_328.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-10575-8_28"
  }
]
 

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-10575-8_28'

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-10575-8_28'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-10575-8_28'

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-10575-8_28'


 

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

186 TRIPLES      23 PREDICATES      108 URIs      101 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-10575-8_28 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N81c9013abcf54dfab327da2d817f7da2
4 schema:datePublished 2018-05-19
5 schema:datePublishedReg 2018-05-19
6 schema:description The model-checking approach was originally formulated for verifying qualitative properties of systems, for example safety and liveness (see Chap. 10.1007/978-3-319-10575-8_2), and subsequently extended to also handle quantitative features, such as real time (see Chap. 10.1007/978-3-319-10575-8_29), continuous flows (see Chap. 10.1007/978-3-319-10575-8_30), as well as stochastic phenomena, where system evolution is governed by a given probability distribution. Probabilistic model checking aims to establish the correctness of probabilistic system models against quantitative probabilistic specifications, such as those capable of expressing, for example, the probability of an unsafe event occurring, expected time to termination, or expected power consumption in the start-up phase. In this chapter, we present the foundations of probabilistic model checking, focusing on finite-state Markov decision processes as models and quantitative properties expressed in probabilistic temporal logic. Markov decision processes can be thought of as a probabilistic variant of labelled transition systems in the following sense: transitions are labelled with actions, which can be chosen nondeterministically, and successor states for the chosen action are specified by means of discrete probabilistic distributions, thus specifying the probability of transiting to each successor state. To reason about expectations, we additionally annotate Markov decision processes with quantitative costs, which are incurred upon taking the selected action from a given state. Quantitative properties are expressed as formulas of the probabilistic computation tree logic (PCTL) or using linear temporal logic (LTL). We summarise the main model-checking algorithms for both PCTL and LTL, and illustrate their working through examples. The chapter ends with a brief overview of extensions to more expressive models and temporal logics, existing probabilistic model-checking tool support, and main application domains.
7 schema:editor Ne4067d413f1e4b959553032832b89c9a
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf Ned86c5cd1b9f4312bf8cef5f48393fa3
12 schema:keywords Computation Tree Logic
13 Markov decision process
14 action
15 algorithm
16 application domains
17 approach
18 brief overview
19 chapter
20 checking
21 consumption
22 continuous flow
23 correctness
24 cost
25 decision process
26 discrete probabilistic distributions
27 distribution
28 domain
29 events
30 evolution
31 example
32 example safety
33 expectations
34 expressive model
35 extension
36 features
37 finite-state Markov decision processes
38 flow
39 formula
40 foundation
41 linear temporal logic
42 liveness
43 logic
44 main application domains
45 main model-checking algorithms
46 means
47 model
48 model checking
49 model-checking algorithm
50 model-checking approach
51 model-checking tool support
52 overview
53 phase
54 phenomenon
55 power consumption
56 probabilistic computation tree logic
57 probabilistic distribution
58 probabilistic model checking
59 probabilistic model-checking tool support
60 probabilistic specifications
61 probabilistic system model
62 probabilistic systems
63 probabilistic temporal logic
64 probabilistic variant
65 probability
66 probability distribution
67 process
68 properties
69 qualitative properties
70 quantitative cost
71 quantitative features
72 quantitative probabilistic specifications
73 quantitative properties
74 real time
75 reasons
76 safety
77 sense
78 specification
79 state
80 stochastic phenomena
81 successor states
82 support
83 system
84 system evolution
85 system model
86 temporal logic
87 termination
88 time
89 tool support
90 transition
91 transition systems
92 tree logic
93 unsafe events
94 variants
95 working
96 schema:name Model Checking Probabilistic Systems
97 schema:pagination 963-999
98 schema:productId N063f499507754a94bb35afe1afad9261
99 N85bed28130c840baaa123c05a4c705bf
100 schema:publisher N85dd348b6f584b918fdbab2e8d29fd3f
101 schema:sameAs https://app.dimensions.ai/details/publication/pub.1104120204
102 https://doi.org/10.1007/978-3-319-10575-8_28
103 schema:sdDatePublished 2021-11-01T18:56
104 schema:sdLicense https://scigraph.springernature.com/explorer/license/
105 schema:sdPublisher Nb0a0e2e0076044bbaa27cb3f20c41c0f
106 schema:url https://doi.org/10.1007/978-3-319-10575-8_28
107 sgo:license sg:explorer/license/
108 sgo:sdDataset chapters
109 rdf:type schema:Chapter
110 N063f499507754a94bb35afe1afad9261 schema:name dimensions_id
111 schema:value pub.1104120204
112 rdf:type schema:PropertyValue
113 N1c41043fbe4d4f508804d8bf14d19f7e rdf:first Nc29ded6c23ba402bb855a8966ded47f0
114 rdf:rest N94871fd959c649bea13d8e39cd59355f
115 N259cfa24dcc54140974e56a9a3ebeda1 rdf:first Nb363464e904047d686076ef1cf448776
116 rdf:rest rdf:nil
117 N81c9013abcf54dfab327da2d817f7da2 rdf:first sg:person.014160444244.72
118 rdf:rest Nff31c2c46949432f9727a655813c64c6
119 N83f4246c9d704870bbd00d4f7d0baed3 rdf:first sg:person.011375012273.39
120 rdf:rest rdf:nil
121 N85bed28130c840baaa123c05a4c705bf schema:name doi
122 schema:value 10.1007/978-3-319-10575-8_28
123 rdf:type schema:PropertyValue
124 N85dd348b6f584b918fdbab2e8d29fd3f schema:name Springer Nature
125 rdf:type schema:Organisation
126 N94871fd959c649bea13d8e39cd59355f rdf:first Na5d87bc6bc13444ca241aaebc6b12abf
127 rdf:rest N259cfa24dcc54140974e56a9a3ebeda1
128 Na5d87bc6bc13444ca241aaebc6b12abf schema:familyName Veith
129 schema:givenName Helmut
130 rdf:type schema:Person
131 Nb0a0e2e0076044bbaa27cb3f20c41c0f schema:name Springer Nature - SN SciGraph project
132 rdf:type schema:Organization
133 Nb363464e904047d686076ef1cf448776 schema:familyName Bloem
134 schema:givenName Roderick
135 rdf:type schema:Person
136 Nc29ded6c23ba402bb855a8966ded47f0 schema:familyName Henzinger
137 schema:givenName Thomas A.
138 rdf:type schema:Person
139 Nc9e5b858ded34ad5b93519f8c9a29f6b schema:familyName Clarke
140 schema:givenName Edmund M.
141 rdf:type schema:Person
142 Ne2a8936fe1ce4d41b5a3c6c9d8ce597c rdf:first sg:person.012103627631.41
143 rdf:rest N83f4246c9d704870bbd00d4f7d0baed3
144 Ne4067d413f1e4b959553032832b89c9a rdf:first Nc9e5b858ded34ad5b93519f8c9a29f6b
145 rdf:rest N1c41043fbe4d4f508804d8bf14d19f7e
146 Ned86c5cd1b9f4312bf8cef5f48393fa3 schema:isbn 978-3-319-10574-1
147 978-3-319-10575-8
148 schema:name Handbook of Model Checking
149 rdf:type schema:Book
150 Nff31c2c46949432f9727a655813c64c6 rdf:first sg:person.016435306053.10
151 rdf:rest Ne2a8936fe1ce4d41b5a3c6c9d8ce597c
152 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
153 schema:name Information and Computing Sciences
154 rdf:type schema:DefinedTerm
155 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
156 schema:name Computation Theory and Mathematics
157 rdf:type schema:DefinedTerm
158 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
159 schema:familyName Kwiatkowska
160 schema:givenName Marta
161 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
162 rdf:type schema:Person
163 sg:person.012103627631.41 schema:affiliation grid-institutes:grid.4991.5
164 schema:familyName Forejt
165 schema:givenName Vojtěch
166 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012103627631.41
167 rdf:type schema:Person
168 sg:person.014160444244.72 schema:affiliation grid-institutes:grid.4488.0
169 schema:familyName Baier
170 schema:givenName Christel
171 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014160444244.72
172 rdf:type schema:Person
173 sg:person.016435306053.10 schema:affiliation grid-institutes:grid.205975.c
174 schema:familyName de Alfaro
175 schema:givenName Luca
176 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016435306053.10
177 rdf:type schema:Person
178 grid-institutes:grid.205975.c schema:alternateName University of California, Santa Cruz, Santa Cruz, CA, USA
179 schema:name University of California, Santa Cruz, Santa Cruz, CA, USA
180 rdf:type schema:Organization
181 grid-institutes:grid.4488.0 schema:alternateName Technische Universität Dresden, Dresden, Germany
182 schema:name Technische Universität Dresden, Dresden, Germany
183 rdf:type schema:Organization
184 grid-institutes:grid.4991.5 schema:alternateName University of Oxford, Oxford, UK
185 schema:name University of Oxford, Oxford, UK
186 rdf:type schema:Organization
 




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


...