?
Branching Processes of Conservative Nested Petri Nets
P. 19-35.
Daniil Frumin, Irina Lomazova
Nested Petri nets (NP-nets) is an extension of the Petri nets formalism within the “nets-within-nets” approach, when tokens in a marking are themselves Petri nets which have autonomous behavior and synchronize with the system net. The formalism of NP- nets allows modeling multi-level multi-agent systems with dynamic structure in a natural way. In this paper we define branching processes and unfoldings for conservative NP- nets, i.e. for NP-nets with a persistent set of agents. We prove that NP-nets unfoldings satisfy the fundamental property of unfoldings, and thus can be used for verification of conservative NP-nets in line with classical unfolding methods.
Publication based on the results of:
In book
Vol. 28: EPiC Series. , EasyChair, 2014
Ermakova V., Lomazova I. A., Труды Института системного программирования РАН 2016 Т. 28 № 4 С. 115-136
Nested Petri nets (NP-nets) have proved to be one of the convenient formalisms for distributed multi-agent systems modeling and analysis. It allows representing multi-agent systems structure in a natural way, since tokens in the system net are Petri nets themselves, and have their own behavior. Multi-agent systems are highly concurrent. Verification of such systems with model ...
Added: October 21, 2016
Lomazova I. A., Ermakova V., , in : CEUR Workshop Proceedings. Vol. 1591: Petri Nets and Software Engineering. International Workshop, PNSE'16, Torun, Poland, June 20-21, 2016. Proceedings.: CEUR Workshop Proceedings, 2016. P. 93-112.
Nested Petri nets (NP-nets) is an extension of the Petri nets formalism within the nets-within-nets approach, allowing to model systems of interacting dynamic agents in a natural way. One of the main problems in verifying of such systems is the State Explosion Problem. To tackle this problem for highly concurrent systems the unfolding method has ...
Added: June 28, 2016
EasyChair, 2014
This volume contains the papers to be presented at VPT 2014: Second International Workshop on Verification and Program Transformation to be held on July 17-18, 2014 in Vienna. The workshop is an event of the Vienna Summer of Logic 2014 and it is co-located with the 26th International Conference on Computer Aided Verification CAV 2014. ...
Added: August 10, 2014
Carrasquel Gamez J. C., Lomazova I. A., Itkin I., , in : Proceedings of the MACSPro Workshop 2019. Vol. 2478: CEUR Workshop Proceedings.: CEUR-WS.org, 2019. P. 92-103.
Electronic trading systems provide the computational support for stock exchanges. Liquid markets use order-driven systems, i.e., where client requests, for trading financial instruments, are served through individual orders. This paper presents Petri net models assembling some crucial processes executed within order-driven systems such as orders submission, application of precedence rules, and the order matching mechanism. ...
Added: October 14, 2019
Mecheraoui K., Carrasquel Gamez J. C., Lomazova I. A., , in : Proceedings of the Conference on Modeling and Analysis of Complex Systems and Processes 2020 (MACSPro 2020). Vol. 2795.: CEUR Workshop Proceedings, 2020. P. 34-45.
This paper presents a compositional conformance checking approach between nested Petri nets and event logs of multi-agent systems. By projecting an event log onto model components, one can perform conformance checking between each projected log and the corresponding component. We formally demonstrate the validity of our approach proving that, to check fitness of a nested ...
Added: January 14, 2021
Mecheraoui K., Carrasquel Gamez J. C., Lomazova I. A., / Cornell University. Series Computer Science "arxiv.org". 2020.
This paper presents a compositional conformance checking approach between nested Petri nets and event logs of multi-agent systems. By projecting an event log onto model components, one can perform conformance checking between each projected log and the corresponding component. We formally demonstrate the validity of our approach proving that, to check fitness of a nested ...
Added: October 20, 2020
Mitsyuk A. A., Lomazova I. A., van der Aalst W., Automatic Control and Computer Sciences 2017 Vol. 51 No. 7 P. 709-723
Added: December 1, 2017
Dworzanski L. W., Lomazova I. A., , in : Program Semantics, Specification and Verification: Theory and Applications. The conference materials. 6th International Computer Science Symposium in Russia. : Yaroslavl : Yaroslavl State University, 2011. P. 27-34.
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. ...
Added: March 23, 2013
Lomazova I. A., Popova-Zeugmann L., Fundamenta Informaticae 2016 Vol. 143 No. 1-2 P. 101-112
In this paper we examine how it is possible to control Petri net behavior with the help of transition priorities. Controlling here means forcing a process to behave in a stable way by ascribing priorities to transitions and hence transforming a classic Petri net into a Priority Petri net. For Petri net models stability is ...
Added: October 12, 2015
Dworzanski L. W., , in : Formal Modeling and Analysis of Timed Systems. Vol. 9884.: Switzerland : Springer, 2016. Ch. 1. P. 3-18.
The nested Petri nets are a nets-within-nets formalism convenient for modelling systems that consist of distributed mobile agents with individual behaviour. The formalism is supported by developed verification methods based on structural analysis and model checking techniques. Time constraints are crucial for many safety critical and everyday IoT systems. Recently, the non Turing-complete time semantics ...
Added: September 13, 2016
Dworzanski L. W., Frumin D. I., , in : Proceedings of the 7th Spring/Summer Young Researchers’ Colloquium on Software Engineering, SYRCoSE 2013. : Kazan : -, 2013. P. 9-14.
Nested Petri nets is an extension of Petri net formalism with net tokens for modelling multi-agent distributed systems with complex structure. While having a number of interesting properties, NP-nets have been lacking tool support. In this paper we present the NPNtool toolset for NP-nets which can be used to edit NP-nets models and check liveness ...
Added: June 18, 2013
Kulagin V., Информатизация образования и науки 2015 № 4(28) С. 133-147
The methods of constructing tensors transform (TT) used in the analysis and synthesis of network models of complex systems, presented in different coordinate systems are described in the article. The general method of construction of the TT, as well as a method of building TT for network models, decomposed into many of the automate synchronization ...
Added: February 25, 2016
Carrasquel Gamez J. C., Lomazova I. A., Rivkin A., , in : Proceedings of the International Workshop on Petri Nets and Software Engineering co-located with 41st International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2020). Vol. 2651: CEUR Workshop Proceedings.: CEUR-WS.org, 2020. P. 118-137.
Trading systems have become sophisticated multi-agent in-frastructures with complex development cycles. This is why the financialindustry constantly seeks for novel approaches to design and validate these systems. We propose the use of models to support such tasks. On the one hand, these models need to describe how objects (e.g., ordersto buy/sell securities) are shared by ...
Added: October 19, 2020
Vladimir A. Bashkin, Lomazova I. A., Novikova Y., , in : Parallel Computing Technologies. 12th International Conference, PaCT 2013, St. Petersburg, Russia, September 30-October 4, 2013, Proceedings. Vol. 7979: Lecture Notes in Computer Science.: Berlin, Heidelberg : Springer, 2013. P. 13-25.
The paper presents a formalism and a tool for modelling and analysis of distributed real-time systems of mobile agents. For that we use a time extension of our Resource Driven Automata Nets (TRDA-nets) formalism. A TRDA-net is a two-level system. The upper level represents distributed environment locations with a net of active resources. On the ...
Added: October 1, 2013
Lomazova I. A., Romanov I., Fundamenta Informaticae 2013 Vol. 128 No. 1-2 P. 129-141
In this work we consider modeling of services with workflow modules, which form a Petri net subclass. The service compatibility problem is to answer the question, whether two services fit together, i.e. whether the composed system is correct. We study complementarity of resources, produced/consumed by two services—a necessary condition for the service compatibility. Resources, which ...
Added: November 18, 2013
Dworzanski L. W., Михайлов В. Е., Proceedings of the Institute for System Programming of the RAS 2017 Vol. 29 No. 4 P. 175-190
Well-structured transition systems (WSTS) became a well-known tool in the study of concurrency systems for proving decidability of properties based on coverability and boundedness. Each year brings new formalisms proven to be WSTS systems. Despite the large body of theoretical work on the WSTS theory, there has been a notable gap of empirical research of ...
Added: October 1, 2017
Петровский Д. В., Кокурин Д. И., Логистика и управление цепями поставок 2017 № 6 С. 125-132
In this paper, the use of the apparatus of stochastic Petri networks applying to the analysis of supply chains is considering. The storage module and the production module of the logistics system and their interaction with other elements of the system have been analyzed. First, the considered logistical system was represented in the form of ...
Added: November 28, 2017
Lomazova I. A., Popova-Zeugmann L., Bartels A., , in : International Conference on Control, Decision and Information Technologies, CoDIT 2017, Barcelona, Spain, April 5-7, 2017. : IEEE, 2017. P. 0236-0241.
In this paper we study how it is possible to control Petri net behavior using priority and time constraints. Controlling here means forcing a process to behave in a stable way by associating priorities, or time intervals to transitions and hence transforming a classic Petri net into a Petri net with priorities, or a Time ...
Added: November 10, 2017
Lomazova I. A., , in : Application and Theory of Petri Nets and Concurrency. 38th International Conference, PETRI NETS 2017, Zaragoza, Spain, June 25–30, 2017, Proceedings. Vol. 10258: Lecture Notes in Computer Science.: Switzerland : Springer, 2017. P. 19-34.
Tokens in Petri net models may represent a control flow state, or resources produced/consumed by transition firings. From the resource perspective a part of a Petri net marking can be considered as a store needed for ensuring some future system behavior. The talk is devoted to the study of several types of resource equivalence in ...
Added: May 6, 2017
K.G. Serebrennikov, Proceedings of the Institute for System Programming of the RAS 2019 Vol. 31 No. 4 P. 163-174
. In this paper, we propose an approach to implementation of the algorithm for computing transition priorities for live Petri nets. Priorities are a form of constraints which can be imposed to ensure liveness and boundedness of a Petri net model. These properties are highly desirable in analysis of different types of systems, ranging from business processes systems ...
Added: October 24, 2019
Dworzanski L. W., Formal Methods in System Design (Нидерланды, целевой журнал) 2020
The nested Petri nets (NP-nets) are a nets-within-nets formalism convenient for modelling systems that consist of distributed mobile agents with individual behaviour. The expressiveness of
the NP-nets formalism is greater than that of classical place/transition nets; and, the formalism
allows to model open multiagent systems with agents being introduced, eliminated, and cloned.
Several verification methods based on structural ...
Added: November 2, 2019
Lomazova I. A., Romanov I., , in : Concurrency, Specification and Programming. CS&P’2012. Berlin, September 26 – September 28, 2012. Volume 2. Vol. 2. Issue 225.: Berlin : Humboldt University of Berlin, 2012. P. 239-250.
In this work we consider modeling of services with workflow modules, which are a subclass of Petri nets. The service compatibility problem is to answer the question, whether two Web services fit together, i.e. whether the composed system is sound. We study complementarity of service produced/consumed resources, that is a necessary condition for the service ...
Added: November 19, 2012
Mitsyuk A. A., Shugurov I., Моделирование и анализ информационных систем 2014 Т. 21 № 4 С. 181-198
Process mining is a new emerging discipline related to process management, formal process models, and data mining. One of the main tasks of process mining is the model synthesis (discovery) based on the event logs. A wide range of algorithms for process model discovery, analysis, and enhancement are developed. The real-life event logs often contain ...
Added: October 20, 2014
Vladimir A. Bashkin, Lomazova I. A., Fundamenta Informaticae 2012 Vol. 120 No. 3-4 P. 243-257
Resource-driven automata (RDA) are finite automata, sitting in the nodes of a finite system net and asynchronously consuming/producing shared resources through input/output system ports (arcs of the system net). RDAs themselves may be resources for each other, thus allowing the highly flexible structure of the model. It was proved earlier, that RDA-nets are expressively equivalent ...
Added: November 28, 2012