Monotonic Extensions of Petri Nets: Forward and Backward Search Revisited

In this paper, we revisit the forward and backward approaches to the verification of extensions of infinite state Petri Nets. As contributions, we propose an efficient data structure to represent infinite downward closed sets of markings and to compute symbolically the minimal coverability set of Petri Nets, we identify a subclass of Transfer Nets for which the forward approach generalizes and we propose a general strategy to use both the forward and the backward approach for the efficient verification of general Transfer Nets. Key words: Extended Petri Nets, Symbolic Verification, Efficient Data Structure, Safety Property.

• Type: Journal
• Year: 2002
• Where: ENTCS
• Authors: Alain Finkel, Jean-François Raskin, Mathias Samuelides, Laurent Van Begin
• Keywords: ENTCS 2002, Petri Nets, State Petri Nets, Transfer Nets