Petri网产品线可达图的高效构造
形式语言与自动机理论
2026-04-08 v1
摘要
本文提出了一套用于计算Petri网产品线（PNPL）可达图的算法。这些算法解决了由产品线配置引起的并发性和变异性带来的综合挑战。所提出的方法将符号状态表示与基于族的变异性处理相结合，生成紧凑的参数化可达图，捕捉所有产品的行为而无需穷举产品枚举。主要贡献有三方面。第一，我们引入了一种适应PNPL语义的符号状态编码。第二，我们定义了保持族的继承过程，在探索过程中应用特征约束。第三，我们提出了缓解状态空间爆炸的约简技术，包括等价符号状态的在线合并和不相关状态细节的选择性抽象。我们证明了构造相对于标准单产品语义的可靠性和完备性，并分析了计算复杂度。一个集成到建模工具中的实现展示了与朴素产品探索相比在内存和时间上的显著节省，同时保留了诊断和验证能力。结果表明，该方法使实际规模的产品线模型的可达分析成为可能，从而促进了可配置并发系统中的验证和设计空间探索。
引用
@article{arxiv.2604.05657,
title = {Efficient Construction of Reachability Graphs for Petri Net Product Lines},
author = {Elena Gómez-Martínez and José Ignacio Requeno Jarabo},
journal= {arXiv preprint arXiv:2604.05657},
year = {2026}
}