• xmlui.mirage2.page-structure.header.title
    • français
    • English
  • Help
  • Login
  • Language 
    • Français
    • English
View Item 
  •   BIRD Home
  • LAMSADE (UMR CNRS 7243)
  • LAMSADE : Publications
  • View Item
  •   BIRD Home
  • LAMSADE (UMR CNRS 7243)
  • LAMSADE : Publications
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

Browse

BIRDResearch centres & CollectionsBy Issue DateAuthorsTitlesTypeThis CollectionBy Issue DateAuthorsTitlesType

My Account

LoginRegister

Statistics

Most Popular ItemsStatistics by CountryMost Popular Authors
Thumbnail - No thumbnail

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, in 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érence
External document link
http://hal.archives-ouvertes.fr/inria-00368580/fr/
Date
2005
Conference title
Third International Symposium on Automated Technology for Verification and Analysis, ATVA 2005
Conference date
2005-10
Conference city
Taipei
Conference country
Taïwan
Book title
Automated Technology for Verification and Analysis. Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings
Book author
Yih-Kuen, Tsay; Peled, Doron A.
Publisher
Springer
Series title
Lecture Notes in Computer Science
Series number
3707
Published in
Berlin
ISBN
978-3-540-29209-8
Number of pages
506
Pages
293-307
Publication identifier
http://dx.doi.org/10.1007/11562948_23
Metadata
Show full item record
Author(s)
Roux, Olivier-Henri
Lime, Didier
Haddad, Serge
Cassez, Franck
Bérard, Béatrice
Abstract (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.
Subjects / Keywords
Time Petri Nets; Timed Bisimilarity; Expressiveness

Related items

Showing items related by title and author.

  • Thumbnail
    Comparison of the Expressiveness of Timed Automata and Time Petri Nets 
    Roux, Olivier-Henri; Bérard, Béatrice; Cassez, Franck; Haddad, Serge; Lime, Didier (2005) Communication / Conférence
  • Thumbnail
    When are Timed Automata Weakly Timed Bisimilar to Time Petri Nets? 
    Roux, Olivier-Henri; Lime, Didier; Haddad, Serge; Cassez, Franck; Bérard, Béatrice (2005) Communication / Conférence
  • Thumbnail
    A Protocol Specification Language with a High-level Petri Net Semantics 
    Zouari, Belhassen; Taghelit, Mohamed; Haddad, Serge (1993) Communication / Conférence
  • Thumbnail
    Extended Timed Automata and Time Petri Nets 
    Bouyer, Patricia; Haddad, Serge; Reynier, Pierre-Alain (2006) Communication / Conférence
  • Thumbnail
    New Efficient Petri Net Reductions for Parallel Programs Verification 
    Haddad, Serge; Pradat-Peyre, Jean-François (2006) Article accepté pour publication ou publié
Dauphine PSL Bibliothèque logo
Place du Maréchal de Lattre de Tassigny 75775 Paris Cedex 16
Phone: 01 44 05 40 94
Contact
Dauphine PSL logoEQUIS logoCreative Commons logo