## 1 Introduction  
Petri nets are a valuable formalism used for modelling and analysis of concurrent systems [1]. Due to their nature and the possibility of graphical representation, they are specialized in capturing the behaviour of concurrent processes [2]. Such processes naturally appear widely in recent complex systems such as cyber-physical systems [3, 4], control systems [5], and manufacturing systems [6]. The application of Petri nets to concurrent systems allows for rigorous verification and validation processes, ensuring the reliability and efficiency of system operations [7]. Through their inherent properties and formal foundations, Petri nets enable the precise modelling of interactions within concurrent systems [8], offering a robust framework [9] for both theoretical exploration and practical implementation [10]. Petri nets are widely applied in the practical applications of concurrent systems. For example, they can be found in systems engineering in the organization of computer access to common resources [1]. Real-life examples of Petri net-based concurrent control systems can be found in [5], including among others beverage machine production, a smart home system, a traffic light controller, and a milling machine. It should be underlined that the last two case studies are oriented towards implementation within field programmable gate arrays (FPGA), with the further possibility of dynamic partial reconfiguration of the device [5]. Another example can be found in a study [11] where a power wheelchair is specified by a Petri net using a digital twin approach. The next case study of a control system presented in a research paper [12] details the design, simulation, and implementation of a supervision system for an industrial pumping system using Petri nets. What is more, a semiconductor fabrication control system is proposed in a paper [13]. Verification of concurrent systems described by Petri nets is an essential aspect of understanding and a key step in design [14]. Concurrent systems, characterized by multiple interacting components operating simultaneously, present unique challenges in terms of synchronization, communication, and resource management [15,16]. Petri nets, with their mathematical formalism, provide a structured approach to verify these systems [17], enabling the possibility of indicating potential fault areas in the model [18,19]. By means of Petri nets, it is possible to identify and analyse crucial properties such as liveness or boundedness which are vital for ensuring system reliability and robustness [20,21]. This paper aims to delve into advanced methods for analysing Petri net-based systems, highlighting an approach based on transition invariants. By leveraging Petri nets for the detailed analysis of concurrent systems, we can achieve more robust designs, ultimately contributing to the development of high-performance and reliable distributed systems [22]. The verification procedures of concurrent systems specified by Petri nets can be divided into two main groups [23]. The first one is based on state space exploration and reachability graph analysis, while the other one utilizes linear algebra techniques e.g., computation of invariants [24]. Let us describe them in detail, with special focus on the second group, since it is the background of the technique shown in this paper. Analysis of a reachability graph provides valuable insights into the state space of concurrent systems; however, it is often hindered by several significant limitations [5,25,26]. One of the primary challenges refers to the state explosion problem in the analysed Petri net-based concurrent system. Since the number of reachable states grows exponentially with the size of the system [27,28], the analysis time may be very long or it may even not be finished within the assumed time. This makes the construction and analysis of the reachability graph computationally infeasible, especially for large-scale systems [25].