ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne

APPEL À
CONTRIBUTION

Le comité de rédaction du JESA lance un appel à proposition de numéros spéciaux.

En savoir plus >>
Autres revues >>

Journal Européen des Systèmes Automatisés

1269-6935
Revues des Systèmes
 

 ARTICLE VOL 45/1-3 - 2011  - pp.13-28  - doi:10.3166/jesa.45.13-28
TITRE
Coercition temporelle de réseaux de Petri

RÉSUMÉ
Le problème de la synthèse de bornes temporelles assurant de bonnes propriétés dans les systèmes réactifs a été bien étudié dans la littérature. Ces travaux reposent principalement sur l’algèbre des dioïdes et imposent des restrictions importantes sur la structure du modèle. Nous nous intéressons dans cet article aux problèmes de l’existence et de la synthèse de l’ensemble des resserrements des bornes temporelles des intervalles d’un réseau de Petri temporel assurant la vérification d’une propriété donnée. Nous montrons que ce problème est décidable pour des propriétés CTL et pour des réseaux de Petri temporels bornés. Nous proposons alors un algorithme symbolique basé sur le graphe des classes d’état pour un fragment de CTL. Si la propriété que nous cherchons à vérifier « inclut » la kbornitude du réseau, notre algorithme termine même si le réseau est non borné. Un prototype a été implémenté dans notre outil Romeo.


ABSTRACT
The problem of the sythesis of time bounds enforcing good properties for reactive systems has been much studied in the literature. These works mainly rely on dioid algebra theory and require important restrictions on the structure of the model (notably by restricting to timed event graphs). In this paper, we address the problems of existence and synthesis of tightenings of the bounds of the time intervals of a time Petri net, such that a given property is verified. We show that this problem is decidable for CTL properties on bounded time Petri nets. We then propose a symbolic algorithm based on the state class graph for a fragment of CTL. If the desired property “includes” k-boundedness, the proposed algorithm terminates even if the net is unbounded. A prototype has been implemented in our tool Romeo.


AUTEUR(S)
Didier LIME, Claude MARTINEZ, Olivier Henri ROUX

MOTS-CLÉS
réseaux de Petri temporels, resserrement d’intervalles temporels, modelchecking, graphes des classes d’états.

KEYWORDS
time Petri nets, time interval tightening, model-checking, state-class graph.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 7.5 €
• Non abonné : 15.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (247 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier