The paper proposes a novel decomposition method aimed at supporting decision-making in manufacturing systems. The main goal of the presented technique is an adequate proposal for dividing the production process flow in the manufacturing system by delegating the selected activities to the outsourcing mode. In order to obtain such separated activities within a production process, the modelled system is decomposed into the set of components (sets of places) that are executed externally. The presented idea involves Petri net and hypergraph theories. In particular, the system is modelled by a Petri net and further decomposed with the use of hypergraph’s transversals. The key advantage of the proposed algorithm is many decomposition possibilities, since the activities performed as part of the production process in an outsourcing mode may be specified precisely, exactly conforming to the production strategy. It can be treated as a tool supporting decision-making by managers in the context of delegating tasks from the production process in an outsourcing mode. Such study complements the results of the analysis of cost and efficiency of the production process realized in a manufacturing enterprise.

This work aims to analyze the efficiency and effectiveness of two invariant coverage verification methods for Petri net-based concurrent systems. The first algorithm is based on the classical approach, where the complete analysis of a Petri net’s incidence matrix is performed. This technique assures the correctness of results, but it may be inefficient due to the exponential computational complexity. The second algorithm applies an innovative idea of a Petri net’s incidence matrix transformation and examination. The main advantage of such an approach is its polynomial computational complexity. On the other hand, the method may not always be accurate and may not detect all errors in the examined system. This paper exhaustively verifies the efficiency (run-time) and effectiveness (correctness of the achieved results) of both methods. The theoretical analysis resutls are supported by the experimental ones via 386 benchmarks (Petri net models). In addition, besides the examination of the run-time of both methods, the number of iterations performed by them is computed and analysed.

The paper proposes a novel modelling and analysis technique of the system supporting implementation of additive manufacturing (AM) technologies specified by the interpreted Petri net. Nowadays, there is a need in a manufacturing enterprise to implement the new technologies supporting the realization of production, especially in terms of the possibility of unplanned crisis events. Managers expect such models to support their decisions in order to maintain or strengthen their competitive position thanks to the investments. Therefore, this paper proposes a system supporting the decision to implement AM technology, based on the interpreted Petri net, by utilizing its main advantages: the possibility of graphical modelling, and strong mathematical support of formal verification techniques. In particular, the proposed verification algorithm allows for detection of possible unbounded places. Contrary to the most popular analysis methods (which are bounded exponential in general case), it is proved that the presented technique is bounded by a cubic polynomial with the number of Petri net nodes. Finally, the presented modelling and analysis method is illustrated by a real-life case-study example of the decision-making model to support the implementation of AM technologies.Note to Practitioners—This paper is motivated by the limited performances in the existing modelling and analysis techniques of systems that support implementation of additive manufacturing (AM) technologies. In particular, the article proposes a system supporting the decision to implement AM technology, based on the interpreted Petri net. Existing approaches have important restrictions related to the exponential computational complexity of analysis methods. Therefore, verification of the model can be a real challenge to the designer. In contradistinction, the algorithm proposed in the paper permits the examination of the system in a polynomial time. The presented modelling and analysis ideas are illustrated by a real-life example of the decision-making system that utilizes implementation of AM technology. Managers of manufacturing enterprises, thanks to the use of the proposed approach, can assess the investment in AM technology in the following three unexpected situations: 1) delays in the delivery of materials and/or semi-finished products or the inability to receive materials and/or semi-finished products; 2) high employee turnover; 3) increasing costs of energy consumption. Thus, the application of this model allows for the harmonious conduct of manufacturing activities in conditions of unexpected situations.

Petri nets (PNs) are graphical and mathematical tools used to model a variety of discrete event systems and analyze their properties. Reachability is their fundamental property that is undecidable for PNs in general and has exponential complexity with respect to net size. One of the possible computation techniques of reachable states (markings) is based on the determination of legal firing sequences (LFSs) that correspond to a non-negative integer solutions (NISs) of a state equation. Our previous work has proposed an algorithm to decide the existence of LFSs corresponding to an NIS in polynomial time. However, it is impossible to check all NISs to decide a marking’s reachability in the case of an infinite number of NISs in a state equation. Hence, this work studies the relationship between the structure of a PN and the number of NISs of its state equation. Furthermore, an innovative method is proposed to modify its structure such that its state equation has no more than one NIS. The relationship between the properties of a PN and its modified one is studied in this article. We conclude that we can modify its structure while maintaining the function of the modeled system such that the reachability of the model can be decided in polynomial time. This can be viewed as a breakthrough result in the area of PN theory and applications. The correctness and time efficiency of the algorithm are verified by case studies and experiments. This work is important in putting PNs into the industrial use.

