Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

2 2011

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Decidability Problems in Petri Nets with Names and Replication

Rosa-Velardo F., Frutos-Escrig D. de

Fundamenta Informaticae

2011

Vol. 105, nr 3

291-317

In this paper we study decidability of several extensions of P/T nets with name creation and/or replication. In particular, we study how to restrict the models of RN systems (P/T nets extended with replication, for which reachability is undecidable) and í-RN systems (RN extendedwith name creation, which are Turing-complete, so that coverability is undecidable), in order to obtain decidability of reachability and coverability, respectively. We prove that if we forbid synchronizations between the different components in a RN system, then reachability is still decidable. Similarly, if we forbid name communication between the different components in a &nuRN system, or restrict communication so that it is allowed only for a given finite set of names, we obtain decidability of coverability. Finally, we consider a polyadic version of ν-PN (P/T nets extended with name creation), that we call pν-PN, in which tokens are tuples of names. We prove that pν-PN are Turing complete, and discuss how the results obtained for ν-RN systems can be translated to them.

Accelerations for the Coverability Set of Petri Nets with Names

Rosa-Velardo F., Martos-Salgado M., Frutos-Escrig D. de

Fundamenta Informaticae

2011

Vol. 113, nr 3/4

313-341

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 v-PN, for which the cover is computable.