Beliebiger Eintrag,
Understanding and Verifying Distributed Algorithms Using Stratified Decomposition (Extended Abstract)
(1988)
Zusammenfassung
) Ching-Tsun Chou (chou@cs.ucla.edu) Eli Gafni (eli@cs.ucla.edu) Abstract Designers of autonomous distributed algorithms (i.e., algorithms whose complete input is available before the start of execution) customarily refer to temporal ordering in describing the behavior of their algorithms---statements like "after A, task B is performed." In the absence of an explicit termination detection for A built into the algorithm such a statement should be puzzling. However, the available proof methodologies do not seem to hinge on such statements. This paper provides firm theoretical ground for such assertions by pinpointing the essential difference between sequential and concurrent algorithms. Moreover we proposes a proof methodoloy along these lines. By being highly congruent with current designers intuition, our proof methodology is also suitable for design purposes. The paper illustrates the method on a variation of the celebrated dis- Supported by NSF Presidential Young Investigators...
