Structural translation from time Petri Nets to timed automata

Franck Cassez*, Olivier H. Roux

*Corresponding author for this work

Research output: Contribution to journalArticle

20 Citations (Scopus)

Abstract

In this paper, we consider Time Petri Nets (TPN) where time is associated with transitions. We give a formal semantics for TPNs in terms of Timed Transition Systems. Then, we propose a translation from TPNs to Timed Automata (TA) that preserves the behavioural semantics (timed bisimilarity) of the TPNs. For the theory of TPNs this result is two-fold: i) reachability problems and more generally TCTL model-checking are decidable for bounded TPNs; ii) allowing strict time constraints on transitions for TPNs preserves the results described in i). The practical applications of the translation are: i) one can specify a system using both TPNs and Timed Automata and a precise semantics is given to the composition; ii) one can use existing tools for analysing timed automata (like Kronos, Uppaal or Cmc) to analyse TPNs.

Original languageEnglish
Pages (from-to)145-160
Number of pages16
JournalElectronic Notes in Theoretical Computer Science
Volume128
Issue number6
DOIs
Publication statusPublished - 23 May 2005
Externally publishedYes

Keywords

  • Model-Checking
  • Time Petri Nets
  • Timed Automata

Fingerprint Dive into the research topics of 'Structural translation from time Petri Nets to timed automata'. Together they form a unique fingerprint.

  • Cite this