Systems and Means of Informatics
2018, Volume 28, Issue 2, pp 99-115
SOFTWARE IMPLEMENTATION OF A METHOD FOR GENERATION OF PETRI NETS OF LARGE SIZE
- D. I. Kharitonov
- G. V. Tarasov
- D. V. Leontyev
Abstract
The software implementation of a method for generation of Petri nets having millions of elements of places and transitions is described. Particular attention is paid to the internal data structures and algorithmic complexity of the method. The presented material allowed the authors to obtain a software tool with computational complexity O(n) where n is the number of elements in a model. The described theoretical results are justified by the performance tests in practical experiments.
[+] References (12)
- Jensen, K., L. M. Kristensen, andT. Mailund. 2012. The sweep-line state space explo-ration method. Theor. Comput. Sci. 429:169-179. doi: 10.1016/ j.tcs.2011.12.036.
- Abid, C. A., and B. Zouari. 2013. Local verification using a distributed state space. Fundam. Inform. 125(1): 1-20. doi: 10.3233/FI-2013-850.
- Jezequel, L., E. Fabre, and V. Khomenko. 2015. Factored planning: From automata to Petri nets. ACM T. Embed. Comput. S. 14(2). Article No. 26. doi: 10.1145/2656215.
- Kammoun, M.A., N. Rezg, Z. Achour, and S. Rezig. 2016. State space search for safe time Petri nets based on binary decision diagrams tools: Application to air traffic flow management problem. Stud. Inform. Control 25(1):39-50. doi: 10.24846/v25i1y201605.
- Wang, C., Y. Tao, and Y. Zhou. 2017. Protocol verification by simultaneous reacha-bility graph. IEEE Commun. Lett. 21(8):1727-1730. doi: 10.1109/LC0MM.2017. 2695191.
- Thierry-Mieg, Y. 2015. Symbolic model-checking using ITS-tools. 21st Conference (International) on Tools and Algorithms for the Construction and Analysis of Systems Proceedings. London: Springer. 231-237.
- Amparore, E. G., M. Beccuti, and S. Donatelli. 2014. (Stochastic) model checking in GreatSPN. Application and theory of Petri nets and concurrency. Eds. G. Ciardo and
E. Kindler. Lecture notes in computer science ser. 8489:354-363. doi: 10.1007/978- 3-319-07734-5_19.
- Berthomieu, B., S. Dal Zilio, andL. Fronc. 2014. Model-checking real-time properties of an aircraft landing gear system using fiacre. Comm. Com. Inf. Sc. 433:110-125. doi: 10.1007/978-3-319-07512-9^.
- Wolf, K. 2016. Running LoLA 2.0 in a model checking competition. Transactions on Petri nets and other models of concurrency XI. Eds. M. Koutny, J. Desel, and J. Kleijn. Lecture notes in computer science ser. Berlin-Heidelberg: Springer-Verlag. 9930:274-285. doi: 10.1007/978-3-662-53401-4.13.
- Kharitonov, D. I., E. A. Golenkov, G. V. Tarasov, and D. V. Leontyev. 2015. Metod generatsii primerov modeley programm v terminakh setey Petri [A method of sample models of program construction in terms of Petri nets]. Modelirovanie i analiz infor- matsionnykh sistem [Modeling and Analysis of Information Systems] 22(4):563-577. doi: 10.18255/1818-1015-2015-4-563-577.
- Cormen, T.H., C.E. Leiserson, R. L. Rivest, and C. Stein. 2001. Introduction to algorithms. 2nd ed. Cambridge, MA: MIT Press; Boston: McGraw-Hill. 1184 p.
- Peterson, J. L. 1981. Petri net theory and the modeling of systems. Englewood Cliffs, NJ: Prentice-Hall. 241 p.
[+] About this article
Title
SOFTWARE IMPLEMENTATION OF A METHOD FOR GENERATION OF PETRI NETS OF LARGE SIZE
Journal
Systems and Means of Informatics
Volume 28, Issue 2, pp 99-115
Cover Date
2018-05-30
DOI
10.14357/08696527180208
Print ISSN
0869-6527
Publisher
Institute of Informatics Problems, Russian Academy of Sciences
Additional Links
Key words
Petri nets; program model; data structures; algorithm analysis; object-oriented programming
Authors
D. I. Kharitonov , G. V. Tarasov , and D. V. Leontyev
Author Affiliations
Institute of Automation and Control Processes, Far-Eastern Branch of the Russian Academy of Sciences, 5 Radio Str., Vladivostok 690041, Russian Federation
|