The expressive power of time Petri nets

B. Bérard, F. Cassez, S. Haddad, D. Lime*, O. H. Roux

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

33 Citations (Scopus)

Abstract

We investigate expressiveness questions for time Petri nets (TPNs) and some of their most useful 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 strictly 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 "à 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.

Original languageEnglish
Pages (from-to)1-20
Number of pages20
JournalTheoretical Computer Science
Volume474
DOIs
Publication statusPublished - 25 Feb 2013
Externally publishedYes

Keywords

  • Bisimilarity
  • Expressiveness
  • Language equivalence
  • Time Petri nets
  • Timed automata

Fingerprint

Dive into the research topics of 'The expressive power of time Petri nets'. Together they form a unique fingerprint.

Cite this