Quantitative Verification Techniques for Biological Processes View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2009-08-13

AUTHORS

Marta Kwiatkowska , Gethin Norman , David Parker

ABSTRACT

Probabilistic model checking is a formal verification framework for systems which exhibit stochastic behavior. It has been successfully applied to a wide range of domains, including security and communication protocols, distributed algorithms and power management. In this chapter, we demonstrate its applicability to the analysis of biological pathways and show how it can yield a better understanding of the dynamics of these systems. Through a case study of the Mitogen-Activated Protein (MAP), Kinase cascade, we explain how biological pathways can be modeled in the probabilistic model checker PRISM and how this enables the analysis of a rich selection of quantitative properties. More... »

PAGES

391-409

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-540-88869-7_20

DOI

http://dx.doi.org/10.1007/978-3-540-88869-7_20

DIMENSIONS

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


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/0801", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Artificial Intelligence and Image Processing", 
        "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"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0803", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computer Software", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Oxford University Computing Laboratory, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Oxford University Computing Laboratory, Wolfson Building, 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": "Oxford University Computing Laboratory, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Oxford University Computing Laboratory, Wolfson Building, Parks Road, OX1 3QD, Oxford, 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": "Oxford University Computing Laboratory, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Oxford University Computing Laboratory, Wolfson Building, 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"
      }
    ], 
    "datePublished": "2009-08-13", 
    "datePublishedReg": "2009-08-13", 
    "description": "Probabilistic model checking is a formal verification framework for systems which exhibit stochastic behavior. It has been successfully applied to a wide range of domains, including security and communication protocols, distributed algorithms and power management. In this chapter, we demonstrate its applicability to the analysis of biological pathways and show how it can yield a better understanding of the dynamics of these systems. Through a case study of the Mitogen-Activated Protein (MAP), Kinase cascade, we explain how biological pathways can be modeled in the probabilistic model checker PRISM and how this enables the analysis of a rich selection of quantitative properties.", 
    "editor": [
      {
        "familyName": "Condon", 
        "givenName": "Anne", 
        "type": "Person"
      }, 
      {
        "familyName": "Harel", 
        "givenName": "David", 
        "type": "Person"
      }, 
      {
        "familyName": "Kok", 
        "givenName": "Joost N.", 
        "type": "Person"
      }, 
      {
        "familyName": "Salomaa", 
        "givenName": "Arto", 
        "type": "Person"
      }, 
      {
        "familyName": "Winfree", 
        "givenName": "Erik", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-540-88869-7_20", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-540-88868-0", 
        "978-3-540-88869-7"
      ], 
      "name": "Algorithmic Bioprocesses", 
      "type": "Book"
    }, 
    "keywords": [
      "formal verification framework", 
      "probabilistic model checker PRISM", 
      "quantitative verification techniques", 
      "probabilistic model checking", 
      "model checker PRISM", 
      "verification framework", 
      "verification techniques", 
      "model checking", 
      "communication protocols", 
      "Mitogen-Activated Protein", 
      "power management", 
      "rich selection", 
      "quantitative properties", 
      "checking", 
      "case study", 
      "security", 
      "algorithm", 
      "stochastic behavior", 
      "system", 
      "framework", 
      "protocol", 
      "wide range", 
      "domain", 
      "applicability", 
      "technique", 
      "selection", 
      "management", 
      "process", 
      "biological pathways", 
      "analysis", 
      "better understanding", 
      "chapter", 
      "behavior", 
      "dynamics", 
      "understanding", 
      "biological processes", 
      "range", 
      "prism", 
      "properties", 
      "study", 
      "pathway", 
      "protein", 
      "kinase"
    ], 
    "name": "Quantitative Verification Techniques for Biological Processes", 
    "pagination": "391-409", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1020553924"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-540-88869-7_20"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-540-88869-7_20", 
      "https://app.dimensions.ai/details/publication/pub.1020553924"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-20T07:43", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220519/entities/gbq_results/chapter/chapter_209.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-540-88869-7_20"
  }
]
 

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-88869-7_20'

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-88869-7_20'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-540-88869-7_20'

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-88869-7_20'


 

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

