Preview

Труды Института системного программирования РАН

Расширенный поиск

Трансляция вложенных сетей Петри в классические сети Петри для верификации разверток

https://doi.org/10.15514/ISPRAS-2016-28(4)-7

Полный текст:

Аннотация

Вложенные сети Петри являются одним из удобных формализмов для моделирования и анализа поведения распределенных мультиагентных систем. Они естественным образом представляют структуру мультиагентных систем, так как фишки в системной сети сами являются классическими сетями Петри и могут иметь автономное поведение. Мультиагентные системы являются системами с высоким уровнем параллелизма. При верификации таких систем методами проверки модели (model checking) возникают серьезные трудности, связанные с взрывным ростом числа промежуточных состояний системы (state-space explosion problem). Для решения этой проблемы в литературе был предложен подход, основанный на построении развертки поведения системы. Ранее была изучена применимость разверток для верификации вложенных сетей Петри и предложен метод построения разверток для безопасных консервативных вложенных сетей Петри. В этой работе предлагается другой метод построения разверток для безопасных консервативных вложенных сетей Петри, основанный на трансляции таких сетей в классические сети Петри. Для классических сетей Петри затем применяются стандартные методы построения разверток. Также в работе обсуждаются сравнительные достоинства двух подходов.

Об авторах

В. О. Ермакова
National Research University Higher School of Economics
Россия


И. А. Ломазова
National Research University Higher School of Economics
Россия


Список литературы

1. Lomazova I.A. Nested Petri nets—a formalism for specification and verification of multi-agent distributed systems. Fundamenta Informaticae 43(1), 2000, pp. 195–214.

2. McMillan K.L. Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. Computer Aided Verification, Springer, 1992, pp. 164–177.

3. Nielsen M., Plotkin G., Winskel G. Petri nets, event structures and domains, part I. Theoretical Computer Science 13(1), 1981, pp. 85–108.

4. Frumin D., Lomazova I.A. Branching processes of conservative nested Petri nets. VPT 2014. Second International Workshop on Verification and Program Transformation Vol. 28: EPiC Series. EasyChair, 2014. P. 19-35.

5. Lomazova I.A., van Hee K.M., Oanea O., Serebrenik A., Sidorova N., Voorhoeve M. Nested nets for adaptive systems. Application and Theory of Petri Nets and Other Models of Concurrency, LNCS, 2006, pp. 241–260.

6. Lomazova I.A. Modeling dynamic objects in distributed systems with nested petri nets. Fundamenta Informaticae 51(1-2), 2002, pp. 121–133.

7. Lomazova I.A. Nested petri nets for adaptive process modeling. Pillars of computer science. Springer, 2008, pp. 460–474

8. L´opez-Mellado E., Villanueva-Paredes N., Almeyda-Canepa H. Modelling of batch production systems using Petri nets with dynamic tokens. Mathematics and Computers in Simulation 67(6), 2005, pp. 541–558.

9. Kahloul L., Djouani K., Chaoui A. Formal study of reconfigurable manufacturing systems: A high level Petri nets based approach. Industrial Applications of Holonic and Multi-Agent Systems. Springer, 2013, pp. 106–117.

10. Zhang, L., Rodrigues, B. Nested coloured timed Petri nets for production configuration of product families. International journal of production research 48(6), 2010, pp. 1805–1833.

11. Venero M.L.F., da Silva F.S.C. Modeling and simulating interaction protocols using nested Petri nets. Software Engineering and Formal Methods. Springer, 2013, pp. 135–150.

12. Chang L., He X., Lian J., Shatz S. Applying a nested Petri net modeling paradigm to coordination of sensor networks with mobile agents. Proc. of Workshop on Petri Nets and Distributed Systems, Xian, China, 2008, pp. 132–145.

13. Cristini F., Tessier C. Nets-within-nets to model innovative space system architectures. Application and Theory of Petri Nets. Springer, 2012, pp. 348–367.

