Local Quantitative LTL Model Checking View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2009

AUTHORS

Jiří Barnat , Luboš Brim , Ivana Černá , Milan Češka , Jana Tůmová

ABSTRACT

Quantitative analysis of probabilistic systems has been studied mainly from the global model checking point of view. In the global model-checking, the goal of verification is to decide the probability of satisfaction of a given property for all reachable states in the state space of the system under investigation. On the other hand, in local model checking approach the probability of satisfaction is computed only for the set of initial states. In theory, it is possible to solve the local model checking problem using the global model checking approach. However, the global model checking procedure can be significantly outperformed by a dedicated local model checking one. In this paper we present several particular local model checking techniques that if applied to global model checking procedure reduce the runtime needed from days to minutes. More... »

PAGES

53-68

Book

TITLE

Formal Methods for Industrial Critical Systems

ISBN

978-3-642-03239-4
978-3-642-03240-0

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-03240-0_8

DOI

http://dx.doi.org/10.1007/978-3-642-03240-0_8

DIMENSIONS

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


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": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Barnat", 
        "givenName": "Ji\u0159\u00ed", 
        "id": "sg:person.011367557177.46", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Brim", 
        "givenName": "Lubo\u0161", 
        "id": "sg:person.0645117057.83", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0645117057.83"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "\u010cern\u00e1", 
        "givenName": "Ivana", 
        "id": "sg:person.016355636647.31", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016355636647.31"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "\u010ce\u0161ka", 
        "givenName": "Milan", 
        "id": "sg:person.016652663056.36", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016652663056.36"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "T\u016fmov\u00e1", 
        "givenName": "Jana", 
        "id": "sg:person.014762675647.44", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014762675647.44"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2009", 
    "datePublishedReg": "2009-01-01", 
    "description": "Quantitative analysis of probabilistic systems has been studied mainly from the global model checking point of view. In the global model-checking, the goal of verification is to decide the probability of satisfaction of a given property for all reachable states in the state space of the system under investigation. On the other hand, in local model checking approach the probability of satisfaction is computed only for the set of initial states. In theory, it is possible to solve the local model checking problem using the global model checking approach. However, the global model checking procedure can be significantly outperformed by a dedicated local model checking one. In this paper we present several particular local model checking techniques that if applied to global model checking procedure reduce the runtime needed from days to minutes.", 
    "editor": [
      {
        "familyName": "Cofer", 
        "givenName": "Darren", 
        "type": "Person"
      }, 
      {
        "familyName": "Fantechi", 
        "givenName": "Alessandro", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-03240-0_8", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-642-03239-4", 
        "978-3-642-03240-0"
      ], 
      "name": "Formal Methods for Industrial Critical Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "goal of verification", 
      "local models", 
      "probabilistic systems", 
      "LTL model", 
      "probability of satisfaction", 
      "reachable states", 
      "checking points", 
      "state space", 
      "global model", 
      "runtime", 
      "system", 
      "verification", 
      "model", 
      "set", 
      "probability", 
      "initial state", 
      "goal", 
      "space", 
      "technique", 
      "view", 
      "satisfaction", 
      "state", 
      "quantitative analysis", 
      "point", 
      "hand", 
      "theory", 
      "procedure", 
      "approach", 
      "problem", 
      "analysis", 
      "properties", 
      "investigation", 
      "minutes", 
      "days", 
      "paper"
    ], 
    "name": "Local Quantitative LTL Model Checking", 
    "pagination": "53-68", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1008146181"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-03240-0_8"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-03240-0_8", 
      "https://app.dimensions.ai/details/publication/pub.1008146181"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-20T07:46", 
    "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_347.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-03240-0_8"
  }
]
 

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-642-03240-0_8'

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-03240-0_8'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-03240-0_8'

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-03240-0_8'


 

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

