EnPAC：线性时态逻辑的Petri网模型检验
摘要：基于线性时序逻辑（LTL）的显式状态Petri网模型检测中，状态生成和探索（反例搜索）是两个核心。传统的状态生成通过更新结构以减少所有迁移的计算，并频繁进行编码/解码以读取每个编码状态。我们提出了基于动态火集的按需启用迁移的优化计算，以避免这种结构。我们还提出了在不需要解码和重新编码的情况下对编码标记进行直接读/写（DRW）操作，以加快状态生成速度并减少内存消耗。为了在实时框架下更快地搜索反例，我们向布基自动机添加启发式信息，以引导探索朝着被接受的状态方向进行。上述策略可以优化现有的LTL模型检测方法。我们将这些优化策略实现在名为EnPAC（Enhanced Petri-net Analyser and Checker）的Petri网模型检测工具中，并在MCC（Model Checking Contest）基准测试中进行评估，结果显示相比现有方法有显著改进。
作者：Zhijun Ding, Cong He and Shuo Li
论文ID：2307.12324
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-07-25