Synthesis for Various Petri Net Classes with Union/Find

• Autorzy: Wolf Karsten

Identyfikatory

DOI

10.3233/FI-2019-1839

• Języki publikacji: EN

Abstrakty

EN

We propose a new algorithmic approach for the synthesis of a Petri net from a transition system. It is first presented for a class of place/transition Petri nets we call Δ1-Petri nets. A Δ1-Petri net has an incidence matrix where entries have values 0, 1, and -1 only. The algorithm employs Tarjans union/find algorithm for managing sets of vertices. It requires just O(|V||T|) space where V is the set of vertices and T is the set of transition labels. Consequently, problem instances even beyond 1,000,000 vertices have a manageable memory footprint. Our results are experimentally validated using a prototype implementation. We further present ideas for adapting the method to various classes of Petri nets, including pure (loop-free), safe and k-bounded, ordinary nets as subclasses of Δ-1-Petri nets as well as an extension to Δk-Petri nets. This article is an extended version of [1].

Słowa kluczowe

EN

Petri net; synthesis; Tarjans union/find algorithm

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 169, nr 1-2
• Strony: 57--84
• Opis fizyczny: Bibliogr. 15 poz., rys., tab.

Twórcy

autor

Wolf Karsten

• Universität Rostock, Institut für Informatik, Rostock, Germany

Bibliografia

• [1] Wolf K. Petri Net Synthesis with Union/Find. In: Proc. PETRI NETS, LNCS vol. 10877. 2018 pp. 60-81. doi:10.1007/978-3-319-91268-4_4.
• [2] Badouel E, Bernardinello L, Darondeau P. Petri Net Synthesis. Texts in Theoretical Computer Science. Springer, 2015. ISBN-978-3-662-47966-7, 978-3-662-51621-8. doi:10.1007/978-3-662-47967-4.
• [3] Cortadella J, Kishinevsky M, Lavagno L, Yakovlev A. Deriving Petri Nets for Finite Transition Systems. IEEE Trans. Computers, 1998. 47(8):859-882. doi:10.1109/12.707587.
• [4] Ehrenfeucht A, Rozenberg G. Partial (Set) 2-Structures. Part I: Basic Notions and the Representation Problem. Acta Inf., 1990. 27(4):315-342. doi:10.1007/BF00264611.
• [5] Ehrenfeucht A, Rozenberg G. Partial (Set) 2-Structures. Part II: State Spaces of Concurrent Systems. Acta Inf., 1990. 27(4):343-368. doi:10.1007/BF00264612.
• [6] Mukund M. Petri Nets and Step Transition Systems. Int. J. Found. Comput. Sci., 1992. 3(4):443-478. URL https://doi.org/10.1142/S0129054192000231.
• [7] Badouel E, Bernardinello L, Darondeau P. Polynomial Algorithms for the Synthesis of Bounded Nets. In: Proc. TAPSOFT, LNCS vol. 915. 1995 pp. 364-378. doi:10.1007/3-540-59293-8_207.
• [8] Cortadella J, Kishinevsky M, Kondratyev A, Lavagno L, Yakovlev A. Petrify: a tool for manipulating concurrent specifications and synthesis of asynchronous controllers. In: IEICE Transactions on Information and Systems, volume E80-D, No. 3. 1997 pp. 315-325.
• [9] Carmona J, Cortadella J, Kishinevsky M. Genet: A Tool for the Synthesis and Mining of Petri Nets. In: Proc. ACSD. 2009 pp. 181-185. doi:10.1109/ACSD.2009.6.
• [10] Badouel E, Caillaud B, Darondeau P. Distributing Finite Automata Through Petri Net Synthesis. Formal Asp. Comput., 2002. 13(6):447-470. doi:10.1007/s001650200022.
• [11] Best E, Schlachter U. Analysis of Petri Nets and Transition Systems. In: Proc. ICE, EPTCS 189. 2015 pp. 53-67. doi:10.4204/EPTCS.189.6.
• [12] Tarjan R. Efficiency of a Good But Not Linear Set Union Algorithm. J. ACM, 1975. 22(2):215-225. doi:10.1145/321879.321884.
• [13] Schlachter U. Petri Net Synthesis for Restricted Classes of Nets. In: Proc. PETRI NETS, LNCS vol. 9698. 2016 pp. 79-97. doi:10.1007/978-3-319-39086-4_6.
• [14] et al FK. Complete Results for the 2016 Edition of the Model Checking Contest. 2016. URL http://mcc.lip6.fr/2016/results.php.
• [15] Schmidt K. LoLA: A Low Level Analyser. In: ICATPN, LNCS vol. 1825. 2000 pp. 465-474. doi:10.1007/3-540-44988-4_27.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).