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.

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.

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.