14. Mascheroni M., Farina F. Nets-within-nets paradigm and grid computing. Transactions on Petri Nets and Other Models of Concurrency V. Springer, 2012, pp. 201–220.

15. Dworza´nski L.W., Lomazova I.A. On compositionality of boundedness and liveness for nested Petri nets. Fundamenta Informaticae 120(3-4), 2012, pp. 275–293.

16. Dworza´nski L., Lomazova I.A. CPN tools-assisted simulation and verification of nested Petri nets. Automatic Control and Computer Sciences 47(7), 2013, pp. 393–402.

17. Venero M.L.F. Verifying cross-organizational workflows over multiagent based environments. Enterprise and Organizational Modeling and Simulation. Springer, 2014, pp. 38–58.

18. Winskel G. Event structures. Springer, 1986.

19. Bonet B., Haslum P., Hickmott S., Thi´ebaux S. Directed unfolding of petri nets. Transactions on Petri Nets and Other Models of Concurrency I. Springer, 2008, pp. 172–198.

20. McMillan K.L. A technique of state space search based on unfolding. Form. Methods Syst. Des. 6(1), 1995, pp. 45–65.

21. Heljanko K. Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe petri nets. Fundamenta Informaticae 37(3), 1999, pp. 247–268.

22. Khomenko V., Koutny M. Branching processes of high-level Petri nets. In Garavel, H., Hatcliff, J., eds.: Tools and Algorithms for the Construction and Analysis of Systems. Volume 2619 of Lecture Notes in Computer Science. Springer, 2003, pp. 458–472.

23. Langerak R., Brinksma E. A complete finite prefix for process algebra. Computer Aided Verification, Springer, 1999, pp. 184–195.

24. Khomenko V., Koutny M., Vogler W. Canonical prefixes of Petri net unfoldings. Acta Informatica 40(2), 2003, pp. 95–118.

25. Khomenko V. Model Checking Based on Prefixes of Petri Net Unfoldings. Ph.D. Thesis, School of Computing Science, Newcastle University, 2003.

26. Esparza J., Heljanko K. Unfoldings: a partial-order approach to model checking. Springer, 2008.

27. Engelfriet J. Branching processes of Petri nets. Acta Informatica 28(6), 1991, pp.575–591.

28. Baldan P., Corradini A., Knig B., Schwoon S. Mcmillans complete prefix for contextual nets. Jensen, K., Aalst, W.M., Billington, J., eds.: Transactions on Petri Nets and Other Models of Concurrency I. Volume 5100 of Lecture Notes in Computer Science. Springer, 2008, pp. 199–220.

29. Fleischhack H., Stehno C. Computing a finite prefix of a time Petri net. Esparza J., Lakos C., eds.: Application and Theory of Petri Nets 2002. Volume 2360 of Lecture Notes in Computer Science. Springer, 2002, pp. 163–181.

30. Mascheroni, M. Hypernets: a Class of Hierarchical Petri Nets. Ph.D. Thesis, Facolt di Scienze Naturali Fisiche e Naturali, Dipartimento di Informatica Sistemistica e Comunicazione, Universit`a Degli Studi Di Milano Bicocca, 2010.

31. Jensen K., Kristensen L.M. Coloured Petri nets: modelling and validation of concurrent systems. Springer, 2009.


Для цитирования:


Ермакова В.О., Ломазова И.А. Трансляция вложенных сетей Петри в классические сети Петри для верификации разверток. Труды Института системного программирования РАН. 2016;28(4):115-136. https://doi.org/10.15514/ISPRAS-2016-28(4)-7

For citation:


Ermakova V.O., Lomazova I.A. Translation of Nested Petri Nets into Classical Petri Nets for Unfoldings Verification. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2016;28(4):115-136. (In Russ.) https://doi.org/10.15514/ISPRAS-2016-28(4)-7

Просмотров: 118


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)