Coverability, Termination, and Finiteness in Recursive Petri Nets

In the early two-thousands, Recursive Petri nets have been introduced in order to model distributed planning of multi-agent systems for which counters and recursivity were necessary. Although Recursive Petri nets strictly extend Petri nets and context-free grammars, most of the usual problems (reachability, coverability, finiteness, boundedness and termination) were known to be solvable by using non-primitive recursive algorithms. For almost all other extended Petri nets models containing a stack, the complexity of coverability and termination are unknown or strictly larger than EXPSPACE. In contrast, we establish here that for Recursive Petri nets, the coverability, termination, boundedness and finiteness problems are EXPSPACE-complete as for Petri nets. From an expressiveness point of view, we show that coverability languages of Recursive Petri nets strictly include the union of coverability languages of Petri nets and context-free languages. Thus we get a more powerful model than Petri net for free.

Modeling of the processes of extracting rules from Neural Network components with Petri nets

The paper deals with the use of extended Petri nets in modeling the processes of extracting rules from neural network components. The mathematical model for extracting rules from neural network components based on a modified timed Petri net is constructed, followed by an analysis of its dynamic behavior based on a timed reachability graph, which is a set of all its states that can be reached when a finite number of transitions are fired. The proposed model allows us to move from the initial detailed structure to its simplified description, which preserves the possibility of obtaining information about the structure and dynamic behavior of the neural network system. The proposed approach can be used in the synthesis of cognitive systems with a neural network organization to provide computational support for the functions of forming, learning, and correcting cognitive networks that display neural network models.

A Petri Nets Evolution Method that Supports BPMN Model Changes

The correctness of the business process modelling notation (BPMN) is essential for software success, and the BPMN formalization is the foundation of the correctness verification process. However, dynamically adapting the formalized BPMN model to changes in the BPMN model and protecting tokens from being lost in the remapping formalization are the main limitations of the BPMN formalization under changing business requirements. To overcome these limitations, an approach for evolving a Petri nets model according to the BPMN changes is proposed in this paper. In this approach, a check algorithm is designed to identify the differences between the original BPMN model and the updated BPMN model. Then, the evolution rules of the extended Petri nets (EPN) model are defined according to the results of the checking program. Finally, these evolution rules are described in the query/view/transformation operational mapping (QVTo) language and implemented in the Eclipse platform. We demonstrate the effectiveness of the evolution of the BPMN formalization using a case study of the Web Payment business system. Moreover, the dynamic evolution of the BPMN formalization can maintain the consistency between the original model and the updated model, and this consistency has been successfully verified.

Multiobjective Heuristic Scheduling of Automated Manufacturing Systems Based on Petri Nets

In practice, automated manufacturing systems usually have multiple, incommensurate, and conflicting objectives to achieve. To deal with them, this paper proposes an extend Petri nets for the multiobjective scheduling of AMSs. In addition, a multiobjective heuristic A* search within reachability graphs of extended Petri nets is also proposed to schedule these nets. The method can obtain all Pareto-optimal schedules for the underlying systems if admissible heuristic functions are used. Finally, the effectiveness of the method is illustrated by some experimental systems.

Model of Process Synchronization in Through Analysis

Synchronization of parallel processes of distributed information systems (DIS) has been largely determined by decisions taken at the stages of their design. Having already been in structural and functional models, when determining cause- and-effect relationships for events and actions in DIS components, it becomes necessary to coordinate them. In the proposed multilevel systemic, structural and functional synchronization model, a hierarchy of such causal relationships with interlevel mappings, inheritance and encapsulation of events and actions have been formed. The model has been also based on hierarchical extended Petri nets, which make it possible to represent various aspects of a special analysis of technical diagnostics, in particular, analysis of correctness, verification, testing, for the adopted display of the asynchronous-behavioral nature of the multilevel interaction of DIS processes. Features of the synchronization model include mapping operations for cross- level inheritance and encapsulations that synchronize events and actions, as well as end-to-end synchronized quasi-order relationships and compatibility for them. The synchronization model is also distinguished by the possibility of specializing its objects, operations and relations for the tasks of check and recognition of behavioral properties set for analysis and verification, basic in technical diagnostics, including in online and offline testing. The synchronization model has allowed one to determine the formal conditions for methods of end-to-end asynchronous coordination of events and actions of multi-level models, that represent design solutions for DIS, in particular, for technical diagnostics methods, and also to reduce the computational complexity of a special synchronization analysis due to an end-to-end decomposition approach. The dimension of the synchronization model has been estimated using the representation of Petri net graphs and special graphs of reachable states using list structures. The above estimates determine the limits of applicability of the formal synchronization model.

Extremely Fast Heuristic Event-Driven Job Shop Scheduler With a New Class of Extended Petri Nets

A very fast scheduling system is proposed and experimentally investigated. The system consists of a job shop manager and dynamic models of machines. A schedule is created in the course of a close cooperation with models of the machines that generate driving events for the scheduler. The system is implemented with a new class of extended Petri nets and runs in the environment of the Petri-net tool WINSIM. The scheduler creates a schedule sequentially, without any form of enumerative search. To investigate the scheduler performance, a large number of experiments were conducted with the use of few strategies. Due to a unique mechanism of monitoring of triggering events in the Petri net, the developed scheduler runs at least hundreds of times faster than any known single-processor job shop scheduler.

A Web Interface for Petri Nets with Transits and Petri Games

Developing algorithms for distributed systems is an error-prone task. Formal models like Petri nets with transits and Petri games can prevent errors when developing such algorithms. Petri nets with transits allow us to follow the data flow between components in a distributed system. They can be model checked against specifications in LTL on both the local data flow and the global behavior. Petri games allow the synthesis of local controllers for distributed systems from safety specifications. Modeling problems in these formalisms requires defining extended Petri nets which can be cumbersome when performed textually.In this paper, we present a web interface (The web interface is deployed at http://adam.informatik.uni-oldenburg.de.) that allows an intuitive, visual definition of Petri nets with transits and Petri games. The corresponding model checking and synthesis problems are solved directly on a server. In the interface, implementations, counterexamples, and all intermediate steps can be analyzed and simulated. Stepwise simulations and interactive state space generation support the user in detecting modeling errors.