Probabilistic verification of Herman’s self-stabilisation algorithm View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

2012-06-29

AUTHORS

Marta Kwiatkowska, Gethin Norman, David Parker

ABSTRACT

Herman’s self-stabilisation algorithm provides a simple randomised solution to the problem of recovering from faults in an N-process token ring. However, a precise analysis of the algorithm’s maximum execution time proves to be surprisingly difficult. McIver and Morgan have conjectured that the worst-case behaviour results from a ring configuration of three evenly spaced tokens, giving an expected time of approximately 0.15N2. However, the tightest upper bound proved to date is 0.64N2. We apply probabilistic verification techniques, using the probabilistic model checker PRISM, to analyse the conjecture, showing it to be correct for all sizes of the ring that can be exhaustively analysed. We furthermore demonstrate that the worst-case execution time of the algorithm can be reduced by using a biased coin. More... »

PAGES

661-670

References to SciGraph publications

  • 2007-01-01. Stochastic Model Checking in FORMAL METHODS FOR PERFORMANCE EVALUATION
  • 2011. On Stabilization in Herman’s Algorithm in AUTOMATA, LANGUAGES AND PROGRAMMING
  • 2008-01-01. Probabilistic CEGAR in COMPUTER AIDED VERIFICATION
  • 2005-10-14. Coupling and self-stabilization in DISTRIBUTED COMPUTING
  • 2010-08-03. A game-based abstraction-refinement framework for Markov decision processes in FORMAL METHODS IN SYSTEM DESIGN
  • 1976. Denumerable Markov Chains, with a chapter of Markov Random Fields by David Griffeath in NONE
  • 1995. It usually works: The temporal logic of stochastic systems in COMPUTER AIDED VERIFICATION
  • 1994-09. A logic for reasoning about time and reliability in FORMAL ASPECTS OF COMPUTING
  • 2011. PRISM 4.0: Verification of Probabilistic Real-Time Systems in COMPUTER AIDED VERIFICATION
  • 2009. Dependability Engineering of Silent Self-stabilizing Systems in STABILIZATION, SAFETY, AND SECURITY OF DISTRIBUTED SYSTEMS
  • 2010-04-07. Probabilistic reachability for parametric Markov models in INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER
  • Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/s00165-012-0227-6

    DOI

    http://dx.doi.org/10.1007/s00165-012-0227-6

    DIMENSIONS

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


    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": "Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK", 
              "id": "http://www.grid.ac/institutes/grid.4991.5", 
              "name": [
                "Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Kwiatkowska", 
            "givenName": "Marta", 
            "id": "sg:person.011375012273.39", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "School of Computing Science, University of Glasgow, Glasgow, UK", 
              "id": "http://www.grid.ac/institutes/grid.8756.c", 
              "name": [
                "School of Computing Science, University of Glasgow, Glasgow, UK"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Norman", 
            "givenName": "Gethin", 
            "id": "sg:person.016323171577.36", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK", 
              "id": "http://www.grid.ac/institutes/grid.4991.5", 
              "name": [
                "Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Parker", 
            "givenName": "David", 
            "id": "sg:person.014007552600.37", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/3-540-60045-0_48", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1002999837", 
              "https://doi.org/10.1007/3-540-60045-0_48"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-22110-1_47", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1027900693", 
              "https://doi.org/10.1007/978-3-642-22110-1_47"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-1-4684-9455-6", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1003855982", 
              "https://doi.org/10.1007/978-1-4684-9455-6"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s10703-010-0097-6", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1013198998", 
              "https://doi.org/10.1007/s10703-010-0097-6"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s10009-010-0146-x", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1008242412", 
              "https://doi.org/10.1007/s10009-010-0146-x"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-22012-8_37", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1006189401", 
              "https://doi.org/10.1007/978-3-642-22012-8_37"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-05118-0_17", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1031653339", 
              "https://doi.org/10.1007/978-3-642-05118-0_17"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-72522-0_6", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1012626164", 
              "https://doi.org/10.1007/978-3-540-72522-0_6"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s00446-005-0142-7", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1039696053", 
              "https://doi.org/10.1007/s00446-005-0142-7"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-70545-1_16", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1044553785", 
              "https://doi.org/10.1007/978-3-540-70545-1_16"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf01211866", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1052049375", 
              "https://doi.org/10.1007/bf01211866"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2012-06-29", 
        "datePublishedReg": "2012-06-29", 
        "description": "Herman\u2019s self-stabilisation algorithm provides a simple randomised solution to the problem of recovering from faults in an N-process token ring. However, a precise analysis of the algorithm\u2019s maximum execution time proves to be surprisingly difficult. McIver and Morgan have conjectured that the worst-case behaviour results from a ring configuration of three evenly spaced tokens, giving an expected time of approximately 0.15N2. However, the tightest upper bound proved to date is 0.64N2. We apply probabilistic verification techniques, using the probabilistic model checker PRISM, to analyse the conjecture, showing it to be correct for all sizes of the ring that can be exhaustively analysed. We furthermore demonstrate that the worst-case execution time of the algorithm can be reduced by using a biased coin.", 
        "genre": "article", 
        "id": "sg:pub.10.1007/s00165-012-0227-6", 
        "inLanguage": "en", 
        "isAccessibleForFree": false, 
        "isPartOf": [
          {
            "id": "sg:journal.1136737", 
            "issn": [
              "0934-5043", 
              "1433-299X"
            ], 
            "name": "Formal Aspects of Computing", 
            "publisher": "Association for Computing Machinery (ACM)", 
            "type": "Periodical"
          }, 
          {
            "issueNumber": "4-6", 
            "type": "PublicationIssue"
          }, 
          {
            "type": "PublicationVolume", 
            "volumeNumber": "24"
          }
        ], 
        "keywords": [
          "maximum execution time", 
          "execution time", 
          "probabilistic verification techniques", 
          "probabilistic model checker PRISM", 
          "model checker PRISM", 
          "worst-case execution time", 
          "algorithm", 
          "token ring", 
          "worst-case behavior", 
          "verification techniques", 
          "probabilistic verification", 
          "tokens", 
          "verification", 
          "solution", 
          "faults", 
          "precise analysis", 
          "time", 
          "configuration", 
          "technique", 
          "biased coin", 
          "coins", 
          "analysis", 
          "McIver", 
          "behavior", 
          "ring configuration", 
          "date", 
          "prism", 
          "conjecture", 
          "size", 
          "problem", 
          "ring", 
          "Morgan"
        ], 
        "name": "Probabilistic verification of Herman\u2019s self-stabilisation algorithm", 
        "pagination": "661-670", 
        "productId": [
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1006141989"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/s00165-012-0227-6"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1007/s00165-012-0227-6", 
          "https://app.dimensions.ai/details/publication/pub.1006141989"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2022-05-10T10:04", 
        "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/article/article_566.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "https://doi.org/10.1007/s00165-012-0227-6"
      }
    ]
     

    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/s00165-012-0227-6'

    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/s00165-012-0227-6'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/s00165-012-0227-6'

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

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/s00165-012-0227-6'


     

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

    151 TRIPLES      22 PREDICATES      68 URIs      49 LITERALS      6 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/s00165-012-0227-6 schema:about anzsrc-for:08
    2 anzsrc-for:0802
    3 schema:author Nbc5c31a905ab4143b5dba5eaa25df117
    4 schema:citation sg:pub.10.1007/3-540-60045-0_48
    5 sg:pub.10.1007/978-1-4684-9455-6
    6 sg:pub.10.1007/978-3-540-70545-1_16
    7 sg:pub.10.1007/978-3-540-72522-0_6
    8 sg:pub.10.1007/978-3-642-05118-0_17
    9 sg:pub.10.1007/978-3-642-22012-8_37
    10 sg:pub.10.1007/978-3-642-22110-1_47
    11 sg:pub.10.1007/bf01211866
    12 sg:pub.10.1007/s00446-005-0142-7
    13 sg:pub.10.1007/s10009-010-0146-x
    14 sg:pub.10.1007/s10703-010-0097-6
    15 schema:datePublished 2012-06-29
    16 schema:datePublishedReg 2012-06-29
    17 schema:description Herman’s self-stabilisation algorithm provides a simple randomised solution to the problem of recovering from faults in an N-process token ring. However, a precise analysis of the algorithm’s maximum execution time proves to be surprisingly difficult. McIver and Morgan have conjectured that the worst-case behaviour results from a ring configuration of three evenly spaced tokens, giving an expected time of approximately 0.15N2. However, the tightest upper bound proved to date is 0.64N2. We apply probabilistic verification techniques, using the probabilistic model checker PRISM, to analyse the conjecture, showing it to be correct for all sizes of the ring that can be exhaustively analysed. We furthermore demonstrate that the worst-case execution time of the algorithm can be reduced by using a biased coin.
    18 schema:genre article
    19 schema:inLanguage en
    20 schema:isAccessibleForFree false
    21 schema:isPartOf Nb148c4441a4840ae876a945b89a64c83
    22 Nfb9409e1a3814f609123f1e84d89098c
    23 sg:journal.1136737
    24 schema:keywords McIver
    25 Morgan
    26 algorithm
    27 analysis
    28 behavior
    29 biased coin
    30 coins
    31 configuration
    32 conjecture
    33 date
    34 execution time
    35 faults
    36 maximum execution time
    37 model checker PRISM
    38 precise analysis
    39 prism
    40 probabilistic model checker PRISM
    41 probabilistic verification
    42 probabilistic verification techniques
    43 problem
    44 ring
    45 ring configuration
    46 size
    47 solution
    48 technique
    49 time
    50 token ring
    51 tokens
    52 verification
    53 verification techniques
    54 worst-case behavior
    55 worst-case execution time
    56 schema:name Probabilistic verification of Herman’s self-stabilisation algorithm
    57 schema:pagination 661-670
    58 schema:productId N155bb167664b4e4591cb16ed3355d488
    59 N60544db2ab0e4be1a659e2f1c720727f
    60 schema:sameAs https://app.dimensions.ai/details/publication/pub.1006141989
    61 https://doi.org/10.1007/s00165-012-0227-6
    62 schema:sdDatePublished 2022-05-10T10:04
    63 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    64 schema:sdPublisher N4a89742a6cf843b8be9055a1e0d273f5
    65 schema:url https://doi.org/10.1007/s00165-012-0227-6
    66 sgo:license sg:explorer/license/
    67 sgo:sdDataset articles
    68 rdf:type schema:ScholarlyArticle
    69 N155bb167664b4e4591cb16ed3355d488 schema:name doi
    70 schema:value 10.1007/s00165-012-0227-6
    71 rdf:type schema:PropertyValue
    72 N4a89742a6cf843b8be9055a1e0d273f5 schema:name Springer Nature - SN SciGraph project
    73 rdf:type schema:Organization
    74 N60544db2ab0e4be1a659e2f1c720727f schema:name dimensions_id
    75 schema:value pub.1006141989
    76 rdf:type schema:PropertyValue
    77 N6ce811e57f8740caa015b334e64a7053 rdf:first sg:person.014007552600.37
    78 rdf:rest rdf:nil
    79 Nb148c4441a4840ae876a945b89a64c83 schema:volumeNumber 24
    80 rdf:type schema:PublicationVolume
    81 Nb6450811122d48a3802fa7f2d34909d0 rdf:first sg:person.016323171577.36
    82 rdf:rest N6ce811e57f8740caa015b334e64a7053
    83 Nbc5c31a905ab4143b5dba5eaa25df117 rdf:first sg:person.011375012273.39
    84 rdf:rest Nb6450811122d48a3802fa7f2d34909d0
    85 Nfb9409e1a3814f609123f1e84d89098c schema:issueNumber 4-6
    86 rdf:type schema:PublicationIssue
    87 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    88 schema:name Information and Computing Sciences
    89 rdf:type schema:DefinedTerm
    90 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
    91 schema:name Computation Theory and Mathematics
    92 rdf:type schema:DefinedTerm
    93 sg:journal.1136737 schema:issn 0934-5043
    94 1433-299X
    95 schema:name Formal Aspects of Computing
    96 schema:publisher Association for Computing Machinery (ACM)
    97 rdf:type schema:Periodical
    98 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
    99 schema:familyName Kwiatkowska
    100 schema:givenName Marta
    101 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
    102 rdf:type schema:Person
    103 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.4991.5
    104 schema:familyName Parker
    105 schema:givenName David
    106 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
    107 rdf:type schema:Person
    108 sg:person.016323171577.36 schema:affiliation grid-institutes:grid.8756.c
    109 schema:familyName Norman
    110 schema:givenName Gethin
    111 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36
    112 rdf:type schema:Person
    113 sg:pub.10.1007/3-540-60045-0_48 schema:sameAs https://app.dimensions.ai/details/publication/pub.1002999837
    114 https://doi.org/10.1007/3-540-60045-0_48
    115 rdf:type schema:CreativeWork
    116 sg:pub.10.1007/978-1-4684-9455-6 schema:sameAs https://app.dimensions.ai/details/publication/pub.1003855982
    117 https://doi.org/10.1007/978-1-4684-9455-6
    118 rdf:type schema:CreativeWork
    119 sg:pub.10.1007/978-3-540-70545-1_16 schema:sameAs https://app.dimensions.ai/details/publication/pub.1044553785
    120 https://doi.org/10.1007/978-3-540-70545-1_16
    121 rdf:type schema:CreativeWork
    122 sg:pub.10.1007/978-3-540-72522-0_6 schema:sameAs https://app.dimensions.ai/details/publication/pub.1012626164
    123 https://doi.org/10.1007/978-3-540-72522-0_6
    124 rdf:type schema:CreativeWork
    125 sg:pub.10.1007/978-3-642-05118-0_17 schema:sameAs https://app.dimensions.ai/details/publication/pub.1031653339
    126 https://doi.org/10.1007/978-3-642-05118-0_17
    127 rdf:type schema:CreativeWork
    128 sg:pub.10.1007/978-3-642-22012-8_37 schema:sameAs https://app.dimensions.ai/details/publication/pub.1006189401
    129 https://doi.org/10.1007/978-3-642-22012-8_37
    130 rdf:type schema:CreativeWork
    131 sg:pub.10.1007/978-3-642-22110-1_47 schema:sameAs https://app.dimensions.ai/details/publication/pub.1027900693
    132 https://doi.org/10.1007/978-3-642-22110-1_47
    133 rdf:type schema:CreativeWork
    134 sg:pub.10.1007/bf01211866 schema:sameAs https://app.dimensions.ai/details/publication/pub.1052049375
    135 https://doi.org/10.1007/bf01211866
    136 rdf:type schema:CreativeWork
    137 sg:pub.10.1007/s00446-005-0142-7 schema:sameAs https://app.dimensions.ai/details/publication/pub.1039696053
    138 https://doi.org/10.1007/s00446-005-0142-7
    139 rdf:type schema:CreativeWork
    140 sg:pub.10.1007/s10009-010-0146-x schema:sameAs https://app.dimensions.ai/details/publication/pub.1008242412
    141 https://doi.org/10.1007/s10009-010-0146-x
    142 rdf:type schema:CreativeWork
    143 sg:pub.10.1007/s10703-010-0097-6 schema:sameAs https://app.dimensions.ai/details/publication/pub.1013198998
    144 https://doi.org/10.1007/s10703-010-0097-6
    145 rdf:type schema:CreativeWork
    146 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK
    147 schema:name Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK
    148 rdf:type schema:Organization
    149 grid-institutes:grid.8756.c schema:alternateName School of Computing Science, University of Glasgow, Glasgow, UK
    150 schema:name School of Computing Science, University of Glasgow, Glasgow, UK
    151 rdf:type schema:Organization
     




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


    ...