Constructing Minimal Coverability Sets

• Autorzy: Piipponen A. , Valmari A.

Identyfikatory

DOI

10.3233/FI-2016-1319

• Języki publikacji: EN

Abstrakty

EN

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 a few 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.

Słowa kluczowe

EN

coverability set; Tarjan’s algorithm; antichain data structure

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2016
• Tom: Vol. 143, nr 3/4
• Strony: 393--414
• Opis fizyczny: Bibliogr. 13 poz., rys., tab.

Twórcy

autor

Piipponen A.

• Department of Mathematics, Tampere University of Technology, P.O. Box 553, FI–33101 Tampere, Finland

autor

Valmari A.

• Department of Mathematics, Tampere University of Technology, P.O. Box 553, FI–33101 Tampere, Finland

Bibliografia

• [1] Karp RM, Miller RE. Parallel Program Schemata. J Comput Syst Sci. 1969;3(2):147–195. Available from: http://dx.doi.org/10.1016/S0022-0000(69)80011-5. doi:10.1016/S0022-0000(69)80011-5.
• [2] Finkel A. The Minimal Coverability Graph for Petri Nets. In: Rozenberg G, editor. Advances in Petri Nets 1993, Papers from the 12th International Conference on Applications and Theory of Petri Nets, Gjern, Denmark, June 1991. vol. 674 of Lecture Notes in Computer Science. Springer; 1993. p. 210–243. Available from: http://dx.doi.org/10.1007/3-540-56689-9_45. doi:10.1007/3-540-56689-9 45.
• [3] Geeraerts G, Raskin J, Van Begin L. On the Efficient Computation of the Minimal Coverability Set of Petri Nets. Int J Found Comput Sci. 2010;21(2):135–165. Available from: http://dx.doi.org/10.1142/S0129054110007180. doi:10.1142/S0129054110007180.
• [4] Reynier P, Servais F. Minimal Coverability Set for Petri Nets: Karp and Miller Algorithm with Pruning. FundamInform. 2013;122(1-2):1–30. Available from: http://dx.doi.org/10.3233/FI-2013-781. doi:10.3233/FI-2013-781.
• [5] Valmari A, Hansen H. Old and New Algorithms for Minimal Coverability Sets. In: Haddad S, Pomello L, editors. Application and Theory of Petri Nets - 33rd International Conference, PETRI NETS 2012, Hamburg, Germany, June 25-29, 2012. Proceedings. vol. 7347 of Lecture Notes in Computer Science. Springer; 2012. p. 208–227. Available from: http://dx.doi.org/10.1007/978-3-642-31131-4_12. doi:10.1007/978-3-642-31131-4 12.
• [6] Valmari A, Hansen H. Old and New Algorithms for Minimal Coverability Sets. Fundam Inform. 2014; 131(1):1–25. Available from: http://dx.doi.org/10.3233/FI-2014-1002.doi:10.3233/FI-2014-1002.
• [7] Tarjan RE. Depth-First Search and Linear Graph Algorithms. SIAMJ Comput. 1972;1(2):146–160.Available from: http://dx.doi.org/10.1137/0201010. doi:10.1137/0201010.
• [8] Aho AV, Hopcroft JE, Ullman JD. The Design and Analysis of Computer Algorithms. Addison-Wesley; 1974.
• [9] Eve J, Kurki-Suonio R. On Computing the Transitive Closure of a Relation. Acta Inf. 1977;8:303–314. Available from: http://dx.doi.org/10.1007/BF00271339. doi:10.1007/BF00271339.
• [10] Bryant RE. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans Computers. 1986; 35(8):677–691. Available from: http://doi.ieeecomputersociety.org/10.1109/TC.1986. 1676819. doi:10.1109/TC.1986.1676819.
• [11] Delzanno G, Raskin J, Van Begin L. Covering sharing trees: a compact data structure for parameterized verification. STTT. 2004;5(2-3):268–297. Available from: http://dx.doi.org/10.1007/s10009-003-0110-0. doi:10.1007/s10009-003-0110-0.
• [12] Piipponen A, Valmari A. Constructing Minimal Coverability Sets. In: Abdulla PA, Potapov I, editors. Reachability Problems - 7th International Workshop, RP 2013, Uppsala, Sweden, September 24-26, 2013 Proceedings. vol. 8169 of Lecture Notes in Computer Science. Springer; 2013. p. 183–195. Available from: http://dx.doi.org/10.1007/978-3-642-41036-9_17. doi:10.1007/978-3-642-41036-9 17.
• [13] Bellettini C, Camilli M, Capra L, Monga M. MaRDiGraS: Simplified Building of Reachability Graphs on Large Clusters. In: Abdulla PA, Potapov I, editors. Reachability Problems - 7th InternationalWorkshop, RP 2013, Uppsala, Sweden, September 24-26, 2013 Proceedings. vol. 8169 of Lecture Notes in Computer Science. Springer; 2013. p. 83–95. Available from: http://dx.doi.org/10.1007/978-3-642-41036-9_9. doi:10.1007/978-3-642-41036-9 9.