Understanding and verifying distributed algorithms using stratified decomposition
Ching-Tsun Chou, Eli M. Gafni · 1988
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 as-