Designing distributed algorithms by means of formal sequentially phased reasoning

The design principle, formulated using Manna and Pnueli's linear time temporal logic, is applicable to large classes of algorithms, such as those for minimum-path, connectivity, network flow, and minimum-weight spanning trees.

Abstract

Designers of network algorithms give elegant informal descriptions of the intuition behind their algorithms (see [GHS83, Hu83, MS79, Se82, Se83, ZS80]). Usually, these descriptions are structured as if tasks or subtasks are performed sequentially. From an operational point of view, however, they are performed concurrently. Here, we present a design principle that formally describes how to develop algorithms according to such sequentially phased explanations. The design principle is formulated using Manna and Pnueli's linear time temporal logic [MP83]. This principle, together with Chandy and Misra's technique [CM88] or Back and Sere's technique [BS89] for designing parallel algorithms, is applicable to large classes of algorithms, such as those for minimum-path, connectivity, network flow, and minimum-weight spanning trees. In particular, the distributed minimum-weight spanning tree algorithm of Gallager, Humblet, and Spira [GHS83] is structured according to our principle.