A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2009

AUTHORS

Jiří Barnat , Luboš Brim , Petr Ročkai

ABSTRACT

One of the most important open problems of parallel LTL model-checking is to design an on-the-fly scalable parallel algorithm with linear time complexity. Such an algorithm would give the optimality we have in sequential LTL model-checking. In this paper we give a partial solution to the problem. We propose an algorithm that has the required properties for a very rich subset of LTL properties, namely those expressible by weak Büchi automata. More... »

PAGES

407-425

Book

TITLE

Formal Methods and Software Engineering

ISBN

978-3-642-10372-8
978-3-642-10373-5

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-10373-5_21

DOI

http://dx.doi.org/10.1007/978-3-642-10373-5_21

DIMENSIONS

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


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": "Ro\u010dkai", 
        "givenName": "Petr", 
        "id": "sg:person.07377571657.86", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2009", 
    "datePublishedReg": "2009-01-01", 
    "description": "One of the most important open problems of parallel LTL model-checking is to design an on-the-fly scalable parallel algorithm with linear time complexity. Such an algorithm would give the optimality we have in sequential LTL model-checking. In this paper we give a partial solution to the problem. We propose an algorithm that has the required properties for a very rich subset of LTL properties, namely those expressible by weak B\u00fcchi automata.", 
    "editor": [
      {
        "familyName": "Breitman", 
        "givenName": "Karin", 
        "type": "Person"
      }, 
      {
        "familyName": "Cavalcanti", 
        "givenName": "Ana", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-10373-5_21", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-642-10372-8", 
        "978-3-642-10373-5"
      ], 
      "name": "Formal Methods and Software Engineering", 
      "type": "Book"
    }, 
    "keywords": [
      "parallel algorithm", 
      "important open problem", 
      "linear time complexity", 
      "Time Optimal", 
      "scalable parallel algorithm", 
      "open problem", 
      "time complexity", 
      "partial solution", 
      "algorithm", 
      "LTL properties", 
      "problem", 
      "optimality", 
      "model checking", 
      "properties", 
      "automata", 
      "solution", 
      "complexity", 
      "B\u00fcchi automata", 
      "rich subset", 
      "subset", 
      "checking", 
      "LTL", 
      "paper"
    ], 
    "name": "A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties", 
    "pagination": "407-425", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1039978342"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-10373-5_21"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-10373-5_21", 
      "https://app.dimensions.ai/details/publication/pub.1039978342"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-10T10:39", 
    "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_161.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-10373-5_21"
  }
]
 

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-10373-5_21'

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-10373-5_21'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-10373-5_21'

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-10373-5_21'


 

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

102 TRIPLES      23 PREDICATES      49 URIs      42 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-10373-5_21 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N21b1a702141747a8b129f28b91a279a0
4 schema:datePublished 2009
5 schema:datePublishedReg 2009-01-01
6 schema:description One of the most important open problems of parallel LTL model-checking is to design an on-the-fly scalable parallel algorithm with linear time complexity. Such an algorithm would give the optimality we have in sequential LTL model-checking. In this paper we give a partial solution to the problem. We propose an algorithm that has the required properties for a very rich subset of LTL properties, namely those expressible by weak Büchi automata.
7 schema:editor N2d823ec53d5c464783827adf9c3f1cdc
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf N6edadc6e5fc24b61ba6a32dada313fa3
12 schema:keywords Büchi automata
13 LTL
14 LTL properties
15 Time Optimal
16 algorithm
17 automata
18 checking
19 complexity
20 important open problem
21 linear time complexity
22 model checking
23 open problem
24 optimality
25 paper
26 parallel algorithm
27 partial solution
28 problem
29 properties
30 rich subset
31 scalable parallel algorithm
32 solution
33 subset
34 time complexity
35 schema:name A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties
36 schema:pagination 407-425
37 schema:productId N1246cf40d88f496e9d8221f08a7df0df
38 N6c4423f4ce184e6880e64aac07aefda0
39 schema:publisher Nb4e951195d854f8c915c2887ebafe4f5
40 schema:sameAs https://app.dimensions.ai/details/publication/pub.1039978342
41 https://doi.org/10.1007/978-3-642-10373-5_21
42 schema:sdDatePublished 2022-05-10T10:39
43 schema:sdLicense https://scigraph.springernature.com/explorer/license/
44 schema:sdPublisher N5f1f80b955f84b01b2c5096f2b5c44d3
45 schema:url https://doi.org/10.1007/978-3-642-10373-5_21
46 sgo:license sg:explorer/license/
47 sgo:sdDataset chapters
48 rdf:type schema:Chapter
49 N094e31749c6a436490d8aa00e7e161cc rdf:first sg:person.0645117057.83
50 rdf:rest N2ab5117528564c23afe17570cff6883c
51 N1246cf40d88f496e9d8221f08a7df0df schema:name doi
52 schema:value 10.1007/978-3-642-10373-5_21
53 rdf:type schema:PropertyValue
54 N21b1a702141747a8b129f28b91a279a0 rdf:first sg:person.011367557177.46
55 rdf:rest N094e31749c6a436490d8aa00e7e161cc
56 N2ab5117528564c23afe17570cff6883c rdf:first sg:person.07377571657.86
57 rdf:rest rdf:nil
58 N2d823ec53d5c464783827adf9c3f1cdc rdf:first Nce4f99dc9d794fc4a152afb840c9511b
59 rdf:rest Ne2954d1c569542588eec6f9ae425441c
60 N4365bb6612de40fea99d4d884e38e5d6 schema:familyName Cavalcanti
61 schema:givenName Ana
62 rdf:type schema:Person
63 N5f1f80b955f84b01b2c5096f2b5c44d3 schema:name Springer Nature - SN SciGraph project
64 rdf:type schema:Organization
65 N6c4423f4ce184e6880e64aac07aefda0 schema:name dimensions_id
66 schema:value pub.1039978342
67 rdf:type schema:PropertyValue
68 N6edadc6e5fc24b61ba6a32dada313fa3 schema:isbn 978-3-642-10372-8
69 978-3-642-10373-5
70 schema:name Formal Methods and Software Engineering
71 rdf:type schema:Book
72 Nb4e951195d854f8c915c2887ebafe4f5 schema:name Springer Nature
73 rdf:type schema:Organisation
74 Nce4f99dc9d794fc4a152afb840c9511b schema:familyName Breitman
75 schema:givenName Karin
76 rdf:type schema:Person
77 Ne2954d1c569542588eec6f9ae425441c rdf:first N4365bb6612de40fea99d4d884e38e5d6
78 rdf:rest rdf:nil
79 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
80 schema:name Information and Computing Sciences
81 rdf:type schema:DefinedTerm
82 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
83 schema:name Computation Theory and Mathematics
84 rdf:type schema:DefinedTerm
85 sg:person.011367557177.46 schema:affiliation grid-institutes:grid.10267.32
86 schema:familyName Barnat
87 schema:givenName Jiří
88 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46
89 rdf:type schema:Person
90 sg:person.0645117057.83 schema:affiliation grid-institutes:grid.10267.32
91 schema:familyName Brim
92 schema:givenName Luboš
93 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0645117057.83
94 rdf:type schema:Person
95 sg:person.07377571657.86 schema:affiliation grid-institutes:grid.10267.32
96 schema:familyName Ročkai
97 schema:givenName Petr
98 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86
99 rdf:type schema:Person
100 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
101 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
102 rdf:type schema:Organization
 




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


...