Compositionality of Some Behavioral Properties for Free-Choice Nested Petri Nets

Dworzanski Leonid W.; Lomazova Irina A.

Глава

Compositionality of Some Behavioral Properties for Free-Choice Nested Petri Nets

P. 27-34.

Dworzanski L. W., Lomazova I. A.

Nested Petri nets (NP-nets) are Petri nets with net tokens. The liveness and boundedness problems are undecidable for two-level Nested Petri nets (NP-nets). Boundedness and liveness are still very hard to check even for plain Petri nets (EXPSPACE or worse). For the restricted class of free-choice Petri nets some problems become more amenable to analysis. There is the polynomial time algorithm to check if a free-choice Petri net is live and bounded. We prove that for some restricted class of NP-nets with free-choice components boundedness can be checked in a compositional way and define restrictions, under which liveness is also compositional. The motivating example of such restricted NP-nets is provided.

Язык: английский

Полный текст (PDF, 295 Кб)

Ключевые слова: Free-choice Petri nets nested Petri nets boundedness liveness

В книге

Compositionality of Some Behavioral Properties for Free-Choice Nested Petri Nets

Program Semantics, Specification and Verification: Theory and Applications. The conference materials. 6th International Computer Science Symposium in Russia

Под науч. редакцией: V. Nepomniaschy, V. Sokolov. Yaroslavl: Yaroslavl State University, 2011.

CPN Tools-Assisted Simulation and Verification of Nested Petri Nets

Dworzanski L. W., Lomazova I. A. Automatic Control and Computer Sciences. 2013. Vol. 47. No. 7. P. 393-402.

Nested Petri nets (NP-nets) is an extension of Petri net formalism within the “nets-within-nets” approach, when tokens in a marking are Petri nets wich have autonomous behavior and synchronize with the system net. The formalism of NP-nets allows modeling multilevel multiagent systems with dynamic structure in a natural way. Currently there is no tool support for NP-nets simulation and analysis. The paper proposes translation of NP-nets into colored Petri nets and using CPN Tools as a virtual machine for NP-nets modeling, simulation and automatic verification.

Добавлено: 10 декабря 2013

Towards a Translation from Nested Petri Nets into Colored Petri Nets

Dworzanski L. W., Lomazova I. A. In bk.: Program Semantics, Specification and Verification: Theory and Applications. The conference materials. Nizhny Novgorod: Nizhny Novgorod State University, 2012. P. 55-63.

Вложенные сети Петри (NP-nets) это сети Петри с сетевыми фишками. NP-nets являются расширением сетей Петри высокого уровня для моделирования активных объектов, мобильности и динамики в распределенных системах. В этой работе мы представляет алгоритм перевода двухуровневых NP-nets в поведенчески эквивалентную цветную сеть Петри, с целью применения методов и инструментов цветных сетей Петри для анализа NP-nets. Мы доказываем, что предложенная трансляция сохраняет динамическую семантику, с точностью до бисимуляционной эквивалентности.

Добавлено: 21 сентября 2012

Application and Theory of Petri Nets and Concurrency. 38th International Conference, PETRI NETS 2017, Zaragoza, Spain, June 25–30, 2017, Proceedings

Под науч. редакцией: W. van der Aalst, E. Best. Vol. 10258: Lecture Notes in Computer Science. Switzerland: Springer, 2017.

This book constitutes the proceedings of the 38th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2017, held in Zaragoza, Spain, in June 2017. Petri Nets 2017 is co-located with the Application of Concurrency to System Design Conference, ACSD 2017.

The 16 papers, 9 theory papers, 4 application papers, and 3 tool papers, with 1 short abstract and 3 extended abstracts of invited talks presented together in this volume were carefully reviewed and selected from 33 submissions. The focus of the conference is on following topics: Simulation of Colored Petri Nets, Petri Net Tools.- Model Checking, Liveness and Opacity, Stochastic Petri Nets, Specific Net Classes, and Petri Nets for Pathways.

Добавлено: 6 мая 2017

On Temporal Properties of Nested Petri Nets

Dworzanski L. W., Frumin D. I. In bk.: Proceedings of the 6th Spring/Summer Young Researchers’ Colloquium on Software Engineering, SYRCoSE 2012. Perm: 2012. P. 122-127.

Nested Petri nets is an extension of Petri net formalism with net tokens for modelling multi-agent distributed systems with complex structure. Temporal logics, such as CTL, are used to state requirements of software systems behaviour. However, in the case of nested Petri nets models, CTL is not expressive enough for specification of system behaviour. In this paper we propose an extension of CTL with a new modality for specifying agents behavior. We define syntax and formal semantics for our logic, and give small examples of its usage.

Добавлено: 20 сентября 2012

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

Ермакова В. О., Ломазова И. А. Труды Института системного программирования РАН. 2016. Т. 28. № 4. С. 115-136.

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

Добавлено: 21 октября 2016

Controlling Petri Net Behavior using Priorities for Transitions

Lomazova I. A., Popova-Zeugmann L. In bk.: Concurrency, Specification and Programming. CS&P 2014. Proceedings of the 23th International Workshop on Concurrency, Specification and Programming. Chemnitz, Germany, September 29 - October 1, 2014.. Vol. 1269: CEUR Workshop Proceedings (CEUR-WS.org). Berlin: Humboldt University of Berlin, 2014. P. 126-137.

In this paper we examine how it is possible to control Petri net behavior with the help of time constraints. Controlling here means to force a process to behave in a desirable way by ascribing priorities to transitions and hence transforming a classic Petri net into a Priority Petri net. Liveness and boundedness are crucial properties in many application areas, e.g. workflow modeling and bioinformatics. The main correctness property for workflow models is soundness, which can be reduced to the liveness and boundedness of a modified net. In biological models, liveness and boundedness are important for system stability. The problem of transforming a given live, but unbounded Petri net into a live and bounded one by adding priority constraints is studied in this paper. We specify necessary conditions for the solvability of this problem and present a method for ascribing priorities to net transitions in such a way that the resulting net becomes bounded while staying live.

Добавлено: 24 октября 2014

Controlling Petri Net Behavior using Priorities for Transitions

Lomazova I. A., Popova-Zeugmann L. Fundamenta Informaticae. 2016. Vol. 143. No. 1-2. P. 101-112.

Добавлено: 12 октября 2015