## 2 Application of T-Invariants to the Verification of Petri Net-Based Concurrent Systems
### Definitions and Notations  
Graphically, a Petri net is represented by circles (places) and rectangles (transitions), connected by directed arcs. The dynamic behaviour of the modelled system is described by a sequence of transition firings. As a transition, it consumes tokens from input places and produces new ones in its output places [41]. The number of tokens needed to fire a given transition and the placement of the new ones is determined by the direction of input and output arcs [42]. The distribution of the tokens is called marking and symbolizes the state of the modelled system [43]. Let \(\mathbb{N}\) denote the set of nonnegative integers. Definition 1: A Petri net graph (Petri net structure) is a 3-tuple \((P,T,F)\), where \(P\) and \(T\) are finite, non-empty, and disjoint sets of places and transitions, respectively. \(F\subseteq(P\times T)\cup(T\times P)\) is called a flow relation of the net, represented by arcs with arrows from places to transitions or from transitions to places. **Definition 2**. : _A marking (a system state) of a Petri net graph \((P,T,F)\) is a mapping \(M:P\rightarrow\mathbb{N}\). \(M(p)\) denotes the number of tokens in place \(p\in P\)._  
**Definition 3**. : _A Petri net (marked Petri net) is a 4-tuple: \(N=(P,T,F,M_{0})\) such that \((P,T,F)\) is a Petri net graph, and \(M_{0}\) is its initial marking._  
**Definition 4**. : _A transition of a Petri net \(N\) is enabled if all its input places are marked (holding at least one token). The firing of an enabled transition removes a token from each of its input places and adds a token to each of its output places. A marking \(M\) is reachable if it can be obtained from the initial marking \(M_{0}\) by a sequence of transition firings._  
**Definition 5**. : _A place \(p\in P\) of a Petri net \(N\) is bounded (\(k\)-bounded) if for every reachable marking \(M\), \(M(p)\leq k\), where \(k\in\mathbb{N}\). A Petri net \(N\) is bounded if every place \(p\in P\) is bounded. A Petri net \(N\) is safe if each of its places is 1-bounded._  
**Definition 6**. : _An incidence matrix \(A_{|T|\times|P|^{n}}=\left[a_{ij}\right]\) (or just \(A\)) of a Petri net \(N\) is a matrix of integers, given by \(a_{ij}=-1\) if \(\left(p_{j},\ t_{i}\right)\in F\); \(a_{ij}=1\) if \(\left(t_{i},p_{j}\right)\in F\); \(a_{ij}=0\), otherwise._  
**Definition 7**. : _A transition invariant (\(t\)-invariant) is a vector \(\overrightarrow{y}:T\rightarrow\mathbb{N}\) such that \(A^{T}\overrightarrow{y}=\overrightarrow{0}\), where \(A^{T}\) is the transposed incidence matrix of the Petri net \(N\). The set of transitions corresponding to non-zero entries in a \(t\)-invariant \(\overrightarrow{y}\) is called a support of a transition invariant._  
**Definition 8**. : _A Petri net \(N\) is covered by \(t\)-invariants if every transition \(t\in T\) belongs to at least one support of a \(t\)-invariant._  
**Definition 9**. : _A deadlock is a marking such that no transition can be fired. A Petri net \(N\) is deadlock-free if no reachable marking \(M\) is a deadlock._  
**Definition 10**. : _A transition \(t\in T\) of a Petri net \(N\) is live for an initial marking \(M_{0}\) if for every reachable marking \(M\) a firing sequence from \(M_{0}\) exists, which contains transition \(t\). A Petri net \(N\) is live if all its transitions are live for \(M_{0}\)._  
Liveness is a much stricter property than deadlock-freeness. Indeed, a system may be deadlock-free, but not live. However, if the system is live, it is deadlock-free [33]. **Definition 11**.