## 1 Introduction  
Petri nets are a mathematical modelling tool that is used to specify and verify concurrent control systems [1]. They were proposed in the 1960s by [PERSON] in his dissertation [2] and have since observed extensive use in areas such as computer science [3], mechanical engineering [4], and others [5]. Essentially, Petri nets consist of two types of nodes: places and transitions [6]. Places form states of the system, while transitions represent actions that can occur in the system [7]. Places and transitions are connected by arcs, which can show the direction of the flow of tokens representing the behaviour of the specified system [8]. Petri nets are especially suitable for modelling systems with complex interactions between multiple concurrent processes such as popular nowadays cyber-physical systems [9]. By representing these interactions graphically, Petri nets can provide easy insight into the behaviour of the system [3]. Furthermore, Petri nets can be analysed using formal methods to verify properties such as boundedness, safeness, or liveness and help identify potential problems or areas for improvement [10]. Boundedness [11] property shortly ensures a finite number of reachable states in the modelled system, safeness [12] makes binary behaviour of a Petri net for logical control while liveness is key in avoiding deadlocks or unwanted states [13]. A cyber-physical system (CPS) integrates computation with physical processes [14]. Its behaviour is defined by cyber and physical parts of the system [15, 16]. The first one (cyber) controls the objects and makes decisions, while the physical part refers to the real world and is disposed to environmental influences. The design techniques of CPS include the joint dynamics of computers, software, networks, as well as physical processes. Such a system is used in a variety of domains, including manufacturing systems, vehicular and transportation systems, medical and health-care systems, smart homes and buildings, social networks and gaming, etc. [17; 18; 19; 20]. A Petri net is one of the popular specification approaches of a CPS [12; 13; 18; 21]. Due to its concurrent nature and wide support of verification and validation techniques, a Petri net suits flawlessly the modelling of a CPS [22]. Moreover, the system can be easily and intuitively modelled by a graphical representation, while further designing steps are supported by mathematical techniques [23; 24]. One of the crucial steps of the design flow of Petri net-based CPS is the decomposition of the system. In short, this is a technique that is used in order to divide a large system into smaller, sub-systems. In the case of a Petri net, the system is usually split into sequential modules (sequential automata), called state machine components (SMCs). Decomposition is especially useful in the case of distributed CPS. In such systems each module can be implemented in a separate device [25; 26; 27; 28; 29]. Furthermore, decomposition plays an important role in the case of integrated systems, implemented within digital devices such as field programmable gate arrays (FPGAs). Recent FPGAs offer a very useful possibility of dynamic partial reconfiguration of the system. This technique permits for the replacement of a portion of the already implemented CPS without stopping the device [7; 19; 30; 31; 32]. This means that the functionality of the selected components of the system is modified while the remaining part of the CPS is still working. It is especially useful in the case of concurrent CPS that executes crucial operations that cannot be interrupted. Moreover, the decomposed modules analysed separately can simplify the analysis of complex cyber-physical systems [33]. There exist several popular decomposition techniques of the Petri net-based systems, each of which has its own advantages and disadvantages. In [34], a method based on shared places and/or shared transitions is presented. The paper shows that place invariants of the global model are the same as those of the decomposed model.