Partial Order Reduction for State/Event LTL View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2009

AUTHORS

Nikola Beneš , Lubos Brim , Ivana Černá , Jiri Sochor , Pavlina Vařeková , Barbora Zimmerova

ABSTRACT

Software systems assembled from a large number of autonomous components become an interesting target for formal verification due to the issue of correct interplay in component interaction. State/event LTL [1,2] incorporates both states and events to express important properties of component-based software systems.The main contribution of the paper is a partial order reduction technique for verification of state/event LTL properties. The core of the partial order reduction is a novel notion of stuttering equivalence which we call state/event stuttering equivalence. The positive attribute of the equivalence is that it can be resolved with existing methods for partial order reduction. State/event LTL properties are, in general, not preserved under state/event stuttering equivalence. To this end we define a new logic, called weak state/event LTL, which is invariant under the new equivalence. More... »

PAGES

307-321

Book

TITLE

Integrated Formal Methods

ISBN

978-3-642-00254-0
978-3-642-00255-7

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-00255-7_21

DOI

http://dx.doi.org/10.1007/978-3-642-00255-7_21

DIMENSIONS

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


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/0803", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computer Software", 
        "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": "Bene\u0161", 
        "givenName": "Nikola", 
        "id": "sg:person.014465763501.21", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014465763501.21"
        ], 
        "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": "Lubos", 
        "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": "Sochor", 
        "givenName": "Jiri", 
        "id": "sg:person.0753572720.98", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0753572720.98"
        ], 
        "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": "Va\u0159ekov\u00e1", 
        "givenName": "Pavlina", 
        "id": "sg:person.07724757205.02", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07724757205.02"
        ], 
        "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": "Zimmerova", 
        "givenName": "Barbora", 
        "id": "sg:person.010107275221.58", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010107275221.58"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2009", 
    "datePublishedReg": "2009-01-01", 
    "description": "Software systems assembled from a large number of autonomous components become an interesting target for formal verification due to the issue of correct interplay in component interaction. State/event LTL [1,2] incorporates both states and events to express important properties of component-based software systems.The main contribution of the paper is a partial order reduction technique for verification of state/event LTL properties. The core of the partial order reduction is a novel notion of stuttering equivalence which we call state/event stuttering equivalence. The positive attribute of the equivalence is that it can be resolved with existing methods for partial order reduction. State/event LTL properties are, in general, not preserved under state/event stuttering equivalence. To this end we define a new logic, called weak state/event LTL, which is invariant under the new equivalence.", 
    "editor": [
      {
        "familyName": "Leuschel", 
        "givenName": "Michael", 
        "type": "Person"
      }, 
      {
        "familyName": "Wehrheim", 
        "givenName": "Heike", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-00255-7_21", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-642-00254-0", 
        "978-3-642-00255-7"
      ], 
      "name": "Integrated Formal Methods", 
      "type": "Book"
    }, 
    "keywords": [
      "partial order reduction", 
      "states/events", 
      "software systems", 
      "LTL properties", 
      "component-based software systems", 
      "partial order reduction technique", 
      "formal verification", 
      "autonomous components", 
      "novel notion", 
      "main contribution", 
      "component interactions", 
      "LTL", 
      "reduction techniques", 
      "verification", 
      "order reduction", 
      "new logic", 
      "large number", 
      "order reduction techniques", 
      "important properties", 
      "correct interplay", 
      "system", 
      "logic", 
      "attributes", 
      "issues", 
      "technique", 
      "new equivalence", 
      "equivalence", 
      "method", 
      "notion", 
      "number", 
      "core", 
      "end", 
      "components", 
      "state", 
      "events", 
      "contribution", 
      "interaction", 
      "interesting target", 
      "positive attributes", 
      "target", 
      "properties", 
      "reduction", 
      "interplay", 
      "paper"
    ], 
    "name": "Partial Order Reduction for State/Event LTL", 
    "pagination": "307-321", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1049262684"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-00255-7_21"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-00255-7_21", 
      "https://app.dimensions.ai/details/publication/pub.1049262684"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-20T07:45", 
    "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_310.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-00255-7_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-00255-7_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-00255-7_21'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-00255-7_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-00255-7_21'


 

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

