Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2014

AUTHORS

Alessandro Abate , Marta Kwiatkowska , Gethin Norman , David Parker

ABSTRACT

This paper concerns labelled Markov processes (LMPs), probabilistic models over uncountable state spaces originally introduced by Prakash Panangaden and colleagues. Motivated by the practical application of the LMP framework, we study its formal semantics and the relationship to similar models formulated in control theory. We consider notions of (exact and approximate) probabilistic bisimulation over LMPs and, drawing on methods from both formal verification and control theory, propose a simple technique to compute an approximate probabilistic bisimulation of a given LMP, where the resulting abstraction is characterised as a finite-state labelled Markov chain (LMC). This construction enables the application of automated quantitative verification and policy synthesis techniques over the obtained abstract model, which can be used to perform approximate analysis of the concrete LMP. We illustrate this process through a case study of a multi-room heating system that employs the probabilistic model checker PRISM. More... »

PAGES

40-58

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-06880-0_2

DOI

http://dx.doi.org/10.1007/978-3-319-06880-0_2

DIMENSIONS

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


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": "Department of Computer Science, University of Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Abate", 
        "givenName": "Alessandro", 
        "id": "sg:person.012500146711.49", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012500146711.49"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of 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, UK", 
          "id": "http://www.grid.ac/institutes/grid.8756.c", 
          "name": [
            "School of Computing Science, University of 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": "School of Computer Science, University of Birmingham, UK", 
          "id": "http://www.grid.ac/institutes/grid.6572.6", 
          "name": [
            "School of Computer Science, University of Birmingham, 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"
      }
    ], 
    "datePublished": "2014", 
    "datePublishedReg": "2014-01-01", 
    "description": "This paper concerns labelled Markov processes (LMPs), probabilistic models over uncountable state spaces originally introduced by Prakash Panangaden and colleagues. Motivated by the practical application of the LMP framework, we study its formal semantics and the relationship to similar models formulated in control theory. We consider notions of (exact and approximate) probabilistic bisimulation over LMPs and, drawing on methods from both formal verification and control theory, propose a simple technique to compute an approximate probabilistic bisimulation of a given LMP, where the resulting abstraction is characterised as a finite-state labelled Markov chain (LMC). This construction enables the application of automated quantitative verification and policy synthesis techniques over the obtained abstract model, which can be used to perform approximate analysis of the concrete LMP. We illustrate this process through a case study of a multi-room heating system that employs the probabilistic model checker PRISM.", 
    "editor": [
      {
        "familyName": "van Breugel", 
        "givenName": "Franck", 
        "type": "Person"
      }, 
      {
        "familyName": "Kashefi", 
        "givenName": "Elham", 
        "type": "Person"
      }, 
      {
        "familyName": "Palamidessi", 
        "givenName": "Catuscia", 
        "type": "Person"
      }, 
      {
        "familyName": "Rutten", 
        "givenName": "Jan", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-06880-0_2", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-319-06879-4", 
        "978-3-319-06880-0"
      ], 
      "name": "Horizons of the Mind. A Tribute to Prakash Panangaden", 
      "type": "Book"
    }, 
    "keywords": [
      "control theory", 
      "Markov process", 
      "uncountable state space", 
      "Labelled Markov Processes", 
      "approximate bisimulation", 
      "Markov chain", 
      "state space", 
      "approximate analysis", 
      "probabilistic model checking", 
      "probabilistic model", 
      "probabilistic bisimulation", 
      "probabilistic model checker PRISM", 
      "abstract model", 
      "paper concerns", 
      "practical applications", 
      "bisimulation", 
      "model checker PRISM", 
      "similar models", 
      "theory", 
      "Panangaden", 
      "model checking", 
      "model", 
      "quantitative verification", 
      "synthesis technique", 
      "space", 
      "LMP", 
      "applications", 
      "technique", 
      "case study", 
      "framework", 
      "verification", 
      "notion", 
      "construction", 
      "system", 
      "simple technique", 
      "heating system", 
      "process", 
      "checking", 
      "abstraction", 
      "formal verification", 
      "analysis", 
      "chain", 
      "semantics", 
      "formal semantics", 
      "relationship", 
      "prism", 
      "study", 
      "concern", 
      "colleagues", 
      "method", 
      "Prakash Panangaden", 
      "LMP framework", 
      "approximate probabilistic bisimulation", 
      "policy synthesis techniques", 
      "concrete LMP", 
      "multi-room heating system", 
      "checker PRISM", 
      "Finite Approximate Bisimulations"
    ], 
    "name": "Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations", 
    "pagination": "40-58", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1053551353"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-06880-0_2"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-06880-0_2", 
      "https://app.dimensions.ai/details/publication/pub.1053551353"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-12-01T20:10", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20211201/entities/gbq_results/chapter/chapter_427.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-06880-0_2"
  }
]
 

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-06880-0_2'

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-06880-0_2'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-06880-0_2'

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-06880-0_2'


 

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

