On liveness analysis in mono-T-semiflow Petri nets based on choice-join pairs

This work introduces novel structural conditions to guarantee the liveness of Mono T-Semiflow (MTS) systems for any valid initial marking. In particular it shows that in MTS the existence of problematic choice-join pairs, a pure structural objects, is equivalent to the existence of transition firing sequences leading to deadlock markings. Moreover, such sequences always include an output transition of a choice place pc, capable of removing all the tokens from pc, but incapable of marking all the input places of a join transition tj In this situation tj will be dead, and since the net is MTS, then the net will reach a deadlock marking.