Verification of Nested Petri Nets Using an Unfolding Approach
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.
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 Nets (P/T-Nets, Coloured Petri Nets and extensions) in the formal process of software engineering, covering modelling, validation, and veriﬁcation, as well as their application and tools supporting the disciplines mentioned above.
ModBE’13 provides a forum for researchers from interested communities to investigate, experience, compare, contrast and discuss solutions for modeling in business environments with Petri nets and other modeling techniques.
Nested Petri nets (NP-nets) are Petri nets with net tokens - an extension of high-level Petri nets for modeling active objects, mobility and dynamics in distributed systems. In this paper we present an algorithm for translating two-level NP-nets into behaviorally equivalent Colored Petri nets with the view of applying CPN methods and tools for nested Petri nets analysis. We prove, that the proposed translation preserves dynamic semantics in terms of bisimulation equivalence.
Process mining is a relatively new field of computer science which deals with process discovery and analysis based on event logs. In this work we consider the problem of discovering workflow nets with cancellation regions from event logs. Cancellations occur in the majority of real-life event logs. In spite of huge amount of process mining techniques little has been done on cancellation regions discovery. We show that the state-based region algorithm gives labeled Petri nets with overcomplicated control flow structure for logs with cancellations. We propose a novel method to discover cancellation regions from the transition systems built on event logs and show the way to construct equivalent workflow net with reset arcs to simplify the control flow structure.
This book constitutes the proceedings of the 37th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2016, held in Toruń, Poland, in June 2016. Petri Nets 2016 was co-located with the Application of Concurrency to System Design Conference, ACSD 2016. The 16 papers including 3 tool papers with 4 invited talks presented together in this volume were carefully reviewed and selected from 42 submissions. Papers presenting original research on application or theory of Petri nets, as well as contributions addressing topics relevant to the general field of distributed and concurrent systems are presented within this volume.
There have been implemented engineering and development of multi-agent recommender system «EZSurf» that performs analysis of interests and provides recommendations for the social network «VKontakte» users based on the data from profile of particular user. During the work process different methods and technological solutions have been analyzed with examination of their advantages and disadvantages. Besides of that the comparative analysis of analogous products has been held where the most similar is Russian start-up service - Surfingbird. Based on this analysis the decision of recommender system implementation and integration has been accepted. The feature of this system is that it uses social network “VKontakte” profile for user’s data collection and API of third-party services (LastFM, TheMovieDB) for an extraction of information about similar objects. Such an approach contributes into optimization of recommender system, because it does not require creation of its own object classification system and objects database. The functionality of multi-agent system was separated between three agents. First agent (Collector) collects user data from “VKontakte” profile using VK API. Second agent (Analyzer) collects similar objects from databases of thitd-party services (LastFM, TheMovieDB) that will be the criteria for further search of recommendatory content. For search and selection of information an agent (Recommender) that works as web-crawler has been implemented. System «EZSurf» can be exploited by the users of social network “VKontakte” in everyday life for time economy on web-surfing process. At the same time they will get recommendations on content that are filtered depending on preferences of every particular user.
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.
To verify realtime properties of UML statecharts one may apply a UPPAAL, toolbox for model checking of realtime systems. One of the most suitable ways to specify an operational semantics of UML statecharts is to invoke the formal model of Hierarchical Timed Automata. Since the model language of UPPAAL is based on Networks of Timed Automata one has to provide a conversion of Hierarchical Timed Automata to Networks of Timed Automata. In this paper we describe this conversion algorithm and prove that it is correct w.r.t. UPPAAL query language which is based on the subset of Timed CTL.