Verification of parallel systems via decomposition View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

1992

AUTHORS

Jan Friso Groote , Faron Moller

ABSTRACT

Recently, Milner and Moller have presented several decomposition results for processes. Inspired by these, we investigate decomposition techniques for the verification of parallel systems. In particular, we consider those of the form p1∥p2∥ ...∥pm = q1 ∥q2 ∥...∥qn (*) where piand qj are (finite-) state systems, and ∥denotes parallel composition. We provide a decomposition procedure for all pi and qj and give criteria that must be checked on the decomposed processes to see whether (*) does or does not hold. We analyse the complexity of our procedure and show that it is polynomial in n, m and the sizes of pi and qj if there is no communication. We also show that with communication the verification of (*) is co-NP hard, which makes it very unlikely that a polynomial complexity bound exists. But by applying our decomposition technique to Milner's cyclic scheduler we show that verification can become polynomial in space and time for practical examples, where standard techniques are exponential. More... »

PAGES

62-76

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/bfb0084783

DOI

http://dx.doi.org/10.1007/bfb0084783

DIMENSIONS

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


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": "CWI, Amsterdam", 
          "id": "http://www.grid.ac/institutes/grid.6054.7", 
          "name": [
            "CWI, Amsterdam"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Groote", 
        "givenName": "Jan Friso", 
        "id": "sg:person.010073156347.09", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010073156347.09"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Dept of Computer Science, University of Edinburgh, The King's Buildings, EH9 3JZ, Edinburgh, Scotland", 
          "id": "http://www.grid.ac/institutes/grid.4305.2", 
          "name": [
            "Dept of Computer Science, University of Edinburgh, The King's Buildings, EH9 3JZ, Edinburgh, Scotland"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Moller", 
        "givenName": "Faron", 
        "id": "sg:person.010425236217.29", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010425236217.29"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "1992", 
    "datePublishedReg": "1992-01-01", 
    "description": "Recently, Milner and Moller have presented several decomposition results for processes. Inspired by these, we investigate decomposition techniques for the verification of parallel systems. In particular, we consider those of the form p1\u2225p2\u2225 ...\u2225pm = q1 \u2225q2 \u2225...\u2225qn (*) where piand qj are (finite-) state systems, and \u2225denotes parallel composition. We provide a decomposition procedure for all pi and qj and give criteria that must be checked on the decomposed processes to see whether (*) does or does not hold. We analyse the complexity of our procedure and show that it is polynomial in n, m and the sizes of pi and qj if there is no communication. We also show that with communication the verification of (*) is co-NP hard, which makes it very unlikely that a polynomial complexity bound exists. But by applying our decomposition technique to Milner's cyclic scheduler we show that verification can become polynomial in space and time for practical examples, where standard techniques are exponential.", 
    "editor": [
      {
        "familyName": "Cleaveland", 
        "givenName": "W.R.", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/bfb0084783", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-540-55822-4"
      ], 
      "name": "CONCUR '92", 
      "type": "Book"
    }, 
    "keywords": [
      "parallel systems", 
      "decomposition technique", 
      "polynomial complexity", 
      "parallel composition", 
      "verification", 
      "Co NPs", 
      "practical examples", 
      "complexity", 
      "communication", 
      "scheduler", 
      "system", 
      "technique", 
      "decomposition procedure", 
      "decomposition results", 
      "standard techniques", 
      "space", 
      "process", 
      "example", 
      "state system", 
      "decomposition", 
      "Milner", 
      "PI", 
      "time", 
      "procedure", 
      "results", 
      "criteria", 
      "size", 
      "exists", 
      "form", 
      "Moller", 
      "composition", 
      "Q1"
    ], 
    "name": "Verification of parallel systems via decomposition", 
    "pagination": "62-76", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1016206183"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/bfb0084783"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/bfb0084783", 
      "https://app.dimensions.ai/details/publication/pub.1016206183"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-20T07:42", 
    "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_143.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/bfb0084783"
  }
]
 

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/bfb0084783'

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/bfb0084783'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/bfb0084783'

RDF/XML is a standard XML format for linked data.

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/bfb0084783'


 

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