128 TRIPLES      23 PREDICATES      61 URIs      54 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-03240-0_8 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N452e5af5aeda41f7af2f23b6ca0f1326
4 schema:datePublished 2009
5 schema:datePublishedReg 2009-01-01
6 schema:description Quantitative analysis of probabilistic systems has been studied mainly from the global model checking point of view. In the global model-checking, the goal of verification is to decide the probability of satisfaction of a given property for all reachable states in the state space of the system under investigation. On the other hand, in local model checking approach the probability of satisfaction is computed only for the set of initial states. In theory, it is possible to solve the local model checking problem using the global model checking approach. However, the global model checking procedure can be significantly outperformed by a dedicated local model checking one. In this paper we present several particular local model checking techniques that if applied to global model checking procedure reduce the runtime needed from days to minutes.
7 schema:editor N9ed1c706a4a24edd881585e829a4e0dc
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf Na05836a660cb4d219e2e4bf9c21f034f
12 schema:keywords LTL model
13 analysis
14 approach
15 checking points
16 days
17 global model
18 goal
19 goal of verification
20 hand
21 initial state
22 investigation
23 local models
24 minutes
25 model
26 paper
27 point
28 probabilistic systems
29 probability
30 probability of satisfaction
31 problem
32 procedure
33 properties
34 quantitative analysis
35 reachable states
36 runtime
37 satisfaction
38 set
39 space
40 state
41 state space
42 system
43 technique
44 theory
45 verification
46 view
47 schema:name Local Quantitative LTL Model Checking
48 schema:pagination 53-68
49 schema:productId N5329f48f92414eeca2a89d5fc97606ef
50 N96832cf0cf214a27934f06bacb77bfc0
51 schema:publisher Nf8beb6495e154e5e8786a893c4d20133
52 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008146181
53 https://doi.org/10.1007/978-3-642-03240-0_8
54 schema:sdDatePublished 2022-05-20T07:46
55 schema:sdLicense https://scigraph.springernature.com/explorer/license/
56 schema:sdPublisher Nfc4a60273f25452b8651950146020cbd
57 schema:url https://doi.org/10.1007/978-3-642-03240-0_8
58 sgo:license sg:explorer/license/
59 sgo:sdDataset chapters
60 rdf:type schema:Chapter
61 N33756853afec477dbc15d37838a788d0 schema:familyName Fantechi
62 schema:givenName Alessandro
63 rdf:type schema:Person
64 N3ed463022d7b49ccaf7737cca5790bd6 rdf:first sg:person.016355636647.31
65 rdf:rest N7d5d02197fa04bc4b6d372b20f514697
66 N4189ceee10b14633a322c4731dd7e364 schema:familyName Cofer
67 schema:givenName Darren
68 rdf:type schema:Person
69 N452e5af5aeda41f7af2f23b6ca0f1326 rdf:first sg:person.011367557177.46
70 rdf:rest N8dc63a3ac064423b8c5530a62c26ddc3
71 N47493f2c60d04826a6a4e6c758157126 rdf:first sg:person.014762675647.44
72 rdf:rest rdf:nil
73 N5329f48f92414eeca2a89d5fc97606ef schema:name doi
74 schema:value 10.1007/978-3-642-03240-0_8
75 rdf:type schema:PropertyValue
76 N5f9914d17f9746ddad50b6b530388298 rdf:first N33756853afec477dbc15d37838a788d0
77 rdf:rest rdf:nil
78 N7d5d02197fa04bc4b6d372b20f514697 rdf:first sg:person.016652663056.36
79 rdf:rest N47493f2c60d04826a6a4e6c758157126
80 N8dc63a3ac064423b8c5530a62c26ddc3 rdf:first sg:person.0645117057.83
81 rdf:rest N3ed463022d7b49ccaf7737cca5790bd6
82 N96832cf0cf214a27934f06bacb77bfc0 schema:name dimensions_id
83 schema:value pub.1008146181
84 rdf:type schema:PropertyValue
85 N9ed1c706a4a24edd881585e829a4e0dc rdf:first N4189ceee10b14633a322c4731dd7e364
86 rdf:rest N5f9914d17f9746ddad50b6b530388298
87 Na05836a660cb4d219e2e4bf9c21f034f schema:isbn 978-3-642-03239-4
88 978-3-642-03240-0
89 schema:name Formal Methods for Industrial Critical Systems
90 rdf:type schema:Book
91 Nf8beb6495e154e5e8786a893c4d20133 schema:name Springer Nature
92 rdf:type schema:Organisation
93 Nfc4a60273f25452b8651950146020cbd schema:name Springer Nature - SN SciGraph project
94 rdf:type schema:Organization
95 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
96 schema:name Information and Computing Sciences
97 rdf:type schema:DefinedTerm
98 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
99 schema:name Computation Theory and Mathematics
100 rdf:type schema:DefinedTerm
101 sg:person.011367557177.46 schema:affiliation grid-institutes:grid.10267.32
102 schema:familyName Barnat
103 schema:givenName Jiří
104 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46
105 rdf:type schema:Person
106 sg:person.014762675647.44 schema:affiliation grid-institutes:grid.10267.32
107 schema:familyName Tůmová
108 schema:givenName Jana
109 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014762675647.44
110 rdf:type schema:Person
111 sg:person.016355636647.31 schema:affiliation grid-institutes:grid.10267.32
112 schema:familyName Černá
113 schema:givenName Ivana
114 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016355636647.31
115 rdf:type schema:Person
116 sg:person.016652663056.36 schema:affiliation grid-institutes:grid.10267.32
117 schema:familyName Češka
118 schema:givenName Milan
119 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016652663056.36
120 rdf:type schema:Person
121 sg:person.0645117057.83 schema:affiliation grid-institutes:grid.10267.32
122 schema:familyName Brim
123 schema:givenName Luboš
124 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0645117057.83
125 rdf:type schema:Person
126 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
127 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
128 rdf:type schema:Organization
 




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


...