Comparison of Different Semantics for Time Petri Nets
Roux, Olivier-Henri; Lime, Didier; Haddad, Serge; Cassez, Franck; Bérard, Béatrice (2005), Comparison of Different Semantics for Time Petri Nets, dans Yih-Kuen, Tsay; Peled, Doron A., Automated Technology for Verification and Analysis. Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings, Springer : Berlin, p. 293-307. http://dx.doi.org/10.1007/11562948_23
Type
Communication / ConférenceLien vers un document non conservé dans cette base
http://hal.archives-ouvertes.fr/inria-00368580/fr/Date
2005Titre du colloque
Third International Symposium on Automated Technology for Verification and Analysis, ATVA 2005Date du colloque
2005-10Ville du colloque
TaipeiPays du colloque
TaïwanTitre de l'ouvrage
Automated Technology for Verification and Analysis. Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, ProceedingsAuteurs de l’ouvrage
Yih-Kuen, Tsay; Peled, Doron A.Éditeur
Springer
Titre de la collection
Lecture Notes in Computer ScienceNuméro dans la collection
3707Ville d’édition
Berlin
Isbn
978-3-540-29209-8
Nombre de pages
506Pages
293-307
Identifiant publication
Métadonnées
Afficher la notice complèteRésumé (EN)
In this paper we study the model of Time Petri Nets (TPNs) where a time interval is associated with the firing of a transition, but we extend it by considering general intervals rather than closed ones. A key feature of timed models is the memory policy, i.e. which timing informations are kept when a transition is fired. The original model selects an intermediate semantics where the transitions disabled after consuming the tokens, as well as the firing transition, are reinitialised. However this semantics is not appropriate for some applications. So we consider here two alternative semantics: the atomic and the persistent atomic ones. First we present relevant patterns of discrete event systems which show the interest of these semantics. Then we compare the expressiveness of the three semantics w.r.t. weak timed bisimilarity, establishing inclusion results in the general case. Furthermore we show that some inclusions are strict with unrestricted intervals even when nets are bounded. Then we focus on bounded TPNs with upper-closed intervals and we prove that the semantics are equivalent. Finally taking into account both the practical and the theoretical issues, we conclude that persistent atomic semantics should be preferred.Mots-clés
Time Petri Nets; Timed Bisimilarity; ExpressivenessPublications associées
Affichage des éléments liés par titre et auteur.
-
Roux, Olivier-Henri; Bérard, Béatrice; Cassez, Franck; Haddad, Serge; Lime, Didier (2005) Communication / Conférence
-
Roux, Olivier-Henri; Lime, Didier; Haddad, Serge; Cassez, Franck; Bérard, Béatrice (2005) Communication / Conférence
-
Zouari, Belhassen; Taghelit, Mohamed; Haddad, Serge (1993) Communication / Conférence
-
Bouyer, Patricia; Haddad, Serge; Reynier, Pierre-Alain (2006) Communication / Conférence
-
Haddad, Serge; Pradat-Peyre, Jean-François (2006) Article accepté pour publication ou publié