论文标题
通用培养皿网的属性指示可达性
Property Directed Reachability for Generalized Petri Nets
论文作者
论文摘要
我们提出了一个基于属性的通用培养皿网（PDR）方法，用于检查通用PETRI网的通用可及性属性的半决定程序。我们实际上定义了三个不同的版本，这些版本会根据用于抽象可能的证人的方法而变化，并且能够处理增加难度的问题。我们已经在名为SMPT的模型检查器中实现了我们的方法，并提供了经验证据，即我们的方法可以处理难以或无法使用当前最先进的工具检查的问题。
We propose a semi-decision procedure for checking generalized reachability properties, on generalized Petri nets, that is based on the Property Directed Reachability (PDR) method. We actually define three different versions, that vary depending on the method used for abstracting possible witnesses, and that are able to handle problems of increasing difficulty. We have implemented our methods in a model-checker called SMPT and give empirical evidences that our approach can handle problems that are difficult or impossible to check with current state of the art tools.
