Petri-Net-Based Partial Order Reduction for Model Checking Temporal Epistemic Logic on Multiagent Systems

Recent years have witnessed extensive research on verifying multiagent system (MAS) properties, with model checking emerging as the predominant validation technique in this domain. The paramount challenge in MAS verification is state space explosion, and the most general method to mitigate this problem is partial order reduction (POR). However, existing PORs for MAS suffer from wasting reduction potential due to the relatively coarse characterization of dependence relationships and the relatively conservative selection rules of the firing set. To deal with the above issues, this article proposes a complete solution from system modeling to reduced state space generation. First, to enable enhanced POR through fine-grained dependence analysis, a Petri net model is presented for MAS. Unlike existing Petri net models, the model focuses on characterizing the semantics of the MAS interpreted system. Second, a stubborn set method for temporal epistemic logic is proposed, based on the model, transition selection rules, and a reduced state space generation algorithm are provided. The correctness of the method is proved by a theorem. Finally, an automated tool embodying the proposed method is developed, with comparative evaluations performed to validate the efficacy. Against the existing POR method, the proposed method is more efficient in terms of both space performance and time performance, which reduces state storage space and time expenses. Moreover, it is relative to binary decision diagram (BDD)-based implicit methods, and the proposed technique demonstrates superior time efficiency for limited-scale systems.