. Avec-le-même-raisonnement, une c<lnditi<ln suffisante pour que le verr<lu minimal {pl,p2, p7} ne soit pas mortel esr : MS,O-M r, p.14

. Il-faut-noter-que, pour Lrn RdP N donné, il est p<lssible c1u'avec la méthode décrite ci-dessus, nous ne trouvons aucun marquage initial M6 tel que <N, Mg> soit sans blocage

. La-figure-5, Le verrou minimal 1.p1,p2, p4] est lui même une trappe et le verrou minimal [p1, p3, p4] ne contient pas de trappe. Supposons que M1+MI*M4=Q, alors l'équation fondamentale du réseau N s'écrit : Considérons chaque transition d'entrée tl, et nous distinguons deux cas vo(tfi) = vo(tli) et vo, pp.4-7

S. Vo, =Vo(tl), d'après la relation (5.11), le chemin Of reliant tl; et tii n'esr pas marqué par M, Nous ajoutons les places de Oi dans P', i

S. Vo, nous avons Vo(tft;<V, ce qui signifie que tf;e f. ti; n'esr pas franchissable d'après l'hypothèse <H5>. Selon l'étape 1), il existe une place de ressource r' tel que M(r') = 0 et un chemin c{tfi) reliant r' à tf; ael qn'aucune place de C(ti;) n'est marquée par M et que les places autres que r

+. Si-tl1 and . Tf, = t[,i. Par conséquenr, nous avons la relation 'P'cP''. Autrement dit, P'est un verrou. En plus, aucune place iie P'n'est marquée par M, donc P' est un verrou mortel

. De-plus, . Mxr, . >o, and . Vre, En conclusion, I'idée de départ cle ce travail (vérification incrémentale) est originale et correspond aussi à la réalité industrielle. Nous pensons que les résultats sont suffisamment généraux pour être appliqués à d'autre domaines que le domairre de la production. Nous sommes confiants dans I'avenir de cette direction de recherche, puisque son imponance se situe non seulement dans I'aspect théorique, mais aussi et surtout dans ses applications pratiques

. All, Spécificatoin et commande des ateliers fleibles -Utilisation des réseaux de Petri colorés", extrait de "fae point en ProductiqueModelling and validation of complex systems by coloured Petri nets; application to a flexible manufacturing system, LNCS, vol.l, pp.15-31

. Ban, Deadlock avoidance inflexible manufacturing systems with concurrently compeling process flows, IEEE Trans. on Robotices and Automation, vol.6, issue.6, pp.724-734

. Bar, An effective chnracterization of minimal deadlocks and traps in Petri nets based on graph theory, Proc. of lOth Petri Net Conference on Theory and Applications of Petri Nets

I. , K. Barkaoui, and M. Minoux, A polynomial-time graph algorithm to decide Iiveness of some basic classes of bounded Petri nets, LNCS, issue.616, pp.62-74

. Bar, An fficient deadlock avoidance control policy in FMS using structural analysis of Petri nets, IEEE Inter. Conf. on Systems, Man, and Cybernetics, pp.525-530

I. and ]. G. Berthelot, Transformation et analyse des réseaux de Petri, Thèse d'Etat

I. and ]. G. Berthelot, Checking properties of nets using transformntion, Advance in Petri Nets 1985, pp.19-40

I. and ]. E. Best, Srructural theory of Petri nets : the free choice hiatus, LNCS, vol.254, pp.68-206

. Bes, Characterization of home states infree choice systems, p.7190

. Bou, Conception structurée et modulaire d'architectures de contrôle réparti en production flexible manufacturingRéseaux de Petri : thé.oric et pratiquc, APII, vol.25, pp.349-376

. Cam, Properties and pe rJormance bounds for closedfree choice synchronized monocla.ss qtteueing netwrtrks, IEEE Tran:;. on Automatic Control, vol.36, issue.72, pp.1368-1382

. Chu, Planning and Scheduling of Discrete Manufacturing Systems: a Petri Net Based Framework, 10th International Sympposium on Applications of Systems Theory, pp.277-295

