Petri Net Structural Reduction for Temporal Epistemic Logic Verification in Multi-Agent Systems

Abstract

With the increasingly widespread application of MAS (Multi-Agent System), recent years have witnessed growing research interest in the verification of MAS properties. Similar to traditional concurrent and multi-component systems, the paramount challenge in MAS verification is the state space explosion problem. One approach to mitigating this issue is to reduce the original model before generating the state space, as reductions at the model level can often substantially alleviate state space complexity. However, for MAS modeled using Petri nets, existing methods primarily focus on reduction at the state space level. In contrast, this paper addresses reduction at the underlying model level by proposing a solution of structural reduction for Petri nets that preserve temporal epistemic logic properties. The main contributions consist of three aspects. Firstly, since existing structural reduction rules for Petri nets are not suitable for temporal epistemic logic verification, modifications and extensions to some of the rules are introduced to accommodate temporal epistemic logic, and corresponding theorems are provided to guarantee the correctness of these rules. Furthermore, given that the applicability of structural reduction rules in Petri nets is constrained by transition visibility, this paper conducts a refined visibility analysis of transitions based on semantic characteristics of epistemic logic for a subclass of Petri nets and a specific category of properties. The resulting analysis relaxes the visibility constraints when applying the rules, and its correctness is formally guaranteed by a theorem. Finally, case studies demonstrate that the proposed structural reduction rules save space overhead during verification and achieve better reduction performance under relaxed visibility constraints.