Skip to main content

TS

The expressive power of time petri nets

Authors

Beatrice Berard, Franck Cassez, Serge Haddad, Didier Lime and Olivier H. Roux

aUniversit ́e Pierre et Marie Curie
LIP6
Paris
France

NICTA

LSV
ENS Cachan

IRCCyN

Abstract

In this paper, we investigate different questions related to the expressiveness of time Petri nets (TPNs) and some their most usefull extensions. We first introduce generalised time Petri nets (GTPNs) as an abstract model that encompasses variants of TPNs such as self modifications and read, reset and inhibitor arcs. We give a syntactical translation from bounded GTPNs to timed automata (TA) that generates isomorphic transition systems. We prove that the class of bounded GTPNs is stricly less expressive than TA w.r.t. weak timed bisimilarity. We prove that bounded GTPNs, bounded TPNs and TA are equally expressive w.r.t. timed language acceptance. Finally, we characterise a syntactical subclass of TA that is equally expressive to bounded GTPNs “a` la Merlin” w.r.t. weak timed bisimilarity. These results provide a unified comparison of the expressiveness of many variants of timed models often used in practice. It leads to new important results for TPNs. Among them are: 1-safe TPNs and bounded-TPNs are equally expressive; ε-transitions strictly increase the expressive power of TPNs; self modifying nets as well as read, inhibitor and reset arcs do not add expressiveness to bounded TPNs.

BibTeX Entry

  @article{Berard_CHLR_13,
    doi              = {10.1016/j.tcs.2012.12.005},
    journal          = {Theoretical Computer Science},
    author           = {Berard, Beatrice and Cassez, Franck and Haddad, Serge and Lime, Didier and Roux, Olivier H.},
    number           = {N/A},
    month            = mar,
    volume           = {474},
    year             = {2013},
    keywords         = {time petri nets, timed automata, expressiveness, language equivalence, bisimilarity},
    title            = {The Expressive Power of Time Petri Nets},
    pages            = {1--20}
  }

Download

Served by Apache on Linux on seL4.