Efficient Verification of Multi-Agent Systems Through Parallel

Multi-agent systems (MASs) have garnered significant interest across various academic fields. Although MASs are widely applicable, they continue to encounter several challenges, particularly in terms of security.. Model checking, a verification technique that examines all possible system states, is employed to address these challenges. However, the state space of many practical systems can be prohibitively large, leading to exponential growth in verification time. This study introduces a new method for verifying MASs using Strategy Computation Tree Logic (SCTL) via the connective probe machine, a model of fully parallel computing. This approach is pioneering in utilizing the probe machine to speed up MAS verification, specifically allowing for the parallel resolution of SCTL formulas. Unlike conventional model checkers, our method can uncover multiple counterexamples for specified properties, facilitating the identification of various system flaws. We have developed a model checker named MC2PM based on our approach and have validated its feasibility and efficiency through experiments.