A Concurrency-Preserving Translation from Time Petri Nets to Networks of Timed Automata - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Formal Methods in System Design Année : 2012

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

Résumé

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.

Domaines

Autre [cs.OH]

Dates et versions

hal-00776605 , version 1 (15-01-2013)

Identifiants

Citer

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

Altmetric

Partager

Gmail Facebook X LinkedIn More