Transition Invariants in the Analysis of Concurrent Systems Modelled by Petri Nets

Petri nets are a well-known mathematical apparatus that is commonly applied in the modeling of concurrent systems. Their main advantage relates to the possibility of graphical modeling, which results in the readable and intuitive specification of the system. Moreover, Petri nets are widely supported by analysis techniques, including formal verification methods. This paper focuses on the possible application of transition invariants to the analysis of Petri net-based concurrent systems. Such an approach seems to be much less popular in the literature than the analysis of place invariants. Nevertheless, our preliminary results indicate that analysis of transition invariants may result in very interesting information about the modeled system, especially in terms of crucial properties (e.g., liveness, boundedness).