Constructing Minimal Coverability Sets

详细信息    查看全文

• 作者：Artturi Piipponen ; Antti Valmari
• 关键词：coverability set ; Tarjan’s algorithm ; antichain data structure
• 刊名：Lecture Notes in Computer Science
• 出版年：2013
• 出版时间：2013
• 年：2013
• 卷：8169
• 期：1
• 页码：196-208
• 全文大小：253KB
• 参考文献：1. Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading (1974)
  2. Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers?C-35(8), 677-91 (1986) CrossRef
  3. Delzanno, G., Raskin, J.-F., Van Begin, L.: Covering Sharing Trees: A Compact Data Structure for Parameterized Verification. Software Tools for Technology Transfer?5(2-3), 268-97 (2004) CrossRef
  4. Finkel, A.: The Minimal Coverability Graph for Petri Nets. In: Rozenberg, G. (ed.) APN 1993. LNCS, vol.?674, pp. 210-43. Springer, Heidelberg (1993) CrossRef
  5. Geeraerts, G., Raskin, J.-F., Van Begin, L.: On the Efficient Computation of the Minimal Coverability Set of Petri Nets. International Journal of Foundations of Computer Science?21(2), 135-65 (2010) CrossRef
  6. Karp, R.M., Miller, R.E.: Parallel Program Schemata. Journal of Computer and System Sciences?3(2), 147-95 (1969) CrossRef
  7. Reynier, P.-A., Servais, F.: Minimal Coverability Set for Petri Nets: Karp and Miller Algorithm with Pruning. In: Kristensen, L.M., Petrucci, L. (eds.) PETRI NETS 2011. LNCS, vol.?6709, pp. 69-8. Springer, Heidelberg (2011) CrossRef
  8. Tarjan, R.E.: Depth-First Search and Linear Graph Algorithms. SIAM J. Computing?1(2), 146-60 (1972) CrossRef
  9. Valmari, A., Hansen, H.: Old and New Algorithms for Minimal Coverability Sets. In: Haddad, S., Pomello, L. (eds.) PETRI NETS 2012. LNCS, vol.?7347, pp. 208-27. Springer, Heidelberg (2012) (Extended version has been accepted to Fundamenta Informaticae) CrossRef
  
• 作者单位：Artturi Piipponen (18)
  Antti Valmari (18)
  
  18. Department of Mathematics, Tampere University of Technology, P.O. Box 553, FI-3101, Tampere, Finland
  
• ISSN：1611-3349

文摘

This publication addresses two bottlenecks in the construction of minimal coverability sets of Petri nets: the detection of situations where the marking of a place can be converted to ω, and the manipulation of the set A of maximal ω-markings that have been found so far. For the former, a technique is presented that consumes very little time in addition to what maintaining A consumes. It is based on Tarjan’s algorithm for detecting maximal strongly connected components of a directed graph. For the latter, a data structure is introduced that resembles BDDs and Covering Sharing Trees, but has additional heuristics designed for the present use. Results from initial experiments are shown. They demonstrate significant savings in running time and varying savings in memory consumption compared to an earlier state-of-the-art technique.