Sémantique concurrente symbolique des réseaux de Petri saufs et dépliages finis des réseaux temporels
Résumé
On considère des réseaux de Petri colorés, à contraintes linéaires et pouvant posséder des arcs de lecture. Sur cette classe, on définit une sémantique concurrente en termes de processus d'ordre partiel permettant de garder explicite l'indépendance entre des tirs de transitions. L'ensemble des processus peut être représenté en utilisant la notion de dépliage symbolique. Nous montrons alors comment les réseaux de Petri temporels peuvent être codés dans ce modèle à l'aide d'une transformation syntaxique préservant la concurrence. Cette transformation permet de définir la notion de dépliage de réseaux de Petri temporels et d'en donner une représentation par préfixe fini.