2026-06-08T04:01:58Zhttps://docta.ucm.es/rest/oai/requestoai:docta.ucm.es:20.500.14352/437262024-07-10T16:12:55Zcom_20.500.14352_14col_20.500.14352_15
Docta Complutense
author
Rosa Velardo, Fernando
author
Martos Salgado, María Rosa
author
Frutos Escrig, David De
2023-06-20T03:31:43Z
2023-06-20T03:31:43Z
2011
Rosa Velardo, F., Martos Salgado, M. R. & Frutos Escrig, D. «Accelerations for the Coverability Set of Petri Nets with Names». Fundamenta Informaticae, vol. 113, n.o 3-4, 2011, pp. 313-41. DOI.org (Crossref), https://doi.org/10.3233/FI-2011-611.
0169-2968
10.3233/FI-2011-611
https://hdl.handle.net/20.500.14352/43726
https//doi.org/10.3233/FI-2011-611
http://iospress.metapress.com/content/h730166n666n20nw/fulltext.pdf
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 ν-PNs 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 ν-PNs, 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 and Data Nets. Finally, we show that a slight modification of the forward analysis yields decidability of a weak form of boundedness called width-boundedness, and identify a subclass of ν-PN that we call dw-bounded ν-PN, for which the cover is computable.
eng
Accelerations for the coverability set of Petri nets with names
journal article
URL
https://docta.ucm.es/bitstreams/b062c5d3-4a59-40b9-88f5-395e5db4b480/download
File
MD5
4685f24933fd2e3365708fd1e3042fc4
260701
application/pdf
Frutos01oficialo.pdf
URL
https://docta.ucm.es/bitstreams/9d660227-091a-4be7-9c01-d17f1e62b493/download
File
MD5
f4e1229cdef63c3ab07594a60a1fda29
85344
text/plain
Frutos01oficialo.pdf.txt