Médésu Sogbohossou ; Antoine Vianou - ε-TPN: definition of a Time Petri Net formalism simulating the behaviour of the timed grafcets

arima:5492 - Revue Africaine de Recherche en Informatique et Mathématiques Appliquées, 3 décembre 2019, Volume 31 - 2019 - CARI 2018 - https://doi.org/10.46298/arima.5492
ε-TPN: definition of a Time Petri Net formalism simulating the behaviour of the timed grafcetsArticle

Auteurs : Médésu Sogbohossou 1; Medesu Sogbohossou 1; Antoine Vianou 1; Nabil Gmati ; Eric Badouel ; Bruce Watson

  • 1 Laboratoire d'Electrotechnique, de Télécommunication et d'Informatique Appliquée

[en]
To allow a formal verification of timed GRAFCET models, many authors proposed to translate them into formal and well-reputed languages such as timed automata or Time Petri nets (TPN). Thus, the work presented in [Sogbohossou, Vianou, Formal modeling of grafcets with Time Petri nets, IEEE Transactions on Control Systems Technology, 23(5)(2015)] concerns the TPN formalism: the resulting TPN of the translation, called here ε-TPN, integrates some infinitesimal delays (ε) to simulate the synchronous semantics of the grafcet. The first goal of this paper is to specify a formal operational semantics for an ε-TPN to amend the previous one: especially, priority is introduced here between two defined categories of the ε-TPN transitions, in order to respect strictly the synchronous hypothesis. The second goal is to provide how to build the finite state space abstraction resulting from the new definitions.

[fr]
Afin de permettre la vérification formelle des grafcets temporisés, plusieurs auteurs ont proposé de les traduire dans des langages formels de réputation tels que les automates temporisés et les réseaux de Petri temporels (TPN). Ainsi, les travaux présentés dans [Sogbohossou, Vianou, Formal modeling of grafcets with Time Petri nets, IEEE Transactions on Control Systems Technology, 23(5)(2015)] concernent le formalisme des TPN: le réseau résultant de la traduction, dénommé ici ε-TPN, intègre des délais infinitésimaux (ε) pour simuler la sémantique synchrone du grafcet. Le premier objectif de cet article est de définir la sémantique opérationnelle d'un ε-TPN afin d'améliorer l'ancienne définition: spécifiquement, une priorité est introduite ici entre deux catégories de transitions définies pour ces réseaux, dans l'optique de respecter rigoureusement l'hypothèse synchrone. Le second but est de fournir une méthode de calcul de l'espace d'état fini qui découle des nouvelles définitions.


Volume : Volume 31 - 2019 - CARI 2018
Publié le : 3 décembre 2019
Accepté le : 3 décembre 2019
Soumis le : 22 mai 2019
Mots-clés : [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], [INFO.INFO-SY]Computer Science [cs]/Systems and Control [cs.SY], [en] state class, partial order execution, synchronous modelling, synchronous mod- elling MOTS-CLÉS : Réseau de Petri temporel, grafcet temporisé, classe d'état, exécution ordre partiel, modélisation synchrone, Time Petri Net, timed grafcet; [fr] Réseau de Petri temporel, classe d’état, Time Petri Net, timed grafcet, state class, partial order execution, synchronous mod- elling MOTS-CLÉS : Réseau de Petri temporel, grafcet temporisé, classe d'état, exécution ordre partiel, modélisation synchrone

Statistiques de consultation

Cette page a été consultée 696 fois.
Le PDF de cet article a été téléchargé 830 fois.