145 TRIPLES      23 PREDICATES      69 URIs      60 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-540-88869-7_20 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 anzsrc-for:0802
4 anzsrc-for:0803
5 schema:author Naa00f6751a0f4c6f9ffb092862167697
6 schema:datePublished 2009-08-13
7 schema:datePublishedReg 2009-08-13
8 schema:description Probabilistic model checking is a formal verification framework for systems which exhibit stochastic behavior. It has been successfully applied to a wide range of domains, including security and communication protocols, distributed algorithms and power management. In this chapter, we demonstrate its applicability to the analysis of biological pathways and show how it can yield a better understanding of the dynamics of these systems. Through a case study of the Mitogen-Activated Protein (MAP), Kinase cascade, we explain how biological pathways can be modeled in the probabilistic model checker PRISM and how this enables the analysis of a rich selection of quantitative properties.
9 schema:editor N3d95ea05a8c24ccb8f624e34c7f6b92a
10 schema:genre chapter
11 schema:inLanguage en
12 schema:isAccessibleForFree true
13 schema:isPartOf Nc866b575ac7a4a4e930ca607984688bf
14 schema:keywords Mitogen-Activated Protein
15 algorithm
16 analysis
17 applicability
18 behavior
19 better understanding
20 biological pathways
21 biological processes
22 case study
23 chapter
24 checking
25 communication protocols
26 domain
27 dynamics
28 formal verification framework
29 framework
30 kinase
31 management
32 model checker PRISM
33 model checking
34 pathway
35 power management
36 prism
37 probabilistic model checker PRISM
38 probabilistic model checking
39 process
40 properties
41 protein
42 protocol
43 quantitative properties
44 quantitative verification techniques
45 range
46 rich selection
47 security
48 selection
49 stochastic behavior
50 study
51 system
52 technique
53 understanding
54 verification framework
55 verification techniques
56 wide range
57 schema:name Quantitative Verification Techniques for Biological Processes
58 schema:pagination 391-409
59 schema:productId N661b777e46c743909e04bd595a8e86c1
60 N8754af6aa0464fb6aa70dadb35cf6016
61 schema:publisher Ncb1df7f0e6124112b1775ae2792bd1e7
62 schema:sameAs https://app.dimensions.ai/details/publication/pub.1020553924
63 https://doi.org/10.1007/978-3-540-88869-7_20
64 schema:sdDatePublished 2022-05-20T07:43
65 schema:sdLicense https://scigraph.springernature.com/explorer/license/
66 schema:sdPublisher N731b5537f33c432e8a5eaa5d00fdb26a
67 schema:url https://doi.org/10.1007/978-3-540-88869-7_20
68 sgo:license sg:explorer/license/
69 sgo:sdDataset chapters
70 rdf:type schema:Chapter
71 N0a622abcffd543e194546ffa75e59293 schema:familyName Salomaa
72 schema:givenName Arto
73 rdf:type schema:Person
74 N267f950444fb44deb06a69c17e63348e rdf:first sg:person.016323171577.36
75 rdf:rest Nb9995b36ed544710bd49fa9e5c46a7b7
76 N3d95ea05a8c24ccb8f624e34c7f6b92a rdf:first Nb1abf56847a0480c86e34e984c2e6791
77 rdf:rest Nfcd99f65f3164786b01e367a3a2259aa
78 N558e8d00843541eca5c12f7a00c11a5a schema:familyName Harel
79 schema:givenName David
80 rdf:type schema:Person
81 N661b777e46c743909e04bd595a8e86c1 schema:name doi
82 schema:value 10.1007/978-3-540-88869-7_20
83 rdf:type schema:PropertyValue
84 N73042a30c6a04122bfbc42091aa76c26 schema:familyName Winfree
85 schema:givenName Erik
86 rdf:type schema:Person
87 N731b5537f33c432e8a5eaa5d00fdb26a schema:name Springer Nature - SN SciGraph project
88 rdf:type schema:Organization
89 N750770f5c7554943ad23c97f33607547 rdf:first N0a622abcffd543e194546ffa75e59293
90 rdf:rest Nd7e7c69f8cb3477a9db05c1186615e1b
91 N8754af6aa0464fb6aa70dadb35cf6016 schema:name dimensions_id
92 schema:value pub.1020553924
93 rdf:type schema:PropertyValue
94 Naa00f6751a0f4c6f9ffb092862167697 rdf:first sg:person.011375012273.39
95 rdf:rest N267f950444fb44deb06a69c17e63348e
96 Nb1abf56847a0480c86e34e984c2e6791 schema:familyName Condon
97 schema:givenName Anne
98 rdf:type schema:Person
99 Nb789cc0eea3148f1935f6d0d12d54fb2 schema:familyName Kok
100 schema:givenName Joost N.
101 rdf:type schema:Person
102 Nb9995b36ed544710bd49fa9e5c46a7b7 rdf:first sg:person.014007552600.37
103 rdf:rest rdf:nil
104 Nc866b575ac7a4a4e930ca607984688bf schema:isbn 978-3-540-88868-0
105 978-3-540-88869-7
106 schema:name Algorithmic Bioprocesses
107 rdf:type schema:Book
108 Ncb1df7f0e6124112b1775ae2792bd1e7 schema:name Springer Nature
109 rdf:type schema:Organisation
110 Nd67b9c208b9445c89ac7e6138bc920d6 rdf:first Nb789cc0eea3148f1935f6d0d12d54fb2
111 rdf:rest N750770f5c7554943ad23c97f33607547
112 Nd7e7c69f8cb3477a9db05c1186615e1b rdf:first N73042a30c6a04122bfbc42091aa76c26
113 rdf:rest rdf:nil
114 Nfcd99f65f3164786b01e367a3a2259aa rdf:first N558e8d00843541eca5c12f7a00c11a5a
115 rdf:rest Nd67b9c208b9445c89ac7e6138bc920d6
116 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
117 schema:name Information and Computing Sciences
118 rdf:type schema:DefinedTerm
119 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
120 schema:name Artificial Intelligence and Image Processing
121 rdf:type schema:DefinedTerm
122 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
123 schema:name Computation Theory and Mathematics
124 rdf:type schema:DefinedTerm
125 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
126 schema:name Computer Software
127 rdf:type schema:DefinedTerm
128 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
129 schema:familyName Kwiatkowska
130 schema:givenName Marta
131 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
132 rdf:type schema:Person
133 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.4991.5
134 schema:familyName Parker
135 schema:givenName David
136 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
137 rdf:type schema:Person
138 sg:person.016323171577.36 schema:affiliation grid-institutes:grid.4991.5
139 schema:familyName Norman
140 schema:givenName Gethin
141 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36
142 rdf:type schema:Person
143 grid-institutes:grid.4991.5 schema:alternateName Oxford University Computing Laboratory, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK
144 schema:name Oxford University Computing Laboratory, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK
145 rdf:type schema:Organization
 




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


...