Class:                          CSE914                                             

Date:                           Oct. 14, 2002

Presented Paper:             A Machine Checkable Logic of Knowledge for Specifying Security Properties of Electronic Commerce Protocols

Presenter:                   Ali Ebnenasir


The main part of the discussion was about the knowledge and the way that knowledge is modeled in this paper. What does it mean when we say an agent A knows fact F?  How do we model this knowledge? It seems that in this paper, the acquisition of a data item by an agent represents the state of knowledge in that agent. This is somewhat different with the representation of knowledge in the literature. The notion of knowledge is mostly modeled in the literature by  Kripke structures (of possible worlds). When we say "agent

A knows fact F", that means in every possible world that is known to "A", fact "F" is true (in a two-value logic).

For example, consider the fact that "today is sunny in East Lansing". If I only consider the city of East Lansing and Chicago then my possible worlds are East Lansing and Chicago. Also, suppose I have no knowledge about the weather in Chicago.

Hence, in every possible world that I have considered, the fact "today is sunny in East Lansing" is true but the fact "Chicago is sunny" is uncertain. If I had just considered East Lansing as my possible world, then I would not have come up with this uncertainty.

Therefore, the fewer worlds an agent considers possible, the less uncertainty (s)he encounters and the more (s)he "knows".



Take a look at the following book for more information, just in case you have not already seen it.


"Reasoning about knowledge",  By: Ronald Fagin, Joseph Halpern, Yoram Moses, and Moshe Y. Vardi, MIT Press, 1995.



There is also a paper about the implementation of knowledge-based programs that are represented by Dijkstra's guarded command language. These programs are distinguished from standard programs by having modal logic conditions in the guard of each program action.


Take a look at the following papers for more information:


1) Meyden, R. v. d. 1996b. Finite state implementations of knowledge-based

programs. In Proceedings of the Conference on Foundations of Software

Technology and Theoretical Computer Science, Volume 1180 of Lecture Notes

in Computer Science (Hyderabad, India, Dec. 1996), pp. 262-273.


2) R. van der Meyden and N. Shilov. Model checking knowledge and time in

systems with perfect recall. In Proceedings of the Conference on

Foundations of Software Technology and Theoretical Computer Science (LNCS

Volume 1738), pages 432.




The second part of the discussion was mostly concentrated on the wrap up of the mini-tutorial. Ali presented a comparison table for the specification languages presented in the mini-tutorial. Students gave their comments about this table and they proposed some modifications for the comparison table. Then Dr. Cheng asked everybody to send their comments to Ali in order to reorganize the comparison table, and then make it available for the class.