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

Sandie Balaguer 1 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 : 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.
Type de document :
Communication dans un congrès
Markey, Nicolas and Wijsen, Jef. Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME'10), Sep 2010, Paris, France, France. IEEE Computer Society Press, pp.77-84, 2010, 〈10.1109/TIME.2010.12〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00638283
Contributeur : Stefan Haar <>
Soumis le : vendredi 4 novembre 2011 - 14:41:59
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37

Lien texte intégral

Identifiants

Collections

Citation

Sandie Balaguer, Thomas Chatain, Stefan Haar. A~Concurrency-Preserving Translation from Time Petri Nets to Networks of Timed Automata. Markey, Nicolas and Wijsen, Jef. Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME'10), Sep 2010, Paris, France, France. IEEE Computer Society Press, pp.77-84, 2010, 〈10.1109/TIME.2010.12〉. 〈inria-00638283〉

Partager

Métriques

Consultations de la notice

166