Weak Bisimulation Approximants View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2006

AUTHORS

Will Harwood , Faron Moller , Anton Setzer

ABSTRACT

Bisimilarity and weak bisimilarity ≈ are canonical notions of equivalence between processes, which are defined co-inductively, but may be approached – and even reached – by their (transfinite) inductively-defined approximants ~α and ≈α. For arbitrary processes this approximation may need to climb arbitrarily high through the infinite ordinals before stabilising. In this paper we consider a simple yet well-studied process algebra, the Basic Parallel Processes (BPP), and investigate for this class of processes the minimal ordinal α such that ≈ = ≈α.The main tool in our investigation is a novel proof of Dickson’s Lemma. Unlike classical proofs, the proof we provide gives rise to a tight ordinal bound, of ωn, on the order type of non-increasing sequences of n-tuples of natural numbers. With this we are able to reduce a long-standing bound on the approximation hierarchy for weak bisimilarity ≈ over BPP, and show that \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}${\approx} = {\approx_{\omega^\omega}}$\end{document}. More... »

PAGES

365-379

Book

TITLE

Computer Science Logic

ISBN

978-3-540-45458-8
978-3-540-45459-5

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/11874683_24

DOI

http://dx.doi.org/10.1007/11874683_24

DIMENSIONS

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


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/01", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Mathematical Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0101", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Pure Mathematics", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, Swansea University, Singleton Park, SA2 8PP, Sketty, Swansea, UK", 
          "id": "http://www.grid.ac/institutes/grid.4827.9", 
          "name": [
            "Department of Computer Science, Swansea University, Singleton Park, SA2 8PP, Sketty, Swansea, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Harwood", 
        "givenName": "Will", 
        "id": "sg:person.012570304207.93", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012570304207.93"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, Swansea University, Singleton Park, SA2 8PP, Sketty, Swansea, UK", 
          "id": "http://www.grid.ac/institutes/grid.4827.9", 
          "name": [
            "Department of Computer Science, Swansea University, Singleton Park, SA2 8PP, Sketty, Swansea, UK"
          ], 
          "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"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, Swansea University, Singleton Park, SA2 8PP, Sketty, Swansea, UK", 
          "id": "http://www.grid.ac/institutes/grid.4827.9", 
          "name": [
            "Department of Computer Science, Swansea University, Singleton Park, SA2 8PP, Sketty, Swansea, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Setzer", 
        "givenName": "Anton", 
        "id": "sg:person.016555714573.74", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016555714573.74"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2006", 
    "datePublishedReg": "2006-01-01", 
    "description": "Bisimilarity and weak bisimilarity \u2248 are canonical notions of equivalence between processes, which are defined co-inductively, but may be approached \u2013 and even reached \u2013 by their (transfinite) inductively-defined approximants ~\u03b1 and \u2248\u03b1. For arbitrary processes this approximation may need to climb arbitrarily high through the infinite ordinals before stabilising. In this paper we consider a simple yet well-studied process algebra, the Basic Parallel Processes (BPP), and investigate for this class of processes the minimal ordinal \u03b1 such that \u2248 = \u2248\u03b1.The main tool in our investigation is a novel proof of Dickson\u2019s Lemma. Unlike classical proofs, the proof we provide gives rise to a tight ordinal bound, of \u03c9n, on the order type of non-increasing sequences of n-tuples of natural numbers. With this we are able to reduce a long-standing bound on the approximation hierarchy for weak bisimilarity \u2248 over BPP, and show that \\documentclass[12pt]{minimal}\n\t\t\t\t\\usepackage{amsmath}\n\t\t\t\t\\usepackage{wasysym}\n\t\t\t\t\\usepackage{amsfonts}\n\t\t\t\t\\usepackage{amssymb}\n\t\t\t\t\\usepackage{amsbsy}\n\t\t\t\t\\usepackage{mathrsfs}\n\t\t\t\t\\usepackage{upgreek}\n\t\t\t\t\\setlength{\\oddsidemargin}{-69pt}\n\t\t\t\t\\begin{document}${\\approx} = {\\approx_{\\omega^\\omega}}$\\end{document}.", 
    "editor": [
      {
        "familyName": "\u00c9sik", 
        "givenName": "Zolt\u00e1n", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/11874683_24", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-540-45458-8", 
        "978-3-540-45459-5"
      ], 
      "name": "Computer Science Logic", 
      "type": "Book"
    }, 
    "keywords": [
      "class of processes", 
      "approximation hierarchy", 
      "Dickson\u2019s lemma", 
      "main tool", 
      "natural numbers", 
      "Basic Parallel Processes", 
      "ordinal \u03b1", 
      "lemma", 
      "order type", 
      "approximants", 
      "process algebra", 
      "classical proofs", 
      "arbitrary process", 
      "infinite ordinal", 
      "novel proof", 
      "canonical notion", 
      "algebra", 
      "proof", 
      "approximation", 
      "ordinal", 
      "non-increasing sequences", 
      "\u03c9n", 
      "bisimilarity", 
      "equivalence", 
      "class", 
      "tuples", 
      "weak bisimilarity", 
      "parallel processes", 
      "notion", 
      "process", 
      "hierarchy", 
      "number", 
      "tool", 
      "types", 
      "sequence", 
      "investigation", 
      "CO", 
      "standing", 
      "paper"
    ], 
    "name": "Weak Bisimulation Approximants", 
    "pagination": "365-379", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1040675574"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/11874683_24"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/11874683_24", 
      "https://app.dimensions.ai/details/publication/pub.1040675574"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-20T07:41", 
    "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_12.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/11874683_24"
  }
]
 

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/11874683_24'

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/11874683_24'

