Epistemic Logic

communication protocols, version 1

description

In communication between different agents, for instance in a computer network, communication protocols play an important role. When transmitting information back and forth, we need to make sure that messages from one agent to another do arrive at their destination. Consider, for instance, email or using FTP to send files.
During communication, it is possible that messages "get lost" (deletion). This is why the protocols need to guarantee that messages from the sender arrive at the receiver.

In this assignment, you will work on a logical approach to these communication protocols. First a few procotols are explained and demonstrated, then you can experiment with some of the rules used in these protocols.


Homework assignments

1. Read pages 39 - 44 from the book "Epistemic Logic for AI and Computer Science" and pages 11-14 from "Basics: the modal aproach to knowledge" (see the literature)

2. Review the demonstrations for the protocols A and B and explain why these protocols are safe from deletion errors. (A formal proof is not required.)

3. Experiment with both protocols by either removing or changing the following rules (you can apply changes by pressing the designated buttons)

a) Replace lines 3 and 4 of S in Protocol A by 'send(Xi)' and leave out lines 4 and 5 of R.
What is going wrong, and why?

b) In Protocol A, leave out line 4 of S and replace lines 4 and 5 of R by 'send(Xi) until Kr(Xi+1)'.

What is going wrong, and why? How is this different from Protocol B?

c) Leave out the fourth line of R in protocol B.

What is going wrong, and why?

d) Add an extra path from S to R which is slower. Use protocol B for this.

What is going wrong, and why?

e) Leave out the "color" from messages sent by S and R in protocol B.

What is going wrong, and why?

4. Solve exercise 1.21 from "Basics: the model approach to knowledge."

5. Optional extra assignment: review the demonstration of the TCP protocol. This protocol is safe from deletion errors as well, and moreover, it ensures that messages are put in the correct order.
Explain how this is done. Describe some of the differences between TCP and protocol B. Consider the number of messages that is being sent, or what should be saved by the sender and the receiver.


sources and auxiliary materials

Literature:
* pages 37-44 from "Epistemic Logic for AI and Computer Science", W. van der Hoek, J.J.Ch. Meyer, 1995
* section 1.5 from "Basics: the modal approach to knowledge", R. Verbrugge


Demonstrations:
  • demonstration Protocol A
  • demonstration Protocol B
  • demonstration Protocol TCP
    • Created by Freek Stulp

    Experimenting:
  • Protocol A
  • Protocol B


    • download the protocol applets





    The TCP applet was created by Freek Stulp.

    developer: Rineke Verbrugge (l.c.verbrugge@ai.rug.nl), RUG