Computers, robots and humans greatly benefit from protocols – predefined rules. What needs to be done and in which order? Do you kiss twice or three times when you are greeting someone, starting left or right? Does giving ice cream mean that you love someone, as some people seem to think in China? Which signal should a computer send first when it starts its communication? Researchers want to mathematically describe protocols in order to determine whether they are correct. Some protocols are epistemic – protocols where reasoning about knowledge is involved. Yanjing Wang, PhD student from the Centrum Wiskunde & Informatica (CWI), the national research center for mathematics and computer science in Amsterdam, investigated their properties and dynamics with mathematical logic. He graduated with his dissertation ‘Epistemic Modelling and Protocol Dynamics’ on 21 September at the University of Amsterdam. His research can be applied to social software and theoretical computer science.
Ice cream and love
One of the things Yanjing Wang studied is that knowledge of protocols sometimes gives meaning to acts. To explain how this works the Chinese researcher uses an analogy. Wang: “In China the ice cream company Haägen-Dasz uses the advertising slogan: ‘If you love her, take her to Haägen-Dasz’. This is quite well-known amongst youngsters in China. Even if they may not know what love is, they are eager to show it to their beloved ones. With this slogan in mind, buying ice cream is regarded as an act to show love: it is sweet but also a bit expensive (this brand follows a high-end strategy in China). Although love has nothing to do with ice cream, the protocol - or in this case the slogan - assigned a meaning to presenting this cold delicacy”.
Protocols can also become false if knowledge about them is disclosed. Wang: “As another analogy: if a girl knows that a young man is simply acting out the protocol that he should ask her about her feelings, seemingly very interested, she is not as impressed as when she thinks he does so spontaneously.” The PhD student studied a mathematical variant of this kind of protocol.
In his research Wang demonstrated that the verification of epistemic protocols (i.e. checking if they are always correct and contain no faults) is more complicated when the correctness of the protocols relies on higher-order reasoning about knowledge. In order to verify these complex protocols, he developed different types of logics – in particular for handling knowledge updates and protocol changes during the execution of the current protocol. He reduced verification problems of the new logics to known ones and also proposed methods of making epistemic model checking more efficient.
More information:
PhD thesis: http://dare.uva.nl/en/record/350521
http://homepages.cwi.nl/~yanjing/
Promotor: Prof. dr. D.J.N. van Eijck (CWI & UvA)
This research has been supported by NWO and has been carried out at CWI, under the auspices of IPA and ILLC.