Turtle is a human-readable linked data format.

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

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

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


 

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

113 TRIPLES      23 PREDICATES      65 URIs      58 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/11874683_24 schema:about anzsrc-for:01
2 anzsrc-for:0101
3 schema:author N3e9bcbbbab5a444f9e4d89b80f268194
4 schema:datePublished 2006
5 schema:datePublishedReg 2006-01-01
6 schema:description Bisimilarity and weak bisimilarity ≈ are canonical notions of equivalence between processes, which are defined co-inductively, but may be approached – and even reached – by their (transfinite) inductively-defined approximants ~α and ≈α. For arbitrary processes this approximation may need to climb arbitrarily high through the infinite ordinals before stabilising. In this paper we consider a simple yet well-studied process algebra, the Basic Parallel Processes (BPP), and investigate for this class of processes the minimal ordinal α such that ≈ = ≈α.The main tool in our investigation is a novel proof of Dickson’s Lemma. Unlike classical proofs, the proof we provide gives rise to a tight ordinal bound, of ωn, on the order type of non-increasing sequences of n-tuples of natural numbers. With this we are able to reduce a long-standing bound on the approximation hierarchy for weak bisimilarity ≈ over BPP, and show that \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}${\approx} = {\approx_{\omega^\omega}}$\end{document}.
7 schema:editor Nde335f2fec0442ae91183410032f8093
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N95e96ee4b72048eda8c4ebf6cc3f9562
12 schema:keywords Basic Parallel Processes
13 CO
14 Dickson’s lemma
15 algebra
16 approximants
17 approximation
18 approximation hierarchy
19 arbitrary process
20 bisimilarity
21 canonical notion
22 class
23 class of processes
24 classical proofs
25 equivalence
26 hierarchy
27 infinite ordinal
28 investigation
29 lemma
30 main tool
31 natural numbers
32 non-increasing sequences
33 notion
34 novel proof
35 number
36 order type
37 ordinal
38 ordinal α
39 paper
40 parallel processes
41 process
42 process algebra
43 proof
44 sequence
45 standing
46 tool
47 tuples
48 types
49 weak bisimilarity
50 ωn
51 schema:name Weak Bisimulation Approximants
52 schema:pagination 365-379
53 schema:productId N074fe0d1f92a4828ad984ec887d13037
54 N22bea5aae4d54378ae95c82e1ed362eb
55 schema:publisher N409d0e18e3814e20b1375f7480467ed5
56 schema:sameAs https://app.dimensions.ai/details/publication/pub.1040675574
57 https://doi.org/10.1007/11874683_24
58 schema:sdDatePublished 2022-05-20T07:41
59 schema:sdLicense https://scigraph.springernature.com/explorer/license/
60 schema:sdPublisher Nbf349eb8676f4539bbbe6b770682743d
61 schema:url https://doi.org/10.1007/11874683_24
62 sgo:license sg:explorer/license/
63 sgo:sdDataset chapters
64 rdf:type schema:Chapter
65 N074fe0d1f92a4828ad984ec887d13037 schema:name doi
66 schema:value 10.1007/11874683_24
67 rdf:type schema:PropertyValue
68 N22bea5aae4d54378ae95c82e1ed362eb schema:name dimensions_id
69 schema:value pub.1040675574
70 rdf:type schema:PropertyValue
71 N2d235a10696a4a1792dbcc4ef75ad3dd schema:familyName Ésik
72 schema:givenName Zoltán
73 rdf:type schema:Person
74 N3e9bcbbbab5a444f9e4d89b80f268194 rdf:first sg:person.012570304207.93
75 rdf:rest N5bcccd2fd02b44669b56a0544ca08163
76 N409d0e18e3814e20b1375f7480467ed5 schema:name Springer Nature
77 rdf:type schema:Organisation
78 N5bcccd2fd02b44669b56a0544ca08163 rdf:first sg:person.010425236217.29
79 rdf:rest Na0e26b77bdef4f2480ad21c8daf66d22
80 N95e96ee4b72048eda8c4ebf6cc3f9562 schema:isbn 978-3-540-45458-8
81 978-3-540-45459-5
82 schema:name Computer Science Logic
83 rdf:type schema:Book
84 Na0e26b77bdef4f2480ad21c8daf66d22 rdf:first sg:person.016555714573.74
85 rdf:rest rdf:nil
86 Nbf349eb8676f4539bbbe6b770682743d schema:name Springer Nature - SN SciGraph project
87 rdf:type schema:Organization
88 Nde335f2fec0442ae91183410032f8093 rdf:first N2d235a10696a4a1792dbcc4ef75ad3dd
89 rdf:rest rdf:nil
90 anzsrc-for:01 schema:inDefinedTermSet anzsrc-for:
91 schema:name Mathematical Sciences
92 rdf:type schema:DefinedTerm
93 anzsrc-for:0101 schema:inDefinedTermSet anzsrc-for:
94 schema:name Pure Mathematics
95 rdf:type schema:DefinedTerm
96 sg:person.010425236217.29 schema:affiliation grid-institutes:grid.4827.9
97 schema:familyName Moller
98 schema:givenName Faron
99 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010425236217.29
100 rdf:type schema:Person
101 sg:person.012570304207.93 schema:affiliation grid-institutes:grid.4827.9
102 schema:familyName Harwood
103 schema:givenName Will
104 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012570304207.93
105 rdf:type schema:Person
106 sg:person.016555714573.74 schema:affiliation grid-institutes:grid.4827.9
107 schema:familyName Setzer
108 schema:givenName Anton
109 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016555714573.74
110 rdf:type schema:Person
111 grid-institutes:grid.4827.9 schema:alternateName Department of Computer Science, Swansea University, Singleton Park, SA2 8PP, Sketty, Swansea, UK
112 schema:name Department of Computer Science, Swansea University, Singleton Park, SA2 8PP, Sketty, Swansea, UK
113 rdf:type schema:Organization
 




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


...