Skip to main content
SpringerLink
Log in

A New Rewrite Method for Proving Convergence of Self-Stabilizing Systems

  • Conference paper
  • First Online:
Distributed Computing (DISC 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1693))

Included in the following conference series:

Abstract

In the framework of self-stabilizing systems, the convergence proof is generally done by exhibiting a measure that strictly decreases until a legitimate configuration is reached. The discovery of such a mea- sure is very specific and requires a deep understanding of the studied transition system. In contrast we propose here a simple method for prov- ing convergence, which regards self-stabilizing systems as string rewrite systems, and adapts a procedure initially designed by Dershowitz for proving termination of string rewrite systems.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. G. Antonoiu and P.K. Srimani. “A Self-Stabilizing Leader Election Algorithm for Tree Graphs”, Journal of Parallel and Distributed Computing, 34:2, May 1996, pp. 227–232.

    Article  Google Scholar 

  2. Y. Afek, S. Kutten and M. Yung M.. “Memory efficient self stabilizing protocols for general networks”, Proc. 7th WDAG, LNCS 725, Springer-Verlag, 1990, pp. 15–28.

    Google Scholar 

  3. A. Arora, M.G. Gouda and T. Herman. “Composite routing protocols”. Proc. 2nd IEEE Symp. on Parallel and Distributed Processing, 1990.

    Google Scholar 

  4. J. Beauquier and O. Debas. “An optimal self-stabilizing algorithm for mutual exclusion on uniform bidirectional rings”. Proc. 2nd Workshop on Self-Stabilizing Systems, Las Vegas, 1995, pp. 226–239.

    Google Scholar 

  5. R.V. Book and F. Otto. String-Rewriting Systems. Springer-Verlag, 1993.

    Google Scholar 

  6. J.E. Burns and J. Pachl. “Uniform Self-Stabilizing Rings”. TOPLAS 11:2, 1989.

    Google Scholar 

  7. N. Dershowitz. “Termination of Linear Rewriting Systems”. Proc. ICALP, LNCS 115, Springer-Verlag, 1981, pp. 448–458.

    Google Scholar 

  8. N. Dershowitz and C. Hoot. “Topics in termination”. Proc. Rewriting Techniques and Applications, LNCS 690, Springer-Verlag, 1993, pp. 198–212.

    Google Scholar 

  9. N. Dershowitz and J.-P. Jouannaud. “Rewrite Systems”. Handbook of Theoretical Computer Science, vol. B, Elsevier–MIT Press, 1990, pp. 243–320.

    MathSciNet  Google Scholar 

  10. E.W. Dijkstra. “Self-stabilizing systems in spite of distributed control”. Comm. ACM 17:11, 1974, pp. 643–644.

    Article  MATH  Google Scholar 

  11. E.W. Dijkstra. “A Belated Proof of Self-stabilization”. Distributed Computing 1:1, 1986, pp. 5–6.

    Article  MATH  MathSciNet  Google Scholar 

  12. M. Fay. “First-order uni.cation in an equational theory”. Proc. 4th Workshop on Automated Deduction, Austin, Texas, 1979, pp. 161–167.

    Google Scholar 

  13. S. Ghosh. “An Alternative Solution to a Problem on Self-Stabilization”. ACM TOPLAS 15:4, 1993, pp. 735–742.

    Article  Google Scholar 

  14. M.G. Gouda. “The triumph and tribulation of system stabilization”. Proc. 9th WDAG, LNCS 972, Springer-Verlag, 1995, pp. 1–18.

    Google Scholar 

  15. M.G. Gouda and T. Herman. “Adaptative programming”. IEEE Transactions on Software Engineering 17, 1991, pp.911–921.

    Article  MathSciNet  Google Scholar 

  16. T. Herman. Adaptativity through distributed convergence. Ph.D. Thesis, University of Texas at Austin. 1991.

    Google Scholar 

  17. J.-H. Hoepman. “Uniform Deterministic Self-Stabilizing Ring-Orientation on Odd-Length Rings”. Proc. 8th Workshop on Distributed Algorithms, LNCS 857, Springer-Verlag. 1994, pp.265–279.

    Chapter  Google Scholar 

  18. S.C. Hsu and S.T. Huang. “A self-stabilizing algorithm for maximal matching”. Information Processing Letters 43:2, 1992, pp. 77–81.

    Article  MATH  MathSciNet  Google Scholar 

  19. J.-M. Hullot. “Canonical Forms and Unification”. Proc. 5th Conf. on Automated Deduction, LNCS, Springer-Verlag, 1980, pp. 318–334.

    Google Scholar 

  20. J. Jaffar. “Minimal and Complete Word Unification”. J. ACM 37:1, 1990, pp. 47–85.

    Article  MATH  MathSciNet  Google Scholar 

  21. S. Katz and K.J. Perry. “Self-stabilizing extensions for message-passing systems”. Distributed Computing 7, 1993, pp. 17–26.

    Article  Google Scholar 

  22. J.L.W. Kessels. “An Exercise in proving self-stabilization with a variant function”. Information and Processing Letters 29, 1988, pp. 39–42.

    Article  MATH  MathSciNet  Google Scholar 

  23. Y. Kesten, O. Maler, M. Marcuse, A. Pnueli and E. Shahar. “Symbolic Model-Checking with Rich Assertional Languages”. Proc. CAV’97, LNCS 1254, Springer-Verlag, 1997, pp. 424–435.

    Google Scholar 

  24. I. Litovski and Y. Métivier. “Computing with Graph Rewriting Systems with Priorities”. Theoretical Computer Science 115:2, 1993, pp. 191–224.

    Article  MathSciNet  Google Scholar 

  25. I. Litovski, Y. Métivier and E. Sopena. “Different Local Controls for Graph Relabeling Systems”. Mathematical Systems Theory 28:1, 1995, pp. 41–65.

    Article  MathSciNet  Google Scholar 

  26. I. Litovski, Y. Métivier and W. Zielonka. “On the Recognition of Families of Graphs with Local Computations”. Information and Computation 118:1, 1995, pp. 110–119.

    Article  MathSciNet  Google Scholar 

  27. G.S. Makanin. “The problem of solvability of equations in a free semigroup”. Matematiceskij Sbornik 103, 1977, pp. 147–236.

    MathSciNet  Google Scholar 

  28. M. Schneider. “Self-Stabilization”. ACM Computing Surveys 25:1, 1993.

    Google Scholar 

  29. J.R. Slagle. “Automated Theorem-Proving for Theories with Simplifiers, Commutativity, and Associativity.” J. ACM 21:4, 1974, pp. 622–642.

    Article  MATH  MathSciNet  Google Scholar 

  30. G. Tel. Introduction to Distributed Algorithms. Cambridge University Press, 1994.

    Google Scholar 

  31. O. Theel and F.C. Gärtner. “An Exercise in Proving Convergence through Transfer Functions”. Proc. 4th Workshop on Self-stabilizing Systems, Austin, Texas, 1999, pp. 41–47.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LRI, CNRS URA 410, Université Paris-Sud, 91405, Orsay cedex, France

    Joffroy Beauquier & Béatrice Bérard

  2. LSV, CNRS UMR 8643, ENS de Cachan, 61 av. du Prés. Wilson, 94235, Cachan cedex, France

    Laurent Fribourg

Authors
  1. Joffroy Beauquier
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Béatrice Bérard
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Laurent Fribourg
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department for Computer Science 6211 Sudikoff Laboratory for Computer Science, Dartmouth College, Hanover, NH, 03755, USA

    Prasad Jayanti

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Beauquier, J., Bérard, B., Fribourg, L. (1999). A New Rewrite Method for Proving Convergence of Self-Stabilizing Systems. In: Jayanti, P. (eds) Distributed Computing. DISC 1999. Lecture Notes in Computer Science, vol 1693. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48169-9_17

Download citation

  • DOI: https://doi.org/10.1007/3-540-48169-9_17

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66531-1

  • Online ISBN: 978-3-540-48169-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation