A Concurrency-Preserving Translation from Time Petri Nets to Networks of Timed Automata
Résumé
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.
Les systèmes temporisés distribués peuvent être modélisés dans différents formalismes comme les réseaux de Petri temporels ou les réseaux d'automates temporisés. Cet article s'intéresse à la traduction d'un réseau de Petri temporel 1-borné vers un réseau d'automates temporisés et considère une équivalence qui tient compte de la distribution des actions. Cette traduction peut s'étendre aux réseaux de Petri temporels bornés. Nous utilisons d'abord les S-invariants pour décomposer le réseau en composants qui donnent directement la structure des automates, puis nous rajoutons des horloges pour retranscrire l'information temporelle. Bien que l'utilisation d'une syntaxe étendue dans les automates temporisés soit nécessaire, ce travail est une approche originale puisque les autres transformations et comparaisons de ces modèles ne considèrent pas la concurrence.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...