LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Past Seminars
(Un)decidability in Petri nets with name creation and replication
- Date
- Tuesday, February 09 2010 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Fernando Rosa Velardo (Universidad Complutense de Madrid)
The study of the expressive power of computation models in between Petri nets and Turing machines, and in particular of the class of Well Structured Transition Systems, is a challenging research problem. In this talk I will present two orthogonal extensions of Petri nets, with the capability of creating and managing pure names, and with a replication primitive, getting ν-Petri nets and g-RN systems, respectively. First, I will show how these two extensions are strongly equivalent, but only when a garbage collection mechanism is added for idle threads. However, when both extensions are considered simultaneously, we obtain a Turing complete model, that we call ν-RN systems. Then I will survey the known expressivity results for ν-Petri nets (and therefore, for g-RN systems). In particular, coverability, boundedness and termination are decidable, while reachability and place-boundedness are undecidable, so that ν-Petri nets are strictly in between Petri nets and Turing machines.
Then I will show how can we restrict ν-Petri nets (and, therefore, g-RN systems) and ν-RN systems in order to keep decidability of reachability and coverability, respectively. In particular, if we forbid synchronizations between the different components in a g-RN system, then reachability is still decidable. Analogously, if we forbid name communication between the different components in a ν-RN system, or restrict communication to happen only for a given finite set of names, we obtain decidability of coverability. Finally, I will comment on some ongoing work. This is joint work with David de Frutos-Escrig.