A linear characterization of the Petri net reachability space corresponding to bounded-length fireable transition sequences and its implications for the structural analysis of process-resource nets with acyclic, quasi-live and strongly reversible process

The first part of this paper develops a linear characterization for the space of the Petri net markings that are reachable from the initial marking, M0, through bounded-length fireable transition sequences. The second part discusses the practical implications of this result for the liveness and reversibility analysis of a particular class of Petri nets known as process-resource nets with acyclic, quasi-live and strongly reversible process subnets.