Sciweavers

Share
APN
2010
Springer

Forward Analysis for Petri Nets with Name Creation

11 years 9 months ago
Forward Analysis for Petri Nets with Name Creation
Pure names are identifiers with no relation between them, except equality and inequality. In previous works we have extended P/T nets with the capability of creating and managing pure names, obtaining -APNs and proved that they are strictly well structured (WSTS), so that coverability and boundedness are decidable. Here we use the framework recently developed by Finkel and Goubault-Larrecq for forward analysis for WSTS, in the case of -APNs, to compute the cover, that gives a good over approximation of the set of reachable markings. We prove that the least complete domain containing the set of markings is effectively representable. Moreover, we prove that in the completion we can compute least upper bounds of simple loops. Therefore, a forward Karp-Miller procedure that computes the cover is applicable. However, we prove that in general the cover is not computable, so that the procedure is non-terminating in general. As a corollary, we obtain the analogous result for Transfer Data nets...
Fernando Rosa Velardo, David de Frutos-Escrig
Added 06 Dec 2010
Updated 06 Dec 2010
Type Conference
Year 2010
Where APN
Authors Fernando Rosa Velardo, David de Frutos-Escrig
Comments (0)
books