Réduction par symétrie du graphe des classes d'états des Réseaux de Petri Temporels

Pierre-Alain Bourdil (1) , Bernard Berthomieu (1) , Silvano Dal Zilio (1) , François Vernadat

1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques

Nous proposons une méthode d'exploitation des symétries pour la vérification par model-checking des systèmes temps réel modélisés par réseaux de Petri temporels. La méthode traite les marquages ainsi que les contraintes temporelles; elle est applicable aux graphes de classes d'états. Nous présentons une implémentation dans TINA ainsi que quelques résultats expérimentaux.

Domaines: Systèmes embarqués; Logique en informatique [cs.LO]

Pierre-Alain Bourdil, Bernard Berthomieu, Silvano Dal Zilio, François Vernadat. Réduction par symétrie du graphe des classes d'états des Réseaux de Petri Temporels. Rapport LAAS n° 14405. Formalisation des activités concurrentes 2014. 2014. ⟨hal-01949504⟩