This article addresses the problem of optimal sensor selection for diagnosability enforcement of discrete event systems modeled with Petri nets. Given a nondiagnosable labeled Petri netlabeled Petri net (LPN) that may reach deadlocks, it can be enforced to be diagnosable by a novel systematic strategy through a mask labeling function. The proposed strategy employs a special nondeterministic finite automaton, namely, a simplified verifierSV, obtained from the original labeled Petri netLPN and a particular set of labels. Since we only need to silence sensors of some particular transitions rather than add or replace new sensors to transitions, it is more computationally efficient compared with other documented methods in the literature. In addition, we formulate and solve an integer linear programming problemILPP to optimize a set of given mask labeling functions. Finally, an algorithm is constructed to calculate the minimum value of$K$for a$K$-diagnosable system with multiple faults under the mask labeling function. Examples are presented to demonstrate the proposed method.

This work deals with the verification of a decision-making system for additive manufacturing (AM) technology adoption specified by a Petri net. An innovative verification technique of a Petri net-based system is oriented toward practical applications, and can detect errors at the early design and modelling stage. The idea is illustrated by a real-life case study of supporting decision making in AM technology adoption affecting supply chain management (SCM). Two main issues are addressed. Firstly, making optimal decisions about AM technology requires models rarely possessed within a company. Therefore, this work proposes a model supporting the decision making related to the implementation of AM technology, based on a Petri net, by utilizing its main advantages: graphical modelling, and strong mathematical support of formal verification techniques. Contrary to the most popular analysis methods (which are bounded exponentially in a general case), it is proved that the presented method is bounded by a cubic polynomial with net size. Secondly, an investment in AM technology is often financially assessed and does not affect other processes, as in our SCM case. Hence, strong connectivity within the proposed Petri net-based model is examined.

Integrating Additive Manufacturing (AM) technologies into manufacturing systems is regarded as a potential solution to improve the effectiveness of the production process flow in terms of the reduction of production costs, the involvement of human resources in the operation and the maximum use of materials. However, to date, the design of a model for the effectiveness of such integration is still an unresolved question. To find an answer to this question and help managers make decisions about AM technologies implementation, this paper applies Petri nets to the development of a formal model for the effectiveness of integrating AM technologies into manufacturing systems. The use of Petri nets in such context allows for modelling the correctness of the structure of the proposed production process improved by the AM technologies. The main novelty of the idea refers to the detailed description of the parameters of the production process integrating AM technologies. Moreover, new methods are proposed for boundedness and safeness verification of the Petri net-based manufacturing system (supported by an adequate algorithm, proposition, and proof). The presented model is illustrated through a real-life case study example of the production process with AM technology.

The paper deals with the modelling and analysis of physical resilient manufacturing systems (RMS) specified by the interpreted Petri net. Nowadays a need to improve manufacturing resilience is evident due to several unexpected situations currently on the market. The production strategy of mass customization application of RMS on the physical layer enables quick and cost-effective reaction to changing market and social conditions. Such systems should be capable of operating under any changes in production. Therefore, in this paper, a novel modelling concept of Petri net-based physical RMS for mass customisation production is proposed. The idea is based on the interpreted Petri net, which permits for additional specification of input and output signals of the system. Moreover, such a net ought to be live and bounded (or even safe), therefore a boundedness and safeness verification algorithm is developed. The proposed techniques are illustrated by the real-life case-study example of a RMS at the physical layer operating according to a mass customisation production strategy.

The paper proposes a novel analysis algorithm of the control part of cyber-physical systems specified by an interpreted Petri net. In particular, the three essential properties of Petri nets are studied: boundedness, safeness, and liveness. The presented idea combines linear algebra technique with reachability tree analysis. To clarify the presented concept, the method is illustrated by a real-life example of a cyber-physical system. Moreover, the experimental verification of the proposed technique was performed to examine its effectiveness and efficiency.

A method to find the minimized state machine cover of live and safe Petri nets (PNs) is proposed in this paper. It is required that a cover be obtained in some implementation methods of PN-based control algorithms and other applications such as data mining. Most of the known methods of its computation have at least exponential time and space complexity; this is true not only for the methods which guarantee a minimal cover is obtained but also for some methods of finding approximate solutions. The proposed algorithm is an approximation algorithm and has polynomial computational complexity. The experimental verification shows a very high efficiency of the presented technique. The proposed method is especially valuable in the case of large systems where a solution is obtained hundreds of times quicker than by other methods.

