research-article

Open access

A Principle for Sequential Reasoning about Distributed Algorithms

Authors:

W.-R de RoeverAuthors Info & Claims

Formal Aspects of Computing, Volume 6, Issue 6

Pages 716 - 737

https://doi.org/10.1007/BF03259394

Published: 01 December 1994 Publication History

Abstract

Designers of network algorithms often give elegant informal descriptions of the intuition behind their algorithms (see [GHS83, Hum83, MeS79, Seg82, Seg83, ZeS80]). Usually these descriptions are structured as if subtasks are performed one after the other. Although these subtasks are performed sequentially from a logical point of view, they are performed concurrently from an operational point of view. The current paper presents a principle for formally designing and verifying these kinds of algorithms. It is formulated in Manna and Pnueli’s linear time temporal logic [MaP83, MaP92]. This principle is applicable to large classes of algorithms, such as those for computing minimum-paths, connectivity, network flow, and minimum-weight spanning trees.

References

References

[1]

Apt KR, Francez N, and de Roever WR A proof system for communicating sequential processes 1980 2-3

[2]

Back RJR and Sere K Stepwise refinement of action systems Proc. of the international conference of mathematics and program construction 1989

[3]

Chou CT and Gafni E Understanding and verifying distributed algorithms using stratified decomposition Proc. of the ACM Symp. on Principles of Distr. Comp. 1988

[4]

Dijkstra EW and Scholten CS Termination detecting for diffusing computations Information Processing Letters 1980 1-4

[5]

Elrad T and Francez N Decomposition of distributed programs into communication closed layers Science of Computer programming 1982 2

[6]

Francez N Distributed termination ACM-TOPLAS 1980

[7]

Fix L, Francez N, and Grumberg O Semantics-driven decompositions for the verification of distributed programs Proc. of the IFIP working group 2.2/2.3 working conference on Programming Concepts and Methods, Sea of Galilea, Israel 1990

[8]

Gallager RT, Humblet PA, and Spira PM A distributed algorithm for minimum-weight spanning trees ACM TOPLAS 1983 5-1

[9]

Gerth RT and Shrira L On proving communication closedness of distributed layers LNCS 1986 241

[10]

Humblet PA A distributed algorithm for minimum-weight directed spanning trees IEEE Trans. on Comm 1983 31-6

[11]

Janssen W., Poel M., and Zwiers J.: Action systems and action refinement in the development of parallel systems, an algebraic approach, LNCS 527, Baeten J.C.M. and Groote J.F. (Editors) (1991).

[12]

Janssen W and Zwiers J From sequential layers to distributed processes —Deriving a distributed minimum weight spanning tree algorithm Proc. of the ACM Symp. on Principles of Distr. Comp. 1992

[13]

Katz S and Peled D Interleaving set temporal logic Proc. of the ACM Symp. on Principles of Distr. Comp. 1987

[14]

Katz S and Peled D An efficient verification method for parallel and distributed programs Proc. of the REX-workshop 1988

[15]

Katz S and Peled D Defining conditional independence using collapses, to appear in TCS. 1991

[16]

Lamport L Paradigms for distributed programs: computing global states LNCS 190 1985

[17]

Manna Z and Pnueli A Verification of concurrent programs: A temporal proof system Foundations of computer science IV, part 2, MC-tracts 1983 159

[18]

Manna Z and Pnueli A The Temporal Logic of Reactive and Concurrent Systems 1992 New York Springer London

[19]

Merlin PM and Segall A A failsafe distributed routing protocol IEEE Trans. on Comm. 1979 27-9

[20]

Owicki SS and Gries D An axiomatic proof technique for parallel programs I Acta Informatica 1976 6

[21]

Pandya PK Compositional verification of distributed programs Tata institute of fundamental research 1988 India Bombay Ph.D. thesis

[22]

Raynal M and Helary J-P Synchronization and control of distributed systems and programs 1990

Digital Library

[23]

Segall A Decentralized maximum-flow algorithms 1982 12

[24]

Segall A.: Distributed network protocols, IEEE Trans. on Inf. Theory. IT29-1 (1983).

[25]

Stomp FA and de Roever WR A correctness proof of a distributed minimum-weight spanning tree algorithm (extended abstract) Proc. of the 7th ICDCS 1987

[26]

Stomp FA and de Roever WR A fully worked out correctness proof of Gallager, Humblet, and Spira’s minimum-weight spanning tree algorithm 1987

[27]

Stomp FA and de Roever WR A formalization of sequentially phased intuition in network protocols 1988

[28]

Stomp FA and de Roever WR Designing distributed algorithms by means of formal sequentially phased reasoning (extended abstract) Proc. of the third International Workshop on Distributed Algorithms (LNCS 392) 1989

[29]

Stomp FA Design and verification of distributed network algorithms: Foundations and applications 1989

[30]

Stomp FA Logrippo L, Probert RL, and Ural H A derivation of a broadcasting protocol using sequentially phased reasoning (extended abstract) Protocol specification, testing, and verification 1990

[31]