160 TRIPLES      23 PREDICATES      84 URIs      77 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-06880-0_2 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N7ba276f712cc4edc884e79842c2e8b9f
4 schema:datePublished 2014
5 schema:datePublishedReg 2014-01-01
6 schema:description This paper concerns labelled Markov processes (LMPs), probabilistic models over uncountable state spaces originally introduced by Prakash Panangaden and colleagues. Motivated by the practical application of the LMP framework, we study its formal semantics and the relationship to similar models formulated in control theory. We consider notions of (exact and approximate) probabilistic bisimulation over LMPs and, drawing on methods from both formal verification and control theory, propose a simple technique to compute an approximate probabilistic bisimulation of a given LMP, where the resulting abstraction is characterised as a finite-state labelled Markov chain (LMC). This construction enables the application of automated quantitative verification and policy synthesis techniques over the obtained abstract model, which can be used to perform approximate analysis of the concrete LMP. We illustrate this process through a case study of a multi-room heating system that employs the probabilistic model checker PRISM.
7 schema:editor N9dae68a582534294881a7645694fea7b
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N824f592e45a64fc2a868c9ca7c8402fb
12 schema:keywords Finite Approximate Bisimulations
13 LMP
14 LMP framework
15 Labelled Markov Processes
16 Markov chain
17 Markov process
18 Panangaden
19 Prakash Panangaden
20 abstract model
21 abstraction
22 analysis
23 applications
24 approximate analysis
25 approximate bisimulation
26 approximate probabilistic bisimulation
27 bisimulation
28 case study
29 chain
30 checker PRISM
31 checking
32 colleagues
33 concern
34 concrete LMP
35 construction
36 control theory
37 formal semantics
38 formal verification
39 framework
40 heating system
41 method
42 model
43 model checker PRISM
44 model checking
45 multi-room heating system
46 notion
47 paper concerns
48 policy synthesis techniques
49 practical applications
50 prism
51 probabilistic bisimulation
52 probabilistic model
53 probabilistic model checker PRISM
54 probabilistic model checking
55 process
56 quantitative verification
57 relationship
58 semantics
59 similar models
60 simple technique
61 space
62 state space
63 study
64 synthesis technique
65 system
66 technique
67 theory
68 uncountable state space
69 verification
70 schema:name Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations
71 schema:pagination 40-58
72 schema:productId Ned290f7e04994709bb32da072d5a7062
73 Nf9039b5ee475465bb9813761f310df5e
74 schema:publisher Nf35c691e3e084eb6896cd8763fca74e1
75 schema:sameAs https://app.dimensions.ai/details/publication/pub.1053551353
76 https://doi.org/10.1007/978-3-319-06880-0_2
77 schema:sdDatePublished 2021-12-01T20:10
78 schema:sdLicense https://scigraph.springernature.com/explorer/license/
79 schema:sdPublisher Nb7478c125342487f95df40cfb2b61637
80 schema:url https://doi.org/10.1007/978-3-319-06880-0_2
81 sgo:license sg:explorer/license/
82 sgo:sdDataset chapters
83 rdf:type schema:Chapter
84 N083c9ec6a6254eb68952580666b0f265 rdf:first sg:person.011375012273.39
85 rdf:rest Neaa6c5bca4a4431788d0dae2b3861b15
86 N0d4fbbdd854e4d3f97ba82d8da0352e5 schema:familyName Kashefi
87 schema:givenName Elham
88 rdf:type schema:Person
89 N2b30400fc2e6422a9c2dde52c789edba rdf:first sg:person.014007552600.37
90 rdf:rest rdf:nil
91 N362cbd953d2f4df990d50fa5d0956fa7 rdf:first Nfc3618abf0494f63965e886a1db0ea80
92 rdf:rest N694e7a8ff414444b8f053e89f7cff97f
93 N4c780f848dbe4330a427a37f39158f6b schema:familyName Rutten
94 schema:givenName Jan
95 rdf:type schema:Person
96 N694e7a8ff414444b8f053e89f7cff97f rdf:first N4c780f848dbe4330a427a37f39158f6b
97 rdf:rest rdf:nil
98 N7ba276f712cc4edc884e79842c2e8b9f rdf:first sg:person.012500146711.49
99 rdf:rest N083c9ec6a6254eb68952580666b0f265
100 N824f592e45a64fc2a868c9ca7c8402fb schema:isbn 978-3-319-06879-4
101 978-3-319-06880-0
102 schema:name Horizons of the Mind. A Tribute to Prakash Panangaden
103 rdf:type schema:Book
104 N9dae68a582534294881a7645694fea7b rdf:first Nd15efa9739d842ea847b4ddd11ab54ad
105 rdf:rest Nb09e225491884a749940af7a80006b2f
106 Nb09e225491884a749940af7a80006b2f rdf:first N0d4fbbdd854e4d3f97ba82d8da0352e5
107 rdf:rest N362cbd953d2f4df990d50fa5d0956fa7
108 Nb7478c125342487f95df40cfb2b61637 schema:name Springer Nature - SN SciGraph project
109 rdf:type schema:Organization
110 Nd15efa9739d842ea847b4ddd11ab54ad schema:familyName van Breugel
111 schema:givenName Franck
112 rdf:type schema:Person
113 Neaa6c5bca4a4431788d0dae2b3861b15 rdf:first sg:person.016323171577.36
114 rdf:rest N2b30400fc2e6422a9c2dde52c789edba
115 Ned290f7e04994709bb32da072d5a7062 schema:name dimensions_id
116 schema:value pub.1053551353
117 rdf:type schema:PropertyValue
118 Nf35c691e3e084eb6896cd8763fca74e1 schema:name Springer Nature
119 rdf:type schema:Organisation
120 Nf9039b5ee475465bb9813761f310df5e schema:name doi
121 schema:value 10.1007/978-3-319-06880-0_2
122 rdf:type schema:PropertyValue
123 Nfc3618abf0494f63965e886a1db0ea80 schema:familyName Palamidessi
124 schema:givenName Catuscia
125 rdf:type schema:Person
126 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
127 schema:name Information and Computing Sciences
128 rdf:type schema:DefinedTerm
129 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
130 schema:name Computation Theory and Mathematics
131 rdf:type schema:DefinedTerm
132 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
133 schema:familyName Kwiatkowska
134 schema:givenName Marta
135 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
136 rdf:type schema:Person
137 sg:person.012500146711.49 schema:affiliation grid-institutes:grid.4991.5
138 schema:familyName Abate
139 schema:givenName Alessandro
140 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012500146711.49
141 rdf:type schema:Person
142 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.6572.6
143 schema:familyName Parker
144 schema:givenName David
145 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
146 rdf:type schema:Person
147 sg:person.016323171577.36 schema:affiliation grid-institutes:grid.8756.c
148 schema:familyName Norman
149 schema:givenName Gethin
150 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36
151 rdf:type schema:Person
152 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, UK
153 schema:name Department of Computer Science, University of Oxford, UK
154 rdf:type schema:Organization
155 grid-institutes:grid.6572.6 schema:alternateName School of Computer Science, University of Birmingham, UK
156 schema:name School of Computer Science, University of Birmingham, UK
157 rdf:type schema:Organization
158 grid-institutes:grid.8756.c schema:alternateName School of Computing Science, University of Glasgow, UK
159 schema:name School of Computing Science, University of Glasgow, UK
160 rdf:type schema:Organization
 




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


...