Petri Net Analysis Using Invariant Generation
Petri Net Analysis Using Invariant Generation
复制标题
使用不变生成的 Petri 网分析
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Z. Manna
中科院分区：
文献类型：
--
作者：
S. Sankaranarayanan;H. B. Sipma;Z. Manna
Petri网已被广泛应用于并发系统的建模和分析。一方面，它们在这一领域的广泛使用得益于它们的简单性和表现力。另一方面，对Petri网的可达性、有界性和死锁自由等问题的分析可能会非常困难。在本文中，我们将Petri网建模为过渡系统。我们利用这些过渡系统的特殊结构，给出了其所有归纳线性不变量的精确和封闭形式的表征。然后，我们利用这个特征来提供一种不变生成技术，我们在实践中证明了这种技术是有效和强大的。我们将我们的工作与文献中的工作进行比较，并讨论扩展。
Petri nets have been widely used to model and analyze concurrent systems. Their wide-spread use in this domain is, on one hand, facilitated by their simplicity and expressiveness. On the other hand, the analysis of Petri nets for questions like reachability, boundedness and deadlock freedom can be surprisingly hard. In this paper, we model Petri nets as transition systems. We exploit the special structure in these transition systems to provide an exact and closed-form characterization of all its inductive linear invariants. We then exploit this characterization to provide an invariant generation technique that we demonstrate to be efficient and powerful in practice. We compare our work with those in the literature and discuss extensions.