Monotonic Extensions of Petri Nets: Forward and Backward Search Revisited |
| |
Authors: | A. Finkel J.-F. Raskin M. Samuelides L. Van Begin |
| |
Affiliation: | aLaboratoire Spécification et Vérification, CNRS UMR 8643 & ENS de Cachan, 61 av. du Prsident Wilson, 94235 Cachan cedex, France;bUniversité Libre de Bruxelles, Blvd du Triomphe, 1050 Bruxelles, Belgium |
| |
Abstract: | 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. |
| |
Keywords: | Extended Petri Nets Symbolic Verification Efficient Data Structure Safety Property |
本文献已被 ScienceDirect 等数据库收录! |
|