Stochastic Model Checking View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2007-01-01

AUTHORS

Marta Kwiatkowska , Gethin Norman , David Parker

ABSTRACT

This tutorial presents an overview of model checking for both discrete and continuous-time Markov chains (DTMCs and CTMCs). Model checking algorithms are given for verifying DTMCs and CTMCs against specifications written in probabilistic extensions of temporal logic, including quantitative properties with rewards. Example properties include the probability that a fault occurs and the expected number of faults in a given time period. We also describe the practical application of stochastic model checking with the probabilistic model checker PRISM by outlining the main features supported by PRISM and three real-world case studies: a probabilistic security protocol, dynamic power management and a biological pathway. More... »

PAGES

220-270

Book

TITLE

Formal Methods for Performance Evaluation

ISBN

978-3-540-72482-7
978-3-540-72522-0

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-540-72522-0_6

DOI

http://dx.doi.org/10.1007/978-3-540-72522-0_6

DIMENSIONS

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


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": "School of Computer Science, University of Birmingham, Edgbaston, Birmingham B15 2TT, United Kingdom", 
          "id": "http://www.grid.ac/institutes/grid.6572.6", 
          "name": [
            "School of Computer Science, University of Birmingham, Edgbaston, Birmingham B15 2TT, United Kingdom"
          ], 
          "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 Computer Science, University of Birmingham, Edgbaston, Birmingham B15 2TT, United Kingdom", 
          "id": "http://www.grid.ac/institutes/grid.6572.6", 
          "name": [
            "School of Computer Science, University of Birmingham, Edgbaston, Birmingham B15 2TT, United Kingdom"
          ], 
          "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": "School of Computer Science, University of Birmingham, Edgbaston, Birmingham B15 2TT, United Kingdom", 
          "id": "http://www.grid.ac/institutes/grid.6572.6", 
          "name": [
            "School of Computer Science, University of Birmingham, Edgbaston, Birmingham B15 2TT, United Kingdom"
          ], 
          "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": "2007-01-01", 
    "datePublishedReg": "2007-01-01", 
    "description": "This tutorial presents an overview of model checking for both discrete and continuous-time Markov chains (DTMCs and CTMCs). Model checking algorithms are given for verifying DTMCs and CTMCs against specifications written in probabilistic extensions of temporal logic, including quantitative properties with rewards. Example properties include the probability that a fault occurs and the expected number of faults in a given time period. We also describe the practical application of stochastic model checking with the probabilistic model checker PRISM by outlining the main features supported by PRISM and three real-world case studies: a probabilistic security protocol, dynamic power management and a biological pathway.", 
    "editor": [
      {
        "familyName": "Bernardo", 
        "givenName": "Marco", 
        "type": "Person"
      }, 
      {
        "familyName": "Hillston", 
        "givenName": "Jane", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-540-72522-0_6", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-540-72482-7", 
        "978-3-540-72522-0"
      ], 
      "name": "Formal Methods for Performance Evaluation", 
      "type": "Book"
    }, 
    "keywords": [
      "probabilistic model checker PRISM", 
      "model checking algorithm", 
      "model checker PRISM", 
      "real-world case study", 
      "stochastic model checking", 
      "dynamic power management", 
      "security protocols", 
      "number of faults", 
      "model checking", 
      "temporal logic", 
      "checking algorithm", 
      "probabilistic extension", 
      "power management", 
      "continuous-time Markov chain", 
      "example properties", 
      "quantitative properties", 
      "overview of models", 
      "Markov chain", 
      "main features", 
      "checking", 
      "case study", 
      "practical applications", 
      "algorithm", 
      "DTMC", 
      "tutorial", 
      "faults", 
      "specification", 
      "logic", 
      "CTMCs", 
      "protocol", 
      "model", 
      "applications", 
      "features", 
      "stochastic model", 
      "extension", 
      "management", 
      "overview", 
      "probability", 
      "number", 
      "reward", 
      "time period", 
      "biological pathways", 
      "chain", 
      "properties", 
      "prism", 
      "study", 
      "period", 
      "pathway"
    ], 
    "name": "Stochastic Model Checking", 
    "pagination": "220-270", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1012626164"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-540-72522-0_6"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-540-72522-0_6", 
      "https://app.dimensions.ai/details/publication/pub.1012626164"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-10T10:53", 
    "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_449.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-540-72522-0_6"
  }
]
 

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-540-72522-0_6'

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-540-72522-0_6'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-540-72522-0_6'

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-540-72522-0_6'


 

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

