TY - GEN
T1 - Designing distributed algorithms by means of formal sequentially phased reasoning (extended abstract)
AU - Stomp, F.A.
AU - Roever, de, W.P.
PY - 1989
Y1 - 1989
N2 - 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.
AB - 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.
U2 - 10.1007/3-540-51687-5_47
DO - 10.1007/3-540-51687-5_47
M3 - Conference contribution
SN - 3-540-51687-5
T3 - Lecture Notes in Computer Science
SP - 242
EP - 253
BT - Distributed Algorithms (Proceedings 3rd International Workshop, Nice, France, September 26-28, 1989)
A2 - Bermond, J.C.
A2 - Raynal, M.
PB - Springer
CY - Berlin
ER -