I. , C. B. Chu, F. Chu, J. M. Proth, and X. L. Xie, Vérification incrémentale de la conststance d'un réseau de Petri, Accepté pour publication dans TSI

. Chu, Conceptictn des systènrcs ci événement discrèts à I'aide des réseauxde Petri: lapropriété de bornitttde struuurelle

. Chu, Siphon and trap generation in an incremental design process based on Petri nets, Conférence ETFA '95

. P. Chretienne, Les réseaux de Petri temporisés

. Cof, Sysrems deadlocÈs, Computing Surveys, vol.3, issue.2, pp.67-78

. Col, Convex geometry and semiflows in PIT nets, Advances in Petri Nets '90, pp.79-112

. Col, lmproving the linearly based characterization of PIT nets, Advances in Petri Nets '90, pp.113-145

I. Commoner, A. Holt, S. Even, and A. Pnueli, Marked directed graphs, Journal of Computer and System Sciences, vol.5, issue.5, pp.51-523
DOI : 10.1016/S0022-0000(71)80013-2

URL : https://doi.org/10.1016/s0022-0000(71)80013-2

I. and ]. F. Commoner, Deadlocks in Petri nets

I. Cruette, J. P. Bourey, and J. C. Jentina, Hierarchical specffication and ualidation of operating sequences in the context of FMS, Computer Intergrated Manufacturing Systems, vol.4, issue.3

. Dav, Du grafcet aux réseaux de Petri

. Dav, Peri nets for modeling of dynamic systemt -s syrysy, Automatica, vol.30, issue.2, pp.175-202

. Des, Applicattons of Petri nets in manufacturing systems

. Dic, Prectice of Petri ncts inmanufactwing

. Esp, On the analysis and synthesis of free choice systems, Advance in Petri Nets '90, pp.243-286

. Esp, Top-down synthesis of live and bounded free-choice systems, Proc. of 1 lth lnternational Conference on Applications and Theory of Petri Nets, pp.63-86

. Esp, Synthesis of live models fttr a class of F MS, Proc.od the 1993 IEEE InternationalConference on Robotics and Automation, pp.557-563

. Gen, Colowed adaptive structured Petri net : A tool for the Automatic synthesis of Hierarchical control of flexible manufacturing systems, Proceedings of the IEEE International Conference on Robotics and Automation, pp.1166-1173

. Gha, Controlled continous Petri nets, IEEE International Conference on Robotics and Automation, vol.1, pp.788-793

. Hil, Performance evaluation to job-sh.op systems using timed event grapgs, IEEE trans. on Automatic Control, vol.34, issue.l, pp.3-9

I. and ]. H. Hillion, Modélisation et analyse des systèmes de production discrets par les réseaux de Petri temporisés

U. , M. Jantzen, and R. Valk, Formal properties of place transition nets, LNCS, vol.84

A. Kaufmann, Méthodes et modèles de Ia recherche opérationnelle -I(Les mat hémathiques de l' e ntrep r iseGencrating siphons and traps by Petri net representation of logic equations, Procs. 2nd Conf, pp.93-100

. Koh, Transformation methods for generalized Petri nets and their applications to flexible manufacturing system.i, Proc. of the 2th Int. Conf. on CIM, pp.364-371

I. and ]. K. Lautenbach, Linear algebraic calculation of deadlocks and taps", irr Coucurency and Nets -Advances in Petri Nets, pp.315-336

I. and ]. K. Lautenbach, Linear algebraic techniques for placeltransitions nets, Net Theory and Application LNCS, issue.254, pp.142-167

. Lee, Hierarchical reduction method for analysis and decomposition of Petri nets, IEEE Transactions on Systems, Man, and Cybernetics, vol.15, issue.2, pp.272-281
DOI : 10.1109/TSMC.1985.6313357

I. and ]. D. Luenberger, lntroduction to linear and nonlinear programnting

I. , ]. J. Martinez, and M. Silva, A simple and fast algorithm ro obtain all invariants of a generalized Petri net, Second European Workshop on Application and Theory of Petri Nets, pp.4-422

I. and ]. M. Mehta, Matrix theory (Selected topics and useful results)

