Modélisation et analyse temporelle par réseaux de Petri et logique linéaire
Rivière, Nicolas · HAL (Le Centre pour la Communication Scientifique Directe) · 2003
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.