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], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
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.
Type de document :
Article dans une revue
Formal Methods in System Design, Springer Verlag, 2012, 40 (3), pp.330-355. 〈10.1007/s10703-012-0146-4〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00776605
Contributeur : Benedikt Bollig <>
Soumis le : mardi 15 janvier 2013 - 17:46:01
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37

Identifiants

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

286