144 TRIPLES      23 PREDICATES      70 URIs      63 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-00255-7_21 schema:about anzsrc-for:08
2 anzsrc-for:0803
3 schema:author N4b1733cb21334ba48a7da86324d74819
4 schema:datePublished 2009
5 schema:datePublishedReg 2009-01-01
6 schema:description Software systems assembled from a large number of autonomous components become an interesting target for formal verification due to the issue of correct interplay in component interaction. State/event LTL [1,2] incorporates both states and events to express important properties of component-based software systems.The main contribution of the paper is a partial order reduction technique for verification of state/event LTL properties. The core of the partial order reduction is a novel notion of stuttering equivalence which we call state/event stuttering equivalence. The positive attribute of the equivalence is that it can be resolved with existing methods for partial order reduction. State/event LTL properties are, in general, not preserved under state/event stuttering equivalence. To this end we define a new logic, called weak state/event LTL, which is invariant under the new equivalence.
7 schema:editor Nbb14344247244212aa981f781e8c26fa
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N4c10883a77d44a8ea0dd0b78a80f282e
12 schema:keywords LTL
13 LTL properties
14 attributes
15 autonomous components
16 component interactions
17 component-based software systems
18 components
19 contribution
20 core
21 correct interplay
22 end
23 equivalence
24 events
25 formal verification
26 important properties
27 interaction
28 interesting target
29 interplay
30 issues
31 large number
32 logic
33 main contribution
34 method
35 new equivalence
36 new logic
37 notion
38 novel notion
39 number
40 order reduction
41 order reduction techniques
42 paper
43 partial order reduction
44 partial order reduction technique
45 positive attributes
46 properties
47 reduction
48 reduction techniques
49 software systems
50 state
51 states/events
52 system
53 target
54 technique
55 verification
56 schema:name Partial Order Reduction for State/Event LTL
57 schema:pagination 307-321
58 schema:productId N5f482a9edc9946b69142b41b5d63d8c6
59 Nd02f968a148a4dd1af68df14984f9c06
60 schema:publisher N52b4c436bdff4c8290601fd287ad5acc
61 schema:sameAs https://app.dimensions.ai/details/publication/pub.1049262684
62 https://doi.org/10.1007/978-3-642-00255-7_21
63 schema:sdDatePublished 2022-05-20T07:45
64 schema:sdLicense https://scigraph.springernature.com/explorer/license/
65 schema:sdPublisher N5e1c5cd17249474381fde1fc2c105289
66 schema:url https://doi.org/10.1007/978-3-642-00255-7_21
67 sgo:license sg:explorer/license/
68 sgo:sdDataset chapters
69 rdf:type schema:Chapter
70 N192f77dee647400a8bedfa09f7d0e769 rdf:first sg:person.010107275221.58
71 rdf:rest rdf:nil
72 N1c5c456f47fc44d287a24a03e314c2c1 schema:familyName Leuschel
73 schema:givenName Michael
74 rdf:type schema:Person
75 N2d0b5405ec9a4bb695f0695e1c0e4a62 rdf:first Ne1eb5b072e0d4a1a99fab130abd95779
76 rdf:rest rdf:nil
77 N2ffe54030b0242ae953233e364c4d477 rdf:first sg:person.07724757205.02
78 rdf:rest N192f77dee647400a8bedfa09f7d0e769
79 N4b1733cb21334ba48a7da86324d74819 rdf:first sg:person.014465763501.21
80 rdf:rest N523be9b0773c43899be9deff40f5e1d3
81 N4c10883a77d44a8ea0dd0b78a80f282e schema:isbn 978-3-642-00254-0
82 978-3-642-00255-7
83 schema:name Integrated Formal Methods
84 rdf:type schema:Book
85 N4e193d3822554224ba68066e2667c4b9 rdf:first sg:person.016355636647.31
86 rdf:rest Nfbf537697df6414c8e0482a884e22c04
87 N523be9b0773c43899be9deff40f5e1d3 rdf:first sg:person.0645117057.83
88 rdf:rest N4e193d3822554224ba68066e2667c4b9
89 N52b4c436bdff4c8290601fd287ad5acc schema:name Springer Nature
90 rdf:type schema:Organisation
91 N5e1c5cd17249474381fde1fc2c105289 schema:name Springer Nature - SN SciGraph project
92 rdf:type schema:Organization
93 N5f482a9edc9946b69142b41b5d63d8c6 schema:name dimensions_id
94 schema:value pub.1049262684
95 rdf:type schema:PropertyValue
96 Nbb14344247244212aa981f781e8c26fa rdf:first N1c5c456f47fc44d287a24a03e314c2c1
97 rdf:rest N2d0b5405ec9a4bb695f0695e1c0e4a62
98 Nd02f968a148a4dd1af68df14984f9c06 schema:name doi
99 schema:value 10.1007/978-3-642-00255-7_21
100 rdf:type schema:PropertyValue
101 Ne1eb5b072e0d4a1a99fab130abd95779 schema:familyName Wehrheim
102 schema:givenName Heike
103 rdf:type schema:Person
104 Nfbf537697df6414c8e0482a884e22c04 rdf:first sg:person.0753572720.98
105 rdf:rest N2ffe54030b0242ae953233e364c4d477
106 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
107 schema:name Information and Computing Sciences
108 rdf:type schema:DefinedTerm
109 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
110 schema:name Computer Software
111 rdf:type schema:DefinedTerm
112 sg:person.010107275221.58 schema:affiliation grid-institutes:grid.10267.32
113 schema:familyName Zimmerova
114 schema:givenName Barbora
115 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010107275221.58
116 rdf:type schema:Person
117 sg:person.014465763501.21 schema:affiliation grid-institutes:grid.10267.32
118 schema:familyName Beneš
119 schema:givenName Nikola
120 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014465763501.21
121 rdf:type schema:Person
122 sg:person.016355636647.31 schema:affiliation grid-institutes:grid.10267.32
123 schema:familyName Černá
124 schema:givenName Ivana
125 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016355636647.31
126 rdf:type schema:Person
127 sg:person.0645117057.83 schema:affiliation grid-institutes:grid.10267.32
128 schema:familyName Brim
129 schema:givenName Lubos
130 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0645117057.83
131 rdf:type schema:Person
132 sg:person.0753572720.98 schema:affiliation grid-institutes:grid.10267.32
133 schema:familyName Sochor
134 schema:givenName Jiri
135 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0753572720.98
136 rdf:type schema:Person
137 sg:person.07724757205.02 schema:affiliation grid-institutes:grid.10267.32
138 schema:familyName Vařeková
139 schema:givenName Pavlina
140 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07724757205.02
141 rdf:type schema:Person
142 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
143 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
144 rdf:type schema:Organization
 




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


...