关键词: Petri网, LTL模型检测, 结构约简, 细粒度并行, 性质保持, 最大独立集, 确定性批提交

Abstract: State space explosion severely limits the scalability of explicit-state LTL(Linear Temporal Logic) model checking for Petri nets.Structural reduction iteratively applies local structural transformations to remove redundant places and transitions,thereby reducing the size of subsequent product-automaton construction and counterexample-path search while preserving consistency in property decisions.To address the preprocessing bottleneck of traditional serial Scan-and-Commit loops on large-scale models,this paper proposes a semantics-aware,fine-grained parallel framework for structural reduction.By analyzing atomic-proposition references in LTL formulas,the framework constructs a PSS(Property Support Set) as the safety boundary for reduction,performs unified one-pass filtering during candidate generation based on the non-intersection between candidate scopes and the PSS,further uses an incremental Impact Set to drive local rescanning,and approximately solves the MIS(Maximum Indepen-dent Set) problem on the scope-conflict graph to schedule conflict-free reduction batches.Statistics over 410 public P/T-net instances from the MCC(Model Checking Contest) 2025 show that,under the K=24 configuration,highly structurally redundant model families achieve 2~4.5x reduction speedups,while most low-redundancy cases remain comparable to the serial baseline; performance regressions on a small number of short-running tasks are mainly attributable to fixed parallel overheads and the serialbarrier in the commit phase.For properties containing the Next(X) operator,the framework supports automatic fallback to a safe rule subset,strictly maintaining the boundary of semantic correctness.

Key words: Petri-net, LTL model checking, Structural reduction, Fine-grained parallelism, Property preservation, Maximum independent set, Deterministic commit