Symbolic Model Checking the Knowledge of the Dining Cryptographers
Ron Van Der Meyden, Kaile Su · 2002
This paper describes how symbolic techniques (in particular, OBDD's) may be used to to implement an algorithm for model checking specifications in the logic of knowledge for a single agent operating with synchronous perfect recall in an environment of which it has incomplete knowledge. As an illustration of the utility...