Abstract:

A SPIN model checker is mainly used to check whether a system satisfies the specifications expressed in linear temporal logic, and the specifications of the distributed systems and protocols expressed in knowledge logic are more convenient. In this paper, the model checking approaches for the temporal logic of knowledge using SPIN are discussed. According to the theory of partial proposition, the problem of how to model check knowledge operators and public knowledge operators is converted into model checking linear temporal logic. These approaches make SPIN’s functions extended from model checking temporal logic to the linear temporal logic of knowledge. The article discusses the approach of model checking the linear temporal logic of knowledge by analyzing an instance of the RPC protocol.

Key words: SPIN;model checking;temporal logic of knowledge;linear temporal logic