. Mem, Linear algebra in net theory, LNCS, vol.84, pp.213-223
DOI : 10.1007/3-540-10001-6_24

. Min, polynomial algorithms for finding deadlocks, traps and other substructures relevant to Petri net analysis, lnternal research report N" 212 of the Laboratoire MASI

I. and ]. M. Molloy, Performance Analysis Using Stochastic Petri Nets, IEEE Transactions on Computers, vol.31, issue.9, pp.913-917
DOI : 10.1109/TC.1982.1676110

I. and ]. M. Molloy, Discrete Time Stochastic Petri Nets, IEEE Transactions on Software Engineering, vol.11, issue.4, pp.417-423
DOI : 10.1109/TSE.1985.232230

. Mu, A synthesis method for Petri Net Modeling of automated manufacturing systems with shared resources, Proc. of the 31st Conf. on Decision and Control, p.1

I. 7. Murata, Circuit theoretic analysis and synthesis of marked graphs, IEEE Transactions on Circuits and Systems, vol.24, issue.7, pp.400-405
DOI : 10.1109/TCS.1977.1084357

I. , T. Murata, N. Komoda, and K. Matsumoto, A Petri net based controllerfor flexible and maintainablc sequence control and its ttpplications in.factnry automation, IEEE Trans. Ind. Electron, pp.33-34

. Mur, Detection of Ada static deadlocks using Petri net invariafis, IEEE Trans. on Software Engineering, vol.15, issue.3, pp.3-4

. Nar, A Peti net approach to the modelling and analysis of flexible manufacturing systems, Annals of Operations Research, vol.3, pp.449-472

H. Ohl, E. Castelain, and J. C. Gentina, State dependent release control in flexible manufacturing systems, Proceedings of IEEE Systems Man and Cybernetics Conference, SMC, pp.295-300
DOI : 10.1109/ICSMC.1993.384760

I. and J. L. Peterson, Petri net theory and the modelling of systems

. Ipro, A demand-to-mnnufacturing-requirement model based on predefined Configurations, European Journal of Operation Research, vol.53, issue.3, pp.297-308

]. J. Ipro-92 and . Proth, Conception et gestion des systèmes de production

. Pro, A class oJ'Petri nets Jbr manufacturing rystèm integration

J. M. Pro, X. L. Proth, and . Xie, Les réseaux de Petri pour Ia conception et Ia gestion des systèmes de production

I. and ]. C. Ramchandani, Analysis of asynchronous courrent systems by timed Petri nets

I. and ]. W. Reisig, Peti nets

]. J. Sif-87 and . Sifakis, Structural properties of Petri nets, Mathematical Foundations of Computers Science LNCS, issue.64

. Sil, Generalized inverses and the calculation of symbolic invariants for coloured Petri nets, pp.113-126

. Sil, On the computation of structural synchronic invariants inPlT nets, Advances in Petri Nets '88, pp.386-417

. Sil, Peri nets andflexible manufacturing, Advance in Petri Nets 1989, pp.374-417

Y. Souissi, On liveness preservation by composition of nets via a set of places, p.66
DOI : 10.1007/BFb0019979

. Suz, A mcthotlJ'or ste.pwise reJinement and abstraction of Petri nets, Joumal of Computer and Systems Sciences, vol.27, pp.5-76

. Ter, Liveness and home states in equ.al conflit systems",ln Applications and Theory of Petri Nets, LNCS, pp.415-432, 1993.

I. and ]. J. Toudic, Algorithme d'analyse structurelle des réseaux de Petri, Thèse de 3ème Cycle

I. and ]. R. Valette, Analysis of petri nets by stepwise refinements, Journal of Computer and System Sciences, vol.18, issue.1, pp.35-46
DOI : 10.1016/0022-0000(79)90050-3

. Vis, Deadlock prevention and deadlock avoidance in flexible manufacturing systems using Petri net models, IEEE Trans on Robotics and Automation, vol.6, issue.6, pp.713-723

R. A. Wys, N. S. Wysk, S. Yang, and . Joshi, Detection of deadlocks in flexible manufacturing cells, IEEE trans. on Robotics and Automation, vol.7, issue.6, pp.853-859

