Skip to Main content Skip to Navigation
Journal articles

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

Sandie Balaguer 1, 2 Thomas Chatain 1, 2 Stefan Haar 1, 2
2 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
Abstract : Several formalisms to model distributed real-time systems coexist in the literature. This naturally induces a need to compare their expressiveness and to translate models from one formalism to another when possible. The first formal comparisons of the expressiveness of these models focused on the preservation of the sequential behavior of the models, using notions like timed language equivalence or timed bisimilarity. They do not consider preservation of concurrency. In this paper we define timed traces as a partial order representation of executions of our models for real-time distributed systems. Timed traces provide an alternative to timed words, and take the distribution of actions into account. We propose a translation between two popular formalisms that describe timed concurrent systems: 1-bounded time Petri nets (TPN) and networks of timed automata (NTA). Our translation preserves the distribution of actions, that is we require that if the TPN represents the product of several components (called processes), then each process should have its counterpart as one timed automaton in the resulting NTA.
Document type :
Journal articles
Complete list of metadata
Contributor : Benedikt Bollig <>
Submitted on : Tuesday, January 15, 2013 - 5:46:01 PM
Last modification on : Monday, April 26, 2021 - 4:24:01 PM

Links full text



Sandie Balaguer, Thomas Chatain, Stefan Haar. A Concurrency-Preserving Translation from Time Petri Nets to Networks of Timed Automata. Formal Methods in System Design, Springer Verlag, 2012, 40 (3), pp.330-355. ⟨10.1007/s10703-012-0146-4⟩. ⟨hal-00776605⟩



Record views