Résumé de la Thèse
Modélisation et analyse temporelle par réseaux de
Petri et logique linéaire
L'objectif de cette thèse est de contribuer à
l'élaboration de méthodes
d'aide à la conception de systèmes coopératifs
en prenant en compte les
contraintes temporelles de manière quantitative. L'approche
développée
est fondée sur les réseaux de Petri, la logique
linéaire et les graphes
de contraintes temporelles. C'est une approche orientée «
événements »
et non orientée « états » comme c'est souvent le cas
dans les approches
fondées sur les réseaux de Petri. Elle est
décomposée en deux étapes :
une étape d'analyse « qualitative » et une étape
d'analyse «
quantitative ».
La première consiste à obtenir les relations de
causalité entre les
événements appartenant à un scénario
donné. L'équivalence entre un arbre
de preuve en logique linéaire et le processus fini obtenu par
dépliage
d'un réseau de Petri à partir du même marquage
initial montre que ces
relations sont des relations de précédence.
L'introduction de la notion
de séquent caractéristique permet de mettre en oeuvre
une approche
compositionnelle des processus à partir des règles du
calcul des
séquents.
La deuxième étape consiste à passer du graphe
décrivant les relations de
précédence à un graphe de contraintes
temporelles exprimant de façon
linéaire l'ensemble des contraintes temporelles quantitatives
que
doivent vérifier les dates des franchissements des
transitions dans un
scénario. Il devient ainsi possible d'exploiter tous les
résultats des
techniques classiques d'analyse et de propagation de contraintes.
Cette
démarche est complètement cohérente avec les
réseaux de Petri
p-temporels mais difficilement compatible avec les t-temporels car
ils
engendrent des ensembles de contraintes qui sont plus complexes.
Nous avons illustré cette démarche par un
problème simple
d'ordonnancement de documents multimédias.
Nous avons par la suite montré comment, pour les
réseaux de Petri
t-temporels, nous pouvions calculer les dates de franchissements et
les
durées de séjour des jetons dans les places en restant
sous une forme
symbolique dans le cadre de la sémantique faible.
Mots-Clés
Réseaux de Petri, logique linéaire, ordres partiels,
processus de réseaux de Petri, graphes de contraintes
temporelles
Thesis abstract
Modelling and temporal analysis by Petri nets and linear logic
The aim of this thesis is to contribute to the elaboration of design
assistance methods of cooperative systems while taking into account
temporal constraints in a quantitative way. The developed approach
is
based on Petri nets, linear logic and temporal constraints networks.
This is an "event" oriented approach and not a "state" oriented one
as
it is often the case in the approaches based on Petri nets. It is
split
in two steps: a step of "qualitative" analysis and a step of
"quantitative" one.
The first consists in obtaining the causality relations between the
events belonging to a given scenario. The equivalence between a
proof
tree in linear logic and the finite process obtained by the
unfolding of
a Petri net from the same initial marking shows that these relations
are
precedence relations. The introduction of the concept of
characteristic
sequent makes it possible to implement a compositional approach of
the
processes from the rules of the linear logic sequent calculus.
The second step consists in changing the graph describing the
precedence
relations into a temporal constraints graph expressing in a linear
way
the set of the quantitative temporal constraints which have to be
verified by the dates of the firing transitions in a scenario. Thus,
it
become possible to exploit all the results of traditional techniques
of
analysis and constraints propagation. This step is completely
consistent
with p-time Petri nets but not easily compatible with the t-timed
ones
because they generate sets of constraints which are more complex.
This
approach is illustrated by a simple scheduling problem of multimedia
documents.
We showed thereafter how, for the t-timed Petri nets, we could
process
the firing dates and the sojourn durations of the tokens in the
places
of a net while remaining in a symbolic form within the framework of
the
weak semantics.
Key words
Petri nets, linear logic, partial orders, Petri nets
processes, temporal constraints graphs
Thèse de
Nicolas Rivière
soutenue le mercredi 26 novembre 2003 devant le jury:
Président Michel Diaz Directeur de Recherche LAAS-CNRS
Rapporteurs
Jean-Pierre Elloy Professeur à l'École Centrale de Nantes
S. Haddad Professeur à l'Université Paris-Dauphine
Examinateurs:
Gilles Motet Professeur à l'INSA de Toulouse
François Vernadat Ma&icrirc;tre de Conférence à
l'INSA de Toulouse
Directeurs de thèse :
Brigitte Chézalviel-Pradin Maître de Conférence à
l'IUT A (Toulouse)
Robert Valette Directeur de recherche au LAAS-CNRS (Toulouse)
Cette thèse a été préparée au LAAS-CNRS
7, Avenue du Colonel Roche, 31077 Toulouse Cedex 4
Rapport LAAS Numéro