101 TRIPLES      23 PREDICATES      58 URIs      51 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/bfb0084783 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author Nfc491fbb64e744d59a1a06f2452a5db2
4 schema:datePublished 1992
5 schema:datePublishedReg 1992-01-01
6 schema:description Recently, Milner and Moller have presented several decomposition results for processes. Inspired by these, we investigate decomposition techniques for the verification of parallel systems. In particular, we consider those of the form p1∥p2∥ ...∥pm = q1 ∥q2 ∥...∥qn (*) where piand qj are (finite-) state systems, and ∥denotes parallel composition. We provide a decomposition procedure for all pi and qj and give criteria that must be checked on the decomposed processes to see whether (*) does or does not hold. We analyse the complexity of our procedure and show that it is polynomial in n, m and the sizes of pi and qj if there is no communication. We also show that with communication the verification of (*) is co-NP hard, which makes it very unlikely that a polynomial complexity bound exists. But by applying our decomposition technique to Milner's cyclic scheduler we show that verification can become polynomial in space and time for practical examples, where standard techniques are exponential.
7 schema:editor N31633e5730bd43e897490a02643338ce
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N6fde822f7b3f4fd1b9e5eb563cc84576
12 schema:keywords Co NPs
13 Milner
14 Moller
15 PI
16 Q1
17 communication
18 complexity
19 composition
20 criteria
21 decomposition
22 decomposition procedure
23 decomposition results
24 decomposition technique
25 example
26 exists
27 form
28 parallel composition
29 parallel systems
30 polynomial complexity
31 practical examples
32 procedure
33 process
34 results
35 scheduler
36 size
37 space
38 standard techniques
39 state system
40 system
41 technique
42 time
43 verification
44 schema:name Verification of parallel systems via decomposition
45 schema:pagination 62-76
46 schema:productId Nd095a83f95924d55b0336e19aeb7133f
47 Nfeed726039a441aa81e90c96cafe3d6d
48 schema:publisher N53246b0e5d774af9801ae75daa7f8a5c
49 schema:sameAs https://app.dimensions.ai/details/publication/pub.1016206183
50 https://doi.org/10.1007/bfb0084783
51 schema:sdDatePublished 2022-05-20T07:42
52 schema:sdLicense https://scigraph.springernature.com/explorer/license/
53 schema:sdPublisher N4420b84f71a0401bb8a16dc8c40dc8d3
54 schema:url https://doi.org/10.1007/bfb0084783
55 sgo:license sg:explorer/license/
56 sgo:sdDataset chapters
57 rdf:type schema:Chapter
58 N218207d3b869490d83e8d021f1de4126 rdf:first sg:person.010425236217.29
59 rdf:rest rdf:nil
60 N31633e5730bd43e897490a02643338ce rdf:first Na960d2d7e7f5436ba2128ce5bc4253c6
61 rdf:rest rdf:nil
62 N4420b84f71a0401bb8a16dc8c40dc8d3 schema:name Springer Nature - SN SciGraph project
63 rdf:type schema:Organization
64 N53246b0e5d774af9801ae75daa7f8a5c schema:name Springer Nature
65 rdf:type schema:Organisation
66 N6fde822f7b3f4fd1b9e5eb563cc84576 schema:isbn 978-3-540-55822-4
67 schema:name CONCUR '92
68 rdf:type schema:Book
69 Na960d2d7e7f5436ba2128ce5bc4253c6 schema:familyName Cleaveland
70 schema:givenName W.R.
71 rdf:type schema:Person
72 Nd095a83f95924d55b0336e19aeb7133f schema:name dimensions_id
73 schema:value pub.1016206183
74 rdf:type schema:PropertyValue
75 Nfc491fbb64e744d59a1a06f2452a5db2 rdf:first sg:person.010073156347.09
76 rdf:rest N218207d3b869490d83e8d021f1de4126
77 Nfeed726039a441aa81e90c96cafe3d6d schema:name doi
78 schema:value 10.1007/bfb0084783
79 rdf:type schema:PropertyValue
80 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
81 schema:name Information and Computing Sciences
82 rdf:type schema:DefinedTerm
83 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
84 schema:name Computation Theory and Mathematics
85 rdf:type schema:DefinedTerm
86 sg:person.010073156347.09 schema:affiliation grid-institutes:grid.6054.7
87 schema:familyName Groote
88 schema:givenName Jan Friso
89 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010073156347.09
90 rdf:type schema:Person
91 sg:person.010425236217.29 schema:affiliation grid-institutes:grid.4305.2
92 schema:familyName Moller
93 schema:givenName Faron
94 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010425236217.29
95 rdf:type schema:Person
96 grid-institutes:grid.4305.2 schema:alternateName Dept of Computer Science, University of Edinburgh, The King's Buildings, EH9 3JZ, Edinburgh, Scotland
97 schema:name Dept of Computer Science, University of Edinburgh, The King's Buildings, EH9 3JZ, Edinburgh, Scotland
98 rdf:type schema:Organization
99 grid-institutes:grid.6054.7 schema:alternateName CWI, Amsterdam
100 schema:name CWI, Amsterdam
101 rdf:type schema:Organization
 




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


...