. L. Xie-91-]-x and . Xie, Hierarchical production control of aflexible manufacturing system Applied Stochastic Models and Data Analysis, pp.343-360

I. and ]. X. Xie, On thc impact ofrundomness irt prcduction lines contntlled by kanbans, Proc. of the 2nd European Control Conference (ECC'93), pp.5-163

I. and X. L. Xie, Performance analysis of a transfer line with unreliable mnchines andfinite buffers, IIE Transactions, vol.1, issue.25, pp.99-108

. Izjjo, A top-down modular approach to synthesis of Petri net models for manufacturing systetns, Proc. of IEEE Robotics and Automation Conf, pp.534-539

. Izho, Adaptive design of Petri net controllers for error recovery in automated manufacturing systems, IEEE Trans. on Syst. Man : Cybemetics, vol.19, issue.5, pp.963-973

. Îzjjo, ParalLel and sequential mutual exclusionfor Petri net modeling of Manufacturing systeltrs with shared resources, IEEE Transaction on Robotics and Automation, vol.7, issue.4, pp.515-527

. Izjjo, A hybrid methodology for synthesis of Petri net models for manufacturing s),stems, IEEE Trans. on Robotics and Automation, vol.8, issue.3, pp.350-361

. Résumé, Dans ce travail, nous nous intéressons à la conception des systèmes de production à I'aide des réseaux de Petri (RdP). L'objectif est de vérifier les propriétés qualitatives dans un processus de conception incrémentale

. Le-bon-fonctionnement, Cela exige que le modèle réseaux de Petri possède de bonnes propriétés qualitatives : la consistance, la conservation, la bornitude structurelle, la répétitivité, I'absence de blocage, vivacité, etc. Nous considérons le processus de conception incrémentale dans lequel la conception se fait étape par étape , ce qui correspond à la réalité industrielle Chaque étape consiste à ajouter des transitions eVou des places à un modèle existant, ou à intégrer des modèles exislants par fusion de places etlou de transitions. Nous nous plaçons dans I'optique d'un ingénieur qui conçoit un modèle et qui souhaite savoir, à chaque étape de la conception, si son modèle conserve ou non les propriétés requises. Les résultats rassemblés dans cette thèse fournissent une base theorique pour le développement. d'un outil qui va dans ce sens. Grâce aux nouveaux résultats théoriques que nous tlévcloppons, la véril'ication des propriétés du rnodèle peut être efïectuée en n, nous établissons des conditions nécessaires etlou suffisantes pour préserver la consistance, la conservation, la bornitude structurelle ou la répétitivité

. Abstract, An efficient behavior of un system needs an appropriate design. Thus, the Petri net model of the system should possess desirable qualitative properties, namely : consistency, conservativeness, structural boundedness, repetitiviness, deadlock-freeness and liveness, and so on We consider a step by step design process which coresponds to a real life situation. The action taken at each st-op consists ol adding placcs and/or transilions to an cxisting modcl, or ol'inLcgrating scvcral cxisting models by mcrging placcs and/or ransitions Wc cxaminc thc problcm frorn the point ol' view of an engineer who designs a model and who v/ants to know, at each step of the design process, if his model preserves the required properties. The results presented in this thesis provide a theoretical basis for the development of a tool devoted to this kind of tests. The theoretical results presented in this work allow to perform these checkings by only considering a part of the whole modcl. Using linear algebraic methods, we propose necessary and/or sufficient conditions to preserve consistency, conservativeness, structural boundedness and repetitiviness. Deadlock-freeness and liveness are checked using siphons and traps. We prove theorems that give the evolution of the siphon and trap bases from step to step in the design process, this work These results allow to develop algorithms to find out the siphon and trap bases. We define thc notion o[ fatal siphon liom which wc establish necessary andlor sufficient conditions for the deadlock-frceness of any ordinary Petri nets and thc liveness of asymmetric nets and event graphs with shared resource places. We show that the absencc ol tatal siphons can be checked out by a linear program

. Keywords, Manufacturing systems, Petri nets, Design, Qualitative properties