Recent years have witnessed the rapid development and deployment of cyber and computer technologies, thus highly influencing the design methodologies of discrete-event and hybrid systems, i.e., systems with discrete and mixed discrete-continuous states/inputs. Their prevalence can be found in almost all areas of human life, such as embedded software, automated manufacturing systems, work-flow management, logic controllers, communication protocols, robotics, transportation and mobility, military, smart buildings, etc. Given the criticality of such applications, such systems ought to be carefully modeled, thoroughly verified, and adequately analyzed.

The paper shows the application of interpreted nets for the specification of the cyber-physical system control unit. In particular, live and safe Petri nets are taken into account in order to present the concurrency relations in the designed system. Additionally, such nets include additional input and output signals used for communication with the environment. A CPS specified by the interpreted net can be easily verified (with the application of formal methods), analyzed, decomposed and even implemented (as an integrated or distributed system). The presented idea is illustrated by a manufacturing system case study.

The paper presents a novel design methodology of cyber-physical systems supported by computer aided tools. In particular, IOPT and Hippo tools are involved in the design and analysis techniques of the system. The proposed idea combines the main advantages of both tools by offering the complex design path of the control part of the cyber-physical system, including specification, analysis and verification, decomposition, and modelling stages. Additionally, the designer is able to choose the most suitable representation of the system (graphical or formal). The presented concepts are illustrated by a case-study example.

A novel prototyping technique for concurrent control systems implemented in field programmable gate array (FPGA) devices is proposed in the paper. The method allows for dynamic modification of the implemented system. It means that the functionality of a part of the controller can be changed, while the rest of the system is still running. The approach applies to unified modeling language state machine diagrams as a specification of the system. Contrary to other methods, the presented concept requires neither major changes to the design, nor the application of external, specialized tools. The proposed idea has been experimentally verified with the use of Xilinx FPGAs.

This paper focuses on the design and verification methods of distributed logic controllers supervising real-life processes. Such systems have to be designed very carefully and precisely in order to operate flawlessly and to meet user needs. We propose to use interpreted Petri nets as modeling formalism. A new design flow of distributed logic controllers is introduced. The methodology covers the development process from the specification stage to the final implementation of the controller in the distributed devices. In the proposed solution, the system is decomposed into separate modules that form a distributed system. Furthermore, the specification (before and after the decomposition process) is formally verified with the application of the model checking technique against predefined behavioral requirements. Finally, the system is implemented in real devices. The usage of formal methods and double model checking ensure the correct functionality of the designed distributed logic controller. The theoretical approach is supplemented by the practical experiments. Furthermore, the proposed idea is illustrated by an example of a smart home system.

In the paper, implementation of application specific logic controller for safety critical systems by means of Petri nets is described. The solution is based on duplicated main control unit and results comparison from both units. The design process of algorithm with use of Petri net is common for both unit. The hardware duplication is obtained during dual synthesis process. This process uses two different logic synthesis methods to obtain two different architectures for both control units. Such design flow simplify the process of realization of safety critical logic controllers.

The article focuses on some aspects regarding logic controller design. Control process is formally specified using interpreted Petri nets. It is then formally verified against behavioral properties using model checking technique and temporal logic. Formal specification can also be documented as UML activity diagram. One can then benefit from advantages of both specification techniques - Petri nets with a wide range of mathematical support and user-friendly UML activity diagrams. An interpreted Petri net can also be decomposed into state machine components (SMCs), each of them to be implemented in a separate module of FPGA device.

In the article we present a new algorithm of Petri net decomposition into State Machine Components (SMCs). The idea bases on the application of the comparability graph theory. The comparability graphs are classified as a subclass of the perfect graphs and have unique properties. If a graph belongs to the comparability class, many problems (like graph coloring, maximal clique problem) can be solved in polynomial time. Therefore, if the sequentiality graph of a Petri net belongs to comparability class, the whole decomposition process turns to be polynomial. The preliminary experiments have demonstrated the effectiveness of the proposed idea. Over 90% of concurrency and sequentiality graphs of tested benchmarks belong to the comparability class. The efficiency is even higher if the Petri net class is reduced to the EFC (Extended Free-Choice).