Petri-Net-Based Model Checking for Privacy-Critical Multiagent Systems

Computation tree logic of knowledge (CTLK) can be used to specify many properties related to privacy of multiagent systems (MASs). Our previous work defined knowledge-oriented Petri nets (KPNs) to formally describe both the interacting/collaborating process of multiagents and their epistemic evolutions. Our KPN-based verification of CTLK required to obtain all reachable states, the transition relation of all states, and the equivalence relations of all states with respect to knowledge, which resulted in a serious state explosion problem and thus only fit some small-scale systems. This article adopts reduced ordered binary decision diagram (ROBDD) to deal with this problem. Especially, the ROBDD technique is used to encode and store all reachable states but not to encode and store any transition relation or equivalence relation. However, when verifying a CTLK formula, the transition relation and equivalence relation of some states must be known. To solve this problem, we design the related algorithms to compute only those required relations and prove their correctness. We design the related model checking algorithms and develop a tool. A number of experiments are done by using a famous benchmark about the privacy problem of MAS: the dining cryptographers protocol (DCP), and the results illustrate the advantages of our methods. For example, our tool running with a general PC spends less than 14 h to verify the DCP with 1200 cryptographers, which involves about 101080 states and two CTLK formulas with more than 6000 atomic propositions and more than 3600 operators. This represents a significant advance in the field of model checking.