Layers as knowledge transitions in the design of distributed systems

  • Wil Janssen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1019)


Knowledge based logics allow to give generic specifications of classes of network protocols. This genericity is combined with methods to derive sequentially structured or layered implementations of distributed algorithms. Knowledge based logic is used to specify layers in such algorithms as knowledge transitions. The resulting layered implementations are transformed to distributed algorithms by means a transformation rule based on the principle of communication closed layers.

In this way a class of solutions to a problem for different architectures can be derived along the same lines simultaneously. This design technique for distributed algorithms is applied to a number of examples including different versions of the Two-Phase Commit protocol.


Sequential Composition Parallel Composition Protocol Layer Virtual Channel Epistemic Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [1]
    G. Andrews. Concurrent Programming — Principles and Practice. The Benjamin/Cummings Publishing Company, 1991.Google Scholar
  2. [2]
    K. Apt and E.-R. Olderog. Verification of sequential and concurrent programs. Springer-Verlag, 1991.Google Scholar
  3. [3]
    R. Back and K. Sere. Stepwise refinement of action systems. Structured Programming, 12:17–30, 1991.Google Scholar
  4. [4]
    P. Bernstein, V. Hadzilacos, and N. Goodman. Concurrency Control and Recovery in Database Systems. Addison-Wesley, 1987.Google Scholar
  5. [5]
    R. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.Google Scholar
  6. [6]
    C. Chou and E. Gafni. Understanding and verifying distributed algorithms using stratified decomposition. In Proceeding 7th ACM Symposium on Principles of Distributed Computing, 1988.Google Scholar
  7. [7]
    F. Cristian, H. Aghili, R. Strong, and D. Dolev. Atomic broadcast: From simple message diffusion to byzantine agreement. In Proceedings 15th International Symposium on Fault-Tolerant Computing, 1985.Google Scholar
  8. [8]
    T. Elrad and N. Francez. Decomposition of distributed programs into communication closed layers. Science of Computer Programming, 2:155–173, 1982.Google Scholar
  9. [9]
    R. Fagin, J. Halpern, Y. Moses, and M. Vardi. Knowledge-based programs. In Proceedings ACM Symposium on Principles of Distributed Computing. ACM, 1995.Google Scholar
  10. [10]
    R. Fagin, J. Halpern, Y. Moses, and M. Vardi. Reasoning About Knowledge. MIT Press, 1995. To appear.Google Scholar
  11. [11]
    J. Halpern and Y. Moses. Knowledge and common knowledge in a distributed environment. Journal of the ACM, 37(3):549–587, 1990.Google Scholar
  12. [12]
    J. Halpern and L. Zuck. A little knowledge goes a long way: Knowledge-based derivations and correctness proofs for a family of protocols. Journal of the ACM, 39(3):449–478, 1992.Google Scholar
  13. [13]
    W. Janssen. Layered Design of Parallel Systems. PhD thesis, University of Twente, 1994.Google Scholar
  14. [14]
    W. Janssen. Layers as knowledge transitions in the design of distributed systems. Technical Report 94-71, University of Twente, 1994.Google Scholar
  15. [15]
    W. Janssen, M. Poel, and J. Zwiers. Action systems and action refinement in the development of parallel systems. In Proceedings of CONCUR '91, LNCS 527, pages 298–316. Springer-Verlag, 1991.Google Scholar
  16. [16]
    W. Janssen and J. Zwiers. Protocol design by layered decomposition, a compositional approach. In J. Vytopil, editor, Proceedings Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 571, pages 307–326. Springer-Verlag, 1992.Google Scholar
  17. [17]
    B. Jonsson. Modular verification of asynchronous networks. In Proceedings 6th ACM Symposium on Principles of Distributed Computing, pages 152–166, 1987.Google Scholar
  18. [18]
    S. Katz and D. Peled. Verification of distributed programs using representative interleaving sequences. Distributed Computing, 6(2), 1992.Google Scholar
  19. [19]
    N. Lynch, M. Merritt, W. Weihl, and A. Fekete. Atomic Transactions. Morgan Kaufman Publishers, 1994.Google Scholar
  20. [20]
    N. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings 6th ACM Symposium on Principles of Distributed Computing, pages 137–151, 1987.Google Scholar
  21. [21]
    J.-J. Meyer, W. van der Hoek, and G. Vreeswijk. Epistemic logic for computer science: A tutorial. Bulletin of the EATCS, numbers 44 and 45, 1991.Google Scholar
  22. [22]
    Y. Moses and O. Kislev. Knowledge-oriented programming, (extended abstract). In Proceedings 12th ACM Symposium on Principles of Distributed Computing, pages 261–270. ACM, 1993.Google Scholar
  23. [23]
    S. Mullender, editor. Distributed Systems. Addison-Wesley, second edition, 1993.Google Scholar
  24. [24]
    S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6:319–340, 1976.Google Scholar
  25. [25]
    M. Poel and J. Zwiers. Layering techniques for development of parallel systems. In G. v. Bochmann and D. Probst, editors, Proceedings Computer Aided Verification, LNCS 663, pages 16–29. Springer-Verlag, 1992.Google Scholar
  26. [26]
    M. Raynal and J.-M. Helary. Synchronization and control of distributed systems and programs. John Wiley & Sons, 1990.Google Scholar
  27. [27]
    F. Stomp and W.-P. de Roever. A correctness proof of a distributed minimum-weight spanning tree algorithm (extended abstract). In Proceedings of the 7th ICDCS, 1987.Google Scholar
  28. [28]
    F. Stomp and W.-P. de Roever. A principle for sequential reasoning about distributed systems. Formal Aspects of Computing, 6(6):716–737, 1994.Google Scholar
  29. [29]
    M. van Hulst and J.-J. Meyer. An epistemic proof system for parallel processes. In R. Fagin, editor, Proceedings 5th TARK, pages 243–254. Morgan Kaufmann, 1994.Google Scholar
  30. [30]
    M. Wieczorek. Locative Temporal Logic and Distributed Real-Time Systems. PhD thesis, Catholic University of Nijmegen, 1994.Google Scholar
  31. [31]
    J. Zwiers and W. Janssen. Partial order based design of concurrent systems. In J. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Proceedings of the REX School/Symposium “A Decade of Concurreny”,m Noordwijkerhout, 1993, LNCS 803, pages 622–684. Springer-Verlag, 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Wil Janssen
    • 1
  1. 1.Fachbereich InformatikUniversity of OldenburgOldenburgGermany

Personalised recommendations