127 TRIPLES      23 PREDICATES      73 URIs      66 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-540-72522-0_6 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N68fcfb63ad60442599db1e086208d536
4 schema:datePublished 2007-01-01
5 schema:datePublishedReg 2007-01-01
6 schema:description This tutorial presents an overview of model checking for both discrete and continuous-time Markov chains (DTMCs and CTMCs). Model checking algorithms are given for verifying DTMCs and CTMCs against specifications written in probabilistic extensions of temporal logic, including quantitative properties with rewards. Example properties include the probability that a fault occurs and the expected number of faults in a given time period. We also describe the practical application of stochastic model checking with the probabilistic model checker PRISM by outlining the main features supported by PRISM and three real-world case studies: a probabilistic security protocol, dynamic power management and a biological pathway.
7 schema:editor Ne6cfc8f654494cb8ac7946f30f2ede60
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N6e905c4777434fbfb4eafbe5d82ecbdd
12 schema:keywords CTMCs
13 DTMC
14 Markov chain
15 algorithm
16 applications
17 biological pathways
18 case study
19 chain
20 checking
21 checking algorithm
22 continuous-time Markov chain
23 dynamic power management
24 example properties
25 extension
26 faults
27 features
28 logic
29 main features
30 management
31 model
32 model checker PRISM
33 model checking
34 model checking algorithm
35 number
36 number of faults
37 overview
38 overview of models
39 pathway
40 period
41 power management
42 practical applications
43 prism
44 probabilistic extension
45 probabilistic model checker PRISM
46 probability
47 properties
48 protocol
49 quantitative properties
50 real-world case study
51 reward
52 security protocols
53 specification
54 stochastic model
55 stochastic model checking
56 study
57 temporal logic
58 time period
59 tutorial
60 schema:name Stochastic Model Checking
61 schema:pagination 220-270
62 schema:productId N9bc56f59df9448bea4ea63e0df0bf22f
63 Ndec6418adfbe404c984d4b0d36025d60
64 schema:publisher Nab44bb6aa0cd4025aa274b416c981336
65 schema:sameAs https://app.dimensions.ai/details/publication/pub.1012626164
66 https://doi.org/10.1007/978-3-540-72522-0_6
67 schema:sdDatePublished 2022-05-10T10:53
68 schema:sdLicense https://scigraph.springernature.com/explorer/license/
69 schema:sdPublisher N7e2d06e801e9468799f58b1fa4d519d4
70 schema:url https://doi.org/10.1007/978-3-540-72522-0_6
71 sgo:license sg:explorer/license/
72 sgo:sdDataset chapters
73 rdf:type schema:Chapter
74 N45ee71c66bab4e95a23dbd5318afe78d rdf:first Nb8d3f881fcc24724929c490f2790abc5
75 rdf:rest rdf:nil
76 N68fcfb63ad60442599db1e086208d536 rdf:first sg:person.011375012273.39
77 rdf:rest N9740456fcd9d4f0f8cc55c0c0e901fe1
78 N6e905c4777434fbfb4eafbe5d82ecbdd schema:isbn 978-3-540-72482-7
79 978-3-540-72522-0
80 schema:name Formal Methods for Performance Evaluation
81 rdf:type schema:Book
82 N7e2d06e801e9468799f58b1fa4d519d4 schema:name Springer Nature - SN SciGraph project
83 rdf:type schema:Organization
84 N83b3a6aa4c574baa96e52baa343b05ee schema:familyName Bernardo
85 schema:givenName Marco
86 rdf:type schema:Person
87 N9740456fcd9d4f0f8cc55c0c0e901fe1 rdf:first sg:person.016323171577.36
88 rdf:rest Nb7dc312585624ef795201c900e6e4c68
89 N9bc56f59df9448bea4ea63e0df0bf22f schema:name dimensions_id
90 schema:value pub.1012626164
91 rdf:type schema:PropertyValue
92 Nab44bb6aa0cd4025aa274b416c981336 schema:name Springer Nature
93 rdf:type schema:Organisation
94 Nb7dc312585624ef795201c900e6e4c68 rdf:first sg:person.014007552600.37
95 rdf:rest rdf:nil
96 Nb8d3f881fcc24724929c490f2790abc5 schema:familyName Hillston
97 schema:givenName Jane
98 rdf:type schema:Person
99 Ndec6418adfbe404c984d4b0d36025d60 schema:name doi
100 schema:value 10.1007/978-3-540-72522-0_6
101 rdf:type schema:PropertyValue
102 Ne6cfc8f654494cb8ac7946f30f2ede60 rdf:first N83b3a6aa4c574baa96e52baa343b05ee
103 rdf:rest N45ee71c66bab4e95a23dbd5318afe78d
104 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
105 schema:name Information and Computing Sciences
106 rdf:type schema:DefinedTerm
107 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
108 schema:name Computation Theory and Mathematics
109 rdf:type schema:DefinedTerm
110 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.6572.6
111 schema:familyName Kwiatkowska
112 schema:givenName Marta
113 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
114 rdf:type schema:Person
115 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.6572.6
116 schema:familyName Parker
117 schema:givenName David
118 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
119 rdf:type schema:Person
120 sg:person.016323171577.36 schema:affiliation grid-institutes:grid.6572.6
121 schema:familyName Norman
122 schema:givenName Gethin
123 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36
124 rdf:type schema:Person
125 grid-institutes:grid.6572.6 schema:alternateName School of Computer Science, University of Birmingham, Edgbaston, Birmingham B15 2TT, United Kingdom
126 schema:name School of Computer Science, University of Birmingham, Edgbaston, Birmingham B15 2TT, United Kingdom
127 rdf:type schema:Organization
 




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


...