Comparison of Different Semantics for Time Petri Nets

Béatrice Berard 1 Franck Cassez 2, 3 Serge Haddad 1, 4 Didier Lime 2 Olivier Henri Roux 2
1 LAMSADE - Laboratoire d'analyse et modélisation de systèmes pour l'aide à la décision
2 IRCCyN - Institut de Recherche en Communications et en Cybernétique de Nantes
3 NICTA - National ICT Australia [Sydney]
4 LSV - Laboratoire Spécification et Vérification [Cachan]
Abstract : 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 \emphintermediate 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 \emphatomic and the \emphpersistent 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. the weak time 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.
Type de document :
Communication dans un congrès
3rd Int. Symp. on Automated Technology for Verification and Analysis (ATVA'05), Oct 2005, Taiwan, Taiwan. Copyright \beginrawhtmlSpringer\endrawhtml, 3707, pp.293--307, 2005
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00368580
Contributeur : Franck Cassez <>
Soumis le : mardi 17 mars 2009 - 05:03:28
Dernière modification le : jeudi 15 mars 2018 - 14:28:03
Document(s) archivé(s) le : mardi 8 juin 2010 - 23:32:16

Fichier

petri-nets-atva05.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00368580, version 1

Collections

IRCCYN-MEFORBIO | UNIV-NANTES | IRCCYN | UNAM | ENS-CACHAN | PSL

Citation

Béatrice Berard, Franck Cassez, Serge Haddad, Didier Lime, Olivier Henri Roux. Comparison of Different Semantics for Time Petri Nets. 3rd Int. Symp. on Automated Technology for Verification and Analysis (ATVA'05), Oct 2005, Taiwan, Taiwan. Copyright \beginrawhtmlSpringer\endrawhtml, 3707, pp.293--307, 2005. 〈inria-00368580〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

326

Téléchargements de fichiers

158

Contact


archive-ouverte@inria.fr