Sogbohossou, Médésu and Sogbohossou, Medesu and Vianou, Antoine and Gmati, Nabil and Badouel, Ericet al. - ε-TPN: definition of a Time Petri Net formalism simulating the behaviour of the timed grafcets

arima:5492 - Revue Africaine de la Recherche en Informatique et Mathématiques Appliquées, December 3, 2019, Volume 31 - 2019 - CARI 2018
ε-TPN: definition of a Time Petri Net formalism simulating the behaviour of the timed grafcets

Authors: Sogbohossou, Médésu and Sogbohossou, Medesu and Vianou, Antoine and Gmati, Nabil and Badouel, Eric and Watson, Bruce

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.


Source : oai:HAL:hal-02112963v3
Volume: Volume 31 - 2019 - CARI 2018
Published on: December 3, 2019
Submitted on: May 22, 2019
Keywords: Time Petri Net,timed grafcet,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,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,[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]


Share