Skip to Main content Skip to Navigation

A Concurrency-Preserving Translation from Time Petri Nets to Networks of Timed Automata

Sandie Balaguer 1, 2, * Thomas Chatain 2, 1 Stefan Haar 2, 1 
* Corresponding author
1 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
Abstract : Real-time distributed systems may be modeled in different formalisms such as time Petri nets (TPN) and networks of timed automata (NTA). This paper focuses on translating a 1-bounded TPN into an NTA and considers an equivalence which takes the distribution of actions into account. This translation is extensible to bounded TPNs. We first use S-invariants to decompose the net into components that give the structure of the automata, then we add clocks to provide the timing information. Although we have to use an extended syntax in the timed automata, this is a novel approach since the other transformations and comparisons of these models did not consider the preservation of concurrency.
Document type :
Complete list of metadata

Cited literature [2 references]  Display  Hide  Download
Contributor : Sandie Balaguer Connect in order to contact the contributor
Submitted on : Monday, July 19, 2010 - 10:03:26 PM
Last modification on : Wednesday, February 2, 2022 - 3:51:14 PM
Long-term archiving on: : Tuesday, October 23, 2012 - 10:40:58 AM


Files produced by the author(s)


  • HAL Id : inria-00504058, version 1


Sandie Balaguer, Thomas Chatain, Stefan Haar. A Concurrency-Preserving Translation from Time Petri Nets to Networks of Timed Automata. [Research Report] RR-7338, INRIA. 2010, pp.22. ⟨inria-00504058⟩



Record views


Files downloads