Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

(Un)decidability in Petri nets with name creation and replication

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

 Fernando Rosa Velardo
Le mardi 09 février 2010 à 11:00
Salle de Conférence (Pavillon des Jardins)
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.


À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

mar. 19 février

Les séminaires précédents