## 2 Application of T-Invariants to the Verification of Petri Net-Based Concurrent Systems
### Application of T-Invariant Cover in the Verification and Analysis of Petri Net-Based Systems  
Broadly speaking, invariant coverage examination is widely used in the analysis of Petri net-based concurrent systems. Invariants have been fundamental concepts in Petri net theory since its inception. Examination of invariant coverage provides insights into the structure of the system modelled by the Petri net [29]. Also, t-invariant coverage proves that the given net is strongly connected, which means that from every marking there is a possible firing sequence to reach every other marking [45]. It is worth noticing that if a bounded system is live, then it is covered by transition invariants [45]. This is an especially important property that we will use in our divagations later. Since invariants represent the cyclic behaviour of the system, lack of coverage of a given transition means that this transition does not participate in a closed cycle [29]. While there is a possibility that it may be fired eventually, tokens produced by it will never recreate the original initial marking of the given Petri net. In systems biology, analogous concepts include chemical moieties and conservation relations, as well as elementary modes and extreme pathways, which are explored within the context of biochemical networks. To streamline the generating system of the solution space, particularly in the presence of numerous reversible reactions, the concept of generic pathways (representing minimal metabolic behaviour) has been proposed. This approach is especially useful for simplifying complex biochemical networks. For biochemical systems that lack reversible reactions, the concepts of t-invariants, elementary modes, extreme pathways, and generic pathways are effectively equivalent [46]. In manufacturing systems, t-invariants help in identifying invariant properties of workflows, ensuring that certain tasks can be repeated indefinitely without leading to deadlocks or resource contention. In communication networks, they are used to analyse and verify the consistency and reliability of data transmission processes, ensuring that messages can circulate within the network without loss or bottleneck. Additionally, their application extends to software engineering as well, particularly in the verification of concurrent and parallel programs, where t-invariants help in proving the correctness and reliability of software systems by ensuring that all possible execution paths are accounted for and managed effectively [47; 48]. It is worth noticing that if a given transition is not part of any invariant, then it may potentially increase or decrease the number of tokens in the circuit if it fires. This may  
Figure 1: An exemplary Petri net with two minimal t-invariants. indicate that the net is unbounded or decreasing the number of tokens [49]. On the other hand, the liveness property in a Petri net means that from any possible marking the net may reach any other marking after several firings [29]. Following this trail, any transition included in any support is fireable. But the ones that are not covered may be permanently disabled [50], thus impacting the liveness property [51]. Transition invariants represent linearly independent solutions of the linear equations from the incidence matrix of a given Petri net. Therefore, they describe the basic system structure, and positive linear combinations of t-invariants can be used to describe the system behaviour in all possible cases (i.e., for any initial marking). Moreover, invariants are associated with home spaces and semi-flows [52]. A home space in a Petri net is a set of markings (states) that can be reached from any reachable marking in the net. Invariants can be deduced from minimal semi-flows and relate to smaller footprints, which are likely to have an impact on optimization of the analysis. In turn, home spaces are used to prove the liveness of the model [52]. Finally, let us discuss limitations of the methods that are based on transition invariants.