Stomp FA and de Roever W P Principles for Sequential Reasoning about Distributed Algorithms Formal Aspects of Computing 1994 6 E 1-70 This paper can be retrieved by downloading the (compressed PostScript) file FACj_6E_p1.ps.Z which can be found in the directory pub/fac of ftp.cs.man.ac.uk.

[32]

Schlichting RD and Schneider FB Using message passing for distributed programming, Proof rules and disciplines ACM TOPLAS 6-3 1984

[33]

Welch JL, Lamport L, and Lynch NA A lattice-structured proof of a minimum spanning tree algorithm Proc. of the ACM Symp. on Principles of Distr. Comp. 1988

[34]

Zerbib FBM and Segall A A distributed shortest path protocol Internal Report EE-395 1980 Israel Technion-Israel Institute of Technology, Haifa

Cited By

Olderog ESwaminathan M(2015)Structural transformations for data-enriched real-time systemsFormal Aspects of Computing10.1007/s00165-014-0306-y27:4(727-750)Online publication date: 1-Jul-2015
https://dl.acm.org/doi/10.1007/s00165-014-0306-y
Swaminathan MKatoen JOlderog E(2012)Layered reasoning for randomized distributed algorithmsFormal Aspects of Computing10.1007/s00165-012-0231-x24:4-6(477-496)Online publication date: 1-Jul-2012
https://dl.acm.org/doi/10.1007/s00165-012-0231-x
Engelhardt KMoses Y(2009)Causing communication closureDistributed Computing10.1007/s00446-009-0081-922:2(73-91)Online publication date: 1-Oct-2009
https://dl.acm.org/doi/10.1007/s00446-009-0081-9
Show More Cited By

Index Terms

A Principle for Sequential Reasoning about Distributed Algorithms

Index terms have been assigned to the content through auto-classification.

Recommendations

A decidable first-order logic for medical reasoning
KES'11: Proceedings of the 15th international conference on Knowledge-based and intelligent information and engineering systems - Volume Part II

This paper is intended to construct a decidable first-order logic for appropriately expressing medical reasoning which may require to express not only time-dependency, paraconsistency, constructiveness, resource-sensitivity, but also order-sensitivity. ...
An introduction to assertional reasoning for concurrent systems

This is a tutorial introduction to assertional reasoning based on temporal logic. The objective is to provide a working familiarity with the technique. We use a simple system model and a simple proof system, and we keep to a minimum the treatment of ...
On Blass Translation for Leśniewski’s Propositional Ontology and Modal Logics
Abstract
In this paper, we shall give another proof of the faithfulness of Blass translation (for short, B-translation) of the propositional fragment $L_{1}$ of Leśniewski’s ontology in the modal logic $K$ by means of Hintikka formula. And we extend the result to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 6, Issue 6

Dec 1994

153 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© BCS 1994.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 December 1994

Accepted: 15 November 1993

Received: 15 October 1993

Published in FAC Volume 6, Issue 6

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
23
Total Downloads

Downloads (Last 12 months)11
Downloads (Last 6 weeks)5

Reflects downloads up to 23 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Olderog ESwaminathan M(2015)Structural transformations for data-enriched real-time systemsFormal Aspects of Computing10.1007/s00165-014-0306-y27:4(727-750)Online publication date: 1-Jul-2015
https://dl.acm.org/doi/10.1007/s00165-014-0306-y
Swaminathan MKatoen JOlderog E(2012)Layered reasoning for randomized distributed algorithmsFormal Aspects of Computing10.1007/s00165-012-0231-x24:4-6(477-496)Online publication date: 1-Jul-2012
https://dl.acm.org/doi/10.1007/s00165-012-0231-x
Engelhardt KMoses Y(2009)Causing communication closureDistributed Computing10.1007/s00446-009-0081-922:2(73-91)Online publication date: 1-Oct-2009
https://dl.acm.org/doi/10.1007/s00446-009-0081-9
Engelhardt KMoses Y(2005)Safe composition of distributed programs communicating over order-preserving imperfect channelsProceedings of the 7th international conference on Distributed Computing10.1007/11603771_4(32-44)Online publication date: 27-Dec-2005
https://dl.acm.org/doi/10.1007/11603771_4
Engelhardt KMoses Y(2005)Causing communication closureProceedings of the 19th international conference on Distributed Computing10.1007/11561927_18(229-243)Online publication date: 26-Sep-2005
https://dl.acm.org/doi/10.1007/11561927_18
Kindler EReisig WVölzer HWalter R(1997)Petri net based verification of distributed algorithms: An exampleFormal Aspects of Computing10.1007/BF012112999:4(409-424)Online publication date: 1-Jul-1997
https://dl.acm.org/doi/10.1007/BF01211299
Janssen WBurns JMoses Y(1996)Refining knowledge oriented actions to layered implementationsProceedings of the fifteenth annual ACM symposium on Principles of distributed computing10.1145/248052.248068(91-100)Online publication date: 1-May-1996
https://dl.acm.org/doi/10.1145/248052.248068

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents