Event-Based Proof of the Mutual Exclusion Property of Peterson’s Algorithm

Event-Based Proof of the Mutual Exclusion Property of Peterson’s Algorithm

Proving properties of distributed algorithms is still a highly challenging problem and various approaches that have been proposed to tackle it [1] can be roughly divided into state-based and event-based proofs. Informally speaking, state-based approaches define the behavior of a distributed algorith...

Full description

Bibliographic Details
Main Authors: Ivanov Ievgen, Nikitchenko Mykola, Abraham Uri
Format: Article
Language:English
Published: Sciendo 2015-12-01
Series:Formalized Mathematics
Subjects:
68m14
68w15
68n30
03b35
distributed system
parallel computing
algorithm
verification
mathematical model
identifier: peterson
version: 8.1.04 5.33.1254
Online Access:https://doi.org/10.1515/forma-2015-0026
id doaj-6554d6d6c8294a08b172cd8ea11a42f6
record_format Article
spelling doaj-6554d6d6c8294a08b172cd8ea11a42f62021-09-05T20:45:03ZengSciendoFormalized Mathematics1426-26301898-99342015-12-0123432533110.1515/forma-2015-0026forma-2015-0026Event-Based Proof of the Mutual Exclusion Property of Peterson’s AlgorithmIvanov Ievgen0Nikitchenko Mykola1Abraham Uri2Taras Shevchenko National University, Kyiv, UkraineTaras Shevchenko National University, Kyiv, UkraineBen-Gurion University, Beer-Sheva, IsraelProving properties of distributed algorithms is still a highly challenging problem and various approaches that have been proposed to tackle it [1] can be roughly divided into state-based and event-based proofs. Informally speaking, state-based approaches define the behavior of a distributed algorithm as a set of sequences of memory states during its executions, while event-based approaches treat the behaviors by means of events which are produced by the executions of an algorithm. Of course, combined approaches are also possible.https://doi.org/10.1515/forma-2015-002668m1468w1568n3003b35distributed systemparallel computingalgorithmverificationmathematical modelidentifier: petersonversion: 8.1.04 5.33.1254
collection DOAJ
language English
format Article
sources DOAJ
author Ivanov Ievgen
Nikitchenko Mykola
Abraham Uri
spellingShingle Ivanov Ievgen
Nikitchenko Mykola
Abraham Uri
Event-Based Proof of the Mutual Exclusion Property of Peterson’s Algorithm
Formalized Mathematics
68m14
68w15
68n30
03b35
distributed system
parallel computing
algorithm
verification
mathematical model
identifier: peterson
version: 8.1.04 5.33.1254
author_facet Ivanov Ievgen
Nikitchenko Mykola
Abraham Uri
author_sort Ivanov Ievgen
title Event-Based Proof of the Mutual Exclusion Property of Peterson’s Algorithm
title_short Event-Based Proof of the Mutual Exclusion Property of Peterson’s Algorithm
title_full Event-Based Proof of the Mutual Exclusion Property of Peterson’s Algorithm
title_fullStr Event-Based Proof of the Mutual Exclusion Property of Peterson’s Algorithm
title_full_unstemmed Event-Based Proof of the Mutual Exclusion Property of Peterson’s Algorithm
title_sort event-based proof of the mutual exclusion property of peterson’s algorithm
publisher Sciendo
series Formalized Mathematics
issn 1426-2630
1898-9934
publishDate 2015-12-01
description Proving properties of distributed algorithms is still a highly challenging problem and various approaches that have been proposed to tackle it [1] can be roughly divided into state-based and event-based proofs. Informally speaking, state-based approaches define the behavior of a distributed algorithm as a set of sequences of memory states during its executions, while event-based approaches treat the behaviors by means of events which are produced by the executions of an algorithm. Of course, combined approaches are also possible.
topic 68m14
68w15
68n30
03b35
distributed system
parallel computing
algorithm
verification
mathematical model
identifier: peterson
version: 8.1.04 5.33.1254
url https://doi.org/10.1515/forma-2015-0026
work_keys_str_mv AT ivanovievgen eventbasedproofofthemutualexclusionpropertyofpetersonsalgorithm
AT nikitchenkomykola eventbasedproofofthemutualexclusionpropertyofpetersonsalgorithm
AT abrahamuri eventbasedproofofthemutualexclusionpropertyofpetersonsalgorithm
_version_ 1717784634377371648

Similar Items