?
Verification of Nested Petri Nets Using an Unfolding Approach
P. 93-112.
Lomazova I. A., Ermakova V.
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 proved to be very helpful. In this paper we continue our research on applying unfoldings for NP-nets verication and compare unfolding of NP-net translated into classical Petri net with direct component-wise unfolding.
Publication based on the results of:
In book
Vol. 1591: Petri Nets and Software Engineering. International Workshop, PNSE'16, Torun, Poland, June 20-21, 2016. Proceedings. , CEUR Workshop Proceedings, 2016
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
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
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
В.А. Башкин, И.А. Ломазова, Cybernetics and Systems Analysis 2011 № 2 С. 31-39
Рассматривается проблема моделирования мультиагентных систем с бесконечным множеством состояний. Исследуются формализмы, основанные на обобщении сетей активных ресурсов. Определены новые способы моделирования: параметризованные АР-сети, двухуровневые АР-схемы и двухуровневые АР-сети. Показано, что эти формализмы обладают удобным синтаксисом для моделирования мультиагентных систем, в том числе систем со сложной модульной или иерархической структурой. Доказано, что параметризованные АР-сети и двухуровневые ...
Added: March 19, 2011
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
Daniil Frumin, Irina Lomazova, , in : VPT 2014. Second International Workshop on Verification and Program Transformation. Vol. 28: EPiC Series.: EasyChair, 2014. P. 19-35.
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 ...
Added: August 10, 2014
R.A. Nesterov, I.A. Lomazova, Proceedings of the Institute for System Programming of the RAS 2017 Vol. 29 No. 4 P. 21-38
Process mining offers various tools for studying process-aware information systems. They mainly involve several participants (or agents) managing and executing operations on the basis of process models. To reveal the actual behavior of agents, we can use process discovery. However, for large-scale processes, it does not yield models, which help understand how agents interact since ...
Added: September 6, 2017
Bernardinello L., Irina Lomazova, Roman Nesterov et al., , in : Proceedings of the International Workshop on Algorithms & Theories for the Analysis of Event Data 2018. Vol. 2115: CEUR Workshop Proceedings.: CEUR-WS.org, 2018. P. 23-38.
This paper presents a modular approach to discover process models for multi-agent systems from event logs. System event logs are filtered according to individual agent behavior. We discover workflow nets for each agent using existing process discovery algorithms. We consider asynchronous interactions among agents. Given a specification of an interaction protocol, we propose a general ...
Added: June 21, 2018
[б.и.], 2013
These are the proceedings of the International Workshop on Petri Nets and Software Engineering (PNSE’13) and the International Workshop on Modeling and Business Environments (ModBE’13) in Milano, Italy, June 24–25, 2013. These are co-located events of Petri Nets 2013, the 34th international conference on Applications and Theory of Petri Nets and Concurrency.
PNSE'13 presents the use of Petri ...
Added: August 17, 2013
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
Vladimir A. Bashkin, Lomazova I. A., Fundamenta Informaticae 2011 Vol. 109 No. 3 P. 223-236
A new formalism of Resource Driven Automata Nets (RDA-nets) is presented. A RDAnet has two levels: a system level is represented by a net of active resources, describing distribution of agents/resources and their interactions; agents in an object level are finite automata, communicating via ports and shared resources of a system level. RDA-nets are assigned ...
Added: February 2, 2013
Roman A. Nesterov, Irina A. Lomazova, , in : Proceedings of the MACSPro Workshop 2019. Vol. 2478: CEUR Workshop Proceedings.: CEUR-WS.org, 2019. P. 62-73.
Process models discovered from event logs of multi-agent systems may be complicated and unreadable. To overcome this problem, we suggest using a compositional approach. A system model is composed from agent models w.r.t. an interface. Morphisms guarantee that composition of correct models is correct. This study contributes to the practical implementation of the morphism-based compositional ...
Added: October 10, 2019
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 ...
Added: December 10, 2013
CEUR Workshop Proceedings, 2016
These are the proceedings of the International Workshop on Petri Nets and Software Engineering (PNSE’16) in Torun, Poland, June 20–21, 2016. It is a co-located event of • Petri Nets 2016 – the 37th International Conference on Applications and Theory of Petri Nets and Concurrency and • ACSD 2016 – the 16th International Conference on ...
Added: June 27, 2016
A. A. Sherstyugina, R. A. Nesterov, Proceedings of the Institute for System Programming of the RAS 2023 Vol. 35 No. 3 P. 11-32
The structure of a process model directly discovered from an event log of a multi-agent system often does not reflect the behavior of individual agents and their interactions. We suggest analyzing the relations between events in an event log to localize actions executed by different agents and involved in their asynchronous interaction. Then, a process ...
Added: October 31, 2023
Nesterov R.A., Mitsyuk A.A., Lomazova I.A., Proceedings of the Institute for System Programming of the RAS 2018 Vol. 30 No. 3 P. 285-302
In this paper, we present an approach to model and simulate models of multi-agent systems (MAS) using Petri nets. A MAS is modeled as a set of workflow nets. The agent-toagent interactions are described by means of an interface. It is a logical formula over atomic interaction constraints specifying the order of inner agent actions. ...
Added: July 10, 2018
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
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
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
Julio C. Carrasquel, Lomazova I. A., , in : ICPM Doctoral Consortium 2019. Vol. 2432: CEUR Workshop Proceedings.: CEUR-WS.org, 2019. Ch. 4. P. 1-12.
This paper presents our research on trading and multi-agent systems. Trading systems support the processes of buying/selling financial instruments between traders, so the validation of their correctness is a crucial task. Conversely, multi-agent systems is a current topic of interest within the analysis of interactive processes. We use Petri nets as the formalism for system ...
Added: August 28, 2019
Nesterov R., Bernardinello L., Lomazova I. A. et al., Software and Systems Modeling 2023 Vol. 22 P. 351-375
A process model discovered from an event log of a multi-agent system often does not fully cover certain viewpoints of its architecture. We consider those concerned with the structure of a model explicitly reflecting agent behavior and interactions. The direct discovery from an event log of a multi-agent system may result in an unclear model ...
Added: May 5, 2022
Vladimir A. Bashkin, Irina A. Lomazova, Transactions on Petri Nets and Other Models of Concurrency 2014 Vol. 9 P. 1-18
A resource workflow net (RWF-net) is a workflow net, supplied with an additional set of initially marked resource places. Resources can be consumed and/or produced by transitions. Neither the intermediate nor final resource markings are constrained, hence a net can have an infinite number of different reachable states. An RWF-net with k tokens in the ...
Added: December 7, 2014