scieee AI-readable full text Open interactive document viewer

Deadlock Analysis, Prevention and Avoidance in Sequential Resource Allocation Systems

Abstract

El propósito de este trabajo es generalizar y extender los resultados existentes en el análisis, prevención y evitación de bloqueos en sistemas de asignación de recursos, con una atención especial hacia los sistemas de fabricación flexible. En este sentido, se proponen nuevas clases de sistemas con restricciones similares a las que podemos encontrar dentro del ámbito de los sistemas de fabricación. En un primer paso se estudiarán las propiedades estructurales de estas clases para comprobar que son adecuadas para el modelado y análisis del tipo de problemas considerado. Las soluciones al problema de los bloqueos se presentarán desde dos puntos de vista: prevención y evitación de los problemas de bloqueo, junto con algunos datos comparativos con otras soluciones al problema. El objetivo es obtener políticas de control muy permisivas, que puedan implantarse según diferentes consideraciones, proporcionando flexibilidad al diseñador del sistema. Finalmente se propone una mejora de un método de cálculo de cerrojos. Estas componentes estructurales están ligadas a la existencia de problemas de bloqueo en algunas clases de sistemas, y en ese sentido es muy conveniente disponer de métodos eficientes para su cálculo. El método propuesto mejora a los existentes mediante la utilización de paralelismo, y la adaptación a las características de los sistemas considerados. ------- This work concentrates on deadlock problems in concurrent systems due to the common use of system resources organized in what is commonly known as Sequential Resource Allocation Systems and paying a special attention to subclasses of manufacturing systems. To do that, special classes of Petri net models are defined that allow to capture resource allocation events used to synchronize processes that have to share a set of reusable system resources. The classes of Petri nets introduced are studied from the structure point of view, showing the clear mapping among system and model structures. It is also shown how deadlock related situations can be explained in terms of markings and model structures. To solve deadlock problems, two different approaches are adopted. The first one is known as a deadlock prevention perspective, and makes an intensive use of different liveness characterizations developed in this work. The final result is a deadlock prevention algorithm that iteratively constrains the language of the input model so that the final controlled model is live in terms of Petri net definitions, which implies that the controlled system is free of deadlocks and ensures that the execution of any active process can terminate. The second approach falls into the deadlock avoidance family of solutions. In this work it is shown how the specific characteristics of the class of systems in consideration can be used to extend and improve the well-known Banker's solution for deadlock avoidance, allowing us to give a solution to deadlock problems in the most general class of sequential resource allocation systems. In both cases, and taking into account that obtaining the most permissive solution is NP-complete, the proposed solutions are experimentally compared with other solutions in order to get insight of how permissive the proposed algorithms are, showing they provide a good trade-off between computation cost and permissiveness. Tricas García, Fernando; Ezpeleta Mateo, Joaquín

Full text

An´ alisis, prevenci´ on y evitaci´ on de bloqueos en sistemas secuenciales de asignaci´ on de recursos Fernando Tricas Garc´ıa TESIS DOCTORAL Departamento de Inform´atica e Ingenier´ıa de Sistemas Universidad de Zaragoza Febrero 2003 A Alicia, gracias. Para Carmen y Juan. Agradecimientos Mi agradecimiento al director de esta tesis, Joaqu´ın Ezpeleta, que me di´o la ayuda necesaria para progresar en este trabajo. Este agradecimiento ha de ser forzosamente extendido a Jos´e Manuel Colom y Fernando Garc´ıa Vall´es, cuya ayuda ha sido decisiva. Tambi´en le corresponde una parte del agradecimiento a Javier Mart´ınez, que me introdujo en mis primeros pasos en este trabajo. Tambi´en quiero agradecer a todos los miembros del Departamento de Inform´atica e Ingenier´ıa de Sistemas de la Universidad de Zaragoza, en particular a la gente del grupo de m´etodos formales, por su pronta disposici´on a echar una mano cuando ha hecho falta. Especial menci´on merece el personal de administraci´on y servicios encargado de los equipos inform´aticos del departamento, en particular Jos´e Antonio Gutierrez Elipe, siempre dispuesto a buscarle las vueltas a cualquier problema con los computadores y a solucionar los problemas que han ido apareciendo. El trabajo desarrollado en esta tesis ha sido apoyado financieramente por una beca de la D.G.A. y la participaci´on en los proyectos TIC91-0354, TIC95-0614C03-01, TAP98-0679, TIC2001-1819, y la acci´on integrada Hispano-Germana, HA2000-0047, financiados por la C.I.C.Y.T,PLAN NACIONALDE I+D.Tambi´en se recibi´o financiaci´on a trav´es del proyecto CHRX - CT94 - 0452 de la CEE Tengo que expresar agradecimiento infinito a mi familia: por la paciencia y por su apoyo incondicional. No creo que me sea posible devolverles la deuda acumulada durante estos a˜nos, pero prometo intentar compensarles a partir de ahora. Finalmente tengo que expresar mi profundo agradecimiento y admiraci´on a los desarrolladores del sistema GNU/Linux y los m´ultiples programas de este entorno que han ayudado a que el trabajo con las m´aquinas haya sido menos duro. A Enrique Teruel, Salvador Sans Rica, Alberto Tappe Mart´ınez, y Germ´an Lozano Fern´andez por la parte que les corresponde a cada uno de ellos en el desarrollo de HARP y herramientas relacionadas. A Giovanni Chiola y otros investigadores de la Universidad de Tur´ın, autores del programa GreatSPN, utilizado para dibujar muchas de las redes que aparecen en este trabajo. A los desarrolladores de la Op- vi timization Subroutine Library de IBM, que ha sido utilizada para la resoluci´on de los problemas de programaci´on entera del cap´ıtulo 3. Finalmente, a los desarrolladores de daVinci, cuya herramienta ha sido empleada para dibujar algunos de los grafos del cap´ıtulo 4. Resumen El prop´osito de este trabajo es generalizar y extender los resultados existentes en el an´alisis, prevenci´on y evitaci´on de bloqueos en sistemas de asignaci´on de recursos, con una atenci´on especial hacia los sistemas de fabricaci´on flexible. En este sentido, se proponen nuevas clases de sistemas con restricciones similares a las que podemos encontrar dentro del ´ambito de los sistemas de fabricaci´on. En un primer paso se estudiar´an las propiedades estructurales de estas clases para comprobar que son adecuadas para el modelado y an´alisis del tipo de problemas considerado. Las soluciones al problema de los bloqueos se presentar´an desde dos puntos de vista: prevenci´on y evitaci´on de los problemas de bloqueo, junto con algunos datos comparativos con otras soluciones al problema. El objetivo es obtener pol´ıticas de control muy permisivas, que puedan implantarse seg´un diferentes consideraciones, proporcionando flexibilidad al dise˜nador del sistema. Finalmente se propone una mejora de un m´etodo de c´alculo de cerrojos. Estas componentes estructurales est´an ligadas a la existencia de problemas de bloqueo en algunas clases de sistemas, y en ese sentido es muy conveniente disponer de m´etodos eficientes para su c´alculo. El m´etodo propuesto mejora a los existentes mediante la utilizaci´on de paralelismo, y la adaptaci´on a las caracter´ısticas de los sistemas considerados. Abstract This work concentrates on deadlock problems in concurrent systems due to the common use of system resources organized in what is commonly known as Sequential Resource Allocation Systems and paying a special attention to subclasses of manufacturing systems. To do that, special classes of Petri net models are defined that allow to capture resource allocation events used to synchronize processes that have to share a set of reusable system resources. The classes of Petri nets introduced are studied from the structure point of view, showing the clear mapping among system and model structures. It is also shown how deadlock related situations can be explained in terms of markings and model structures. To solve deadlock problems, two different approaches are adopted. The first one is known as a deadlock prevention perspective, and makes an intensive use of different liveness characterizations developed in this work. The final result is a deadlock prevention algorithm that iteratively constrains the language of the input model so that the final controlled model is live in terms of Petri net definitions, which implies that the controlled system is free of deadlocks and ensures that the execution of any active process can terminate. The second approach falls into the deadlock avoidance family of solutions. In this work it is shown how the specific characteristics of the class of systems in consideration can be used to extend and improve the well-known Banker’s solution for deadlock avoidance, allowing us to give a solution to deadlock problems in the most general class of sequential resource allocation systems. In both cases, and taking into account that obtaining the most permissive solution is NP-complete, the proposed solutions are experimentally compared with other solutions in order to get insight of how permissive the proposed algorithms are, showing they provide a good trade-off between computation cost and permissiveness. xvi 5.10 A different distribution of resources among four processors for the FMSAD–8 problem ......................... 168 5.11 A different distribution of resources among six processors for the FMSAD–8 problem ......................... 168 5.12 A comparison with a different distribution of resources for the first family . ............................... 172 Chapter 1 Introduction 1.1 Motivation When several activities need to be done, and they can be in progress at the same time, we can configure them as a concurrent system: users trying to run programs in an operating system, processes trying to access to a database system, clients trying to do some bank transactions, parts being processed in a production plant, etc.A concurrent system can be seen as the composition of a set of independent, interacting components. The management of such a concurrent system is the management of these different simultaneous activities and the interactions among them. In many cases, a concurrent organization can improve the system performance, abilities, and usage. As a classical example of concurrent system, let us recall the dining philosophers problem, proposed in [Dij65]: Five philosophers spend their lives thinking and eating. The philosophers share a common circular table surrounded by five chairs, each belonging to one philosopher. In the center of the table there is a bowl of spaghetti, and the table is laid with five forks, as shown in Figure 1.1. When a philosopher does think he does not interact with other philosophers. From time to time, a philosopher gets hungry. In order to eat he must try to pick up the two forks that are closest (and are shared with his left and right neighbors), but may only pick up one fork at a time. He cannot pick up a fork already held by a neighbor. When a hungry philosopher has both his forks at the same time he eats 2 1. Introduction Figure 1.1: The dining philosophers problem without releasing them and when he has finished eating, he puts down both forks and starts thinking again. These systems, being able to carry out several activities simultaneously, have a new property: the sequence of operations involved in the different concurrent activities show only a partial ordering, as opposed to sequential systems, where a total ordering is imposed on the execution of the system activities. In the previous example, each philosopher can be seen as a sequential system: when he is hungry, he gets the forks, starts eating, finishes eating, and releases the forks. When all the philosophers are considered this same ordering is acceptable (for each one individually), but no total ordering relation can be established if the whole set of operations is considered. This uncertainty over the precise order of some events is a property that is referred to as nondeterminism. Usually, a concurrent system is generated by a set of agents, executing each one of them their own sequence of activities, but that need to interact with others in order to terminate their tasks. This introduces a new concept in concurrent systems, which does not exist in sequential systems: interaction. In general, this interaction can occur in three different circumstances [SPG91]:  Competition for shared resources: several processes may need the use of the same set of resources, having in some occasions to compete for them. The term resources is used here in a broad sense: it will represent the physical or 1.1. Motivation 3 logical entities needed to carry out the system activities (in the philosopher example they are the forks). For example, each philosopher needs to share a fork with one of his neighbors. To eat, they need to compete: if one of the philosophers gets the fork, the other will not be able to eat until the former release the fork.  Cooperation. This can be done in two ways: – Exchange of data between processes: the results of some processes can be useful/necessary for other processes, as they may need them in order to advance. For example, a philosopher could inform his neighbors about when he expects to finish eating, in order to let them know when to get the forks. Of course, and if it has sense, they could share the result of their thinking periods. – Temporal considerations: that is, when the activities need to occur and how their relative timings are: at the same time (in parallel), one after another (in a sequential way), etc. For example, a philosopher only can begin to eat before or after his two neighbors use the corresponding forks. In these three cases the processes need to synchronize their activities; either to avoid conflicts, or to cooperate to achieve some task. Concurrent systems may/must exhibit some specific properties which can be non–defined (or trivially obtained) in non–concurrent ones. These are properties related to the interactions among the processes. They can be classified as safety properties and liveness properties.  Safety properties: these properties represent that nothing bad will ever happen. That is, they are related to the avoidance/non–existence of bad states. Let us remark the following desirable properties: – Mutual exclusion is needed when some sections of the concurrent system have to be atomic respect to other sections. That is, when one of these sections is being executed, the others cannot be being executed. In the philosophers example, two neighbor philosophers cannot be eating at the same time. The sections ‘eating’ of those two philosophers are in mutual exclusion. 4 1. Introduction – Absence of deadlock; a deadlock occurs when some processes are waiting for the evolution of other processes, that are also waiting for the former ones to evolve. For example, if there are activities using resources and waiting for the resources that others are holding, and if these activities are holding some resources requested by the first ones all of them will be waiting for each other’s resources and no evolution will be possible. If the five philosophers get hungry at the same time, all of them get the fork that is on their right, and they are actively observing the others until the other fork is available, the reached situation is a deadlock: none of the philosophers will releases his fork, and none of them will be able to eat because the other fork is being held by another philosopher. – Absence of race conditions; race conditions occur when several entities are about to perform some action. Depending on the exact timing, they will perform the action following some ordering. There is a problem when the correct result depends on this ordering. For example, if a philosopher checks for the availability of his right fork and then requests it, his colleague on the right can be fast enough to get the fork between these two steps.  Liveness properties represent that some good things will eventually happen. That is, they are related to the existence of good behavioral properties: it not only works, but it works well. Let us remark the following ones: – Absence of Livelock; a livelock occurs when an entity is busy waiting for some event to occur, and it cannot be ensured this to happen. Let us suppose that the philosophers have adopted the following policy: a philosopher who becomes hungry will get first the fork on the left, and then the fork on the right. If the fork on the right is not available, he will desist and leave the left fork on the table. Now, the philosopher number one becomes hungry: he gets his left fork, then the right one and starts eating. While he is eating, the philosopher number three becomes hungry, gets his left fork and later the right one. The philosopher number one finishes eating and releases his forks. However, before the number three finishes eating, philosopher number one becomes hungry again. Both philosophers continue eating and thinking following the same pattern. The philosopher number two (who is located between 1.2. The deadlock problem 5 number one and three) will never eat: when philosopher number one is eating, he will not be able to get his left fork; when philosopher number three is eating, he will take the left fork but he will not be able to get the right one and will return to thinking state. – Fairness properties are related to every entity (user, process, etc.) being able to carry out its activity in similar conditions as the rest of entities in the system. If some philosopher gets hungry very often and is very fast acquiring the forks, or he gets the forks and does not release them, the philosophers next to him will not be able to eat, and the system is not fair. – Absence of starvation; starvation occurs when an entity needs some system event to occur and it is repeatedly overtaken in such a way that it is not guaranteed that the activating event will occur in finite time. Both deadlock and livelock situations presented above will make that no philosopher can eat, so they are clear cases of (literal) starvation. Another example can be when some philosophers never get to eat because their neighbors are faster. 1.2 The deadlock problem Remember that a deadlock occurs when some processes are waiting for the evolution of other processes, that are also waiting for the former ones to evolve. When a deadlock affects all the system activities, a total deadlock occurs. When it only affects some activities, it is called a partial deadlock. Both of them are undesirable situations since they make that some (or all) of the activities cannot terminate. Furthermore, in some cases no new activities can start, or if they can start, they will never terminate. Let us remark that two kinds of deadlocks can appear in concurrent systems (see for example [Sin89a]): resource deadlocks and communication deadlocks:  In resource deadlocks, processes make access to resources (data objects in database systems, machines, tools or buffer space in manufacturing systems, etc.). When the state of a concurrent system is such that each process is waiting for some resource that is being held by other process in the set, in such a way that any further change of state depends on the allocation of one of the involved resources, we say that it is a resource deadlock. 6 1. Introduction In the previous example, the resources are the forks; the philosophers need them in order to eat. If all of them decide to start eating at the same time and get their left fork, a deadlock is reached.  In communication deadlocks, processes communicate via message passing. A communication deadlock corresponds to a system state such that a set of processes exist so that each one of them is blocked, waiting to receive some message from another process in the set, but none of them can deliver his messages. Let us now suppose that the philosophers used as example decide to modify the synchronization protocol: before taking a fork, a philosopher will ask the philosopher who is near to it whether the fork is free or not. If it is free, he will get it; if not, he will request the other philosopher to inform him about when he will release the fork so that he can get it. If all the philosophers decide to eat at the same time, they’ll ask the left philosopher about the fork, they will be able to get this fork and then, they will ask to the right philosopher for the other one. None of them will be able to release the corresponding fork, so none of them will be able to notify the other philosopher that he has finished. We will have a situation where all the philosophers are waiting for the message about the availability of its right fork, but none of them will be able to send such message. As stated before, this work concentrates on resource deadlock problems. In resource related deadlocks, four necessary conditions must occur (see, for example [CES71]):  Mutual exclusion: At least one resource must be held exclusively; that is, it can be used by only one process at a time. Other processes requesting this resource will be delayed until the resource has been released by the process that is using it.  Hold and wait: There must be at least one process that is holding a resource and waiting for other resources currently held by another processes.  No preemption: Processes cannot be forced by any external entity to release resources.  Circular wait: There must exist a set of waiting processes that can be ordered in such a way that each one of them is waiting for a resource that is 1.2. The deadlock problem 7 held by the next one, and the last one is waiting for a resource held by the first one. In the philosophers example, at the described deadlock situation, we can see that the four conditions hold:  A fork can be used by just a philosopher at a time (mutual exclusion).  Each philosopher is waiting for the philosopher at its left, in order to get the fork (hold and wait).  There is no way for a philosopher to release its fork without obtaining first the other fork and eating (no preemption).  Each philosopher is waiting for the philosopher at his left, who is waiting for the philosopher at his left, and so on, in such a way that they are in a circular wait. 1.2.1 Strategies to deal with the deadlock problems Typically there are four strategies to deal with deadlock problems:  To ignore the problem (The Ostrich algorithm [Tan87]). The idea is to leave the system evolve, without worrying about deadlock problems. This strategy is adequate when deadlock problems are not as frequent as other events that force the system halting (breakdown, reconfiguration, etc.) and a deadlock is not a risky situation.  Deadlock Detection and Recovery. The system freely evolves. A monitoring subsystem is running; when a deadlock situation is detected, a rollback process should move the system to an adequate state. A recovery strategy requires to “kill” some of the active deadlocked processes. In some cases (in an operating system, for instance) this can be easily done. However, in other systems this can be almost impossible or very expensive (imagine to have to move a plane or a car in order to free some resources). For example, in a deadlock situation, the philosophers can discuss. Then, they can decide which ones have to release their forks in order the others can eat. 8 1. Introduction  Deadlock Prevention. The system is designed to be deadlock–free by ensuring that no deadlock situation can occur. In some cases, this can mean that some restrictions have to be imposed to the situations under which a process can be activated (or it can evolve). Usually, some off–line computations are needed before a prevention approach can be applied. Let us consider, for instance, a system for which it is known that it can deadlock if there are three or more active processes, but no deadlock can occur with two or less active processes. Then, a prevention policy could consist in ensuring that no more than two processes are active at the same time. As a second example, let us consider another system where a set of processes share a set of non–consumable resources. It is well known that if an ordering can be established in the set of resources in such a way that each process uses the resources according to this ordering, no deadlock can occur (since no circular wait is possible). Then, a prevention policy would consist in designing the system in such a way that only processes that request the resources following this ordering are accepted. For example, if this approach is adopted for the philosophers problem, it is necessary to convince the last one to get the forks in reverse order than the other philosophers (first the right fork, then the left one).  Deadlock Avoidance. These strategies constrain the system evolution so that only safe states are reached. A reachable state is said to be safe if, once it has been reached, it can be ensured that all the active processes can terminate. An avoidance policy must be able to know whether a state is safe or not (or, at least, to be able to select a subset of safe states). Usually a deadlock avoidance strategy runs as follows: when a state change is possible, the controller checks for the safeness of that state. If it is safe, the system transition is allowed; if not, it is forbidden. Therefore, avoidance control policies require the on–line checking for the safeness of a given state, which implies that very efficient algorithms are needed. The most classical example for this approach is the well–known Banker’s algorithm [Dij65]. In this work we are going to concentrate on the prevention and avoidance approaches. Their main differences can be abstracted as follows. Initially, we have a set of processes that share a set of system resources. In order to execute a process action, two conditions must hold:  First, the necessary resources must be available. 1.3. Flexible manufacturing systems 9  Second, the state reached if the action is executed must be neither a deadlock nor a state leading in an inevitable way to a future deadlock. In the case of a prevention approach the control necessary to ensure the good behavior has been, in some way, embedded in the system structure, so that instead of executing the original processes a set of transformed ones are executed. The way the processes have been transformed ensures that as soon as the needed resources are available, a process action can be executed, because no system deadlock can be reached in the modified system. In the class of systems we are going to concentrate on in this work each process state will be explicitly modeled. A deadlock state corresponds to a given tuple of process states. A way to prevent such state would consist in establishing a generalized mutual exclusion on the involved processes so that the tuple is not reachable. From the model perspective, these mutual exclusions can be implemented as a kind of logical resources, whose integration in the model will be straightforward (if we are able to model physical resources, we are also able to model logical ones) obtaining the model of the controlled system. If the control is carried out in this way, the prevention approach has been adopted. In the case of an avoidance approach, an external decision procedure has to be launched each time a resource related action has to be executed. This procedure will allow the action only if it is sure that no future deadlock problems can arise. 1.3 Flexible manufacturing systems Flexible manufacturing systems (FMS) are part ofan interesting class of concurrent systems. They are used to organize production systems in such a way that they can be quickly adapted to new customer demands. In this work we are mainly concerned with the control of such systems (to avoid deadlock problems). Let us introduce in this section their main features. Aflexible manufacturing system is an automatically controlled set of machines, material handling, and storage facilities that can process simultaneously a set of different types of products. Usually, a  has two main subsystems [VN92], as depicted in Figure 1.2:  Thephysical subsystem, composed ofthe physical elements (hardware components) such as transport facilities (conveyors, robots, pallets, automated guided vehicles –AGVs–, etc.); processing machines (work stations, tools, 16 1. Introduction L C1M1C1R1 R2 U C2 M3 C2 M4 Type 1 Type 2 M1C1 C1 M2 C1 C2 LR1 U R2 (a) I2 R3 M4 R2 M3 R1 O 2 B2 Type 1 Type 2 I 1R2M2R3 B1 M1 M3 R1 O1 (b) Figure 1.5: Skeleton of the different routings for the types of parts to be processed in the cells depicted in Figure 1.4 1.3. Flexible manufacturing systems 17 one of such tools. Machine  uses one copy of each tool for the processing of each part, while machine  uses only one copy of  .  contains two copies of  tool and two copies of  tool. Machines  and  use one  tool and one  tool for the processing of each part. In order to move parts between the cell components there are three robots,  ,  ,  . Robot  loads machines  and  from  , and unloads machine  towards point  . Robot  loads and unloads the four machines, and can also interact with the intermediate buffers  and  . These buffers are used for the intermediate storage of parts of type 1 and type 2, respectively, whose processing has not finished yet. Each one of these buffers has capacity for simultaneously storing a maximum of four parts. Finally, the cell also contains a robot  , which can load parts into machine  from  and unload parts from  to  . Parts of type 1 are taken from a conveyor at point   , processed in machine   or   , then in machine   and finally unloaded on a conveyor at point   . Parts of type 2 are first loaded into the system from a conveyor at point   , then processed in machine   and machine   and finally unloaded to another conveyor at point   . ¾ The system of this example is clearly a NO-RAS. The possible routes for these types of parts can be seen in Figure 1.5(b). About the use of resources The main constraint related to resources refers to the number and type of resources a process can use at a given state. According to this point of view, resource allocation systems can be classified into the following categories [LRF98a]:  Single Unit RAS (SU–RAS): at each processing step, a part requires a single unit from a single resource type (just one unit of buffering capacity of the resource holding the part).  Single Type RAS (ST–RAS): at each processing step, a part can use several units of a single resource type. This allows to model the use of different buffering capacities that different parts can need, and also the different buffering capacities that jobs organized in batches can need, depending on the size of the batch.  Multiple Type RAS (MT–RAS): at each processing step, a part can use several units of several types of resources (the buffering capacity used by the part plus a set of tools, for instance). 18 1. Introduction It is clear that SU–RAS  ST–RAS  MT–RAS.Most previous work concentrate on the SU–RAS, however, this constraint was removed, for example, in [BCZ97, TCE99, TGVCE00]. For the MT–RAS there have been partial approaches, where the resources must be requested one copy at a time [TGVCE98, JXH00, HJW02, GS02], until the needed buffering capacity is reached. Another approach is the MT–single unit– RAS(just one copy of several types of resources allowed) as can be seen in[CX97]. We will comment more on some of them to compare with our approaches, when needed.  A lot of work can be found for the SU–TO–RAS ([BK90, VNJ90], [HC94, FMMT97, XHC96, EGVC98b]).  A solution for the MT–TO–RAS can be found in [RR92b].  For a subclass of the SU–PO–RAS class, where a special case of routing flexibility is allowed (each operation can be carried out in a set of different resources), solutions can be found in [Rev98, Rev99, Law00]. The flexibility is reduced because these methods need that a part can flow between any pair of resources that can be used in two consecutive steps.  In [GK90, Lan99, TCE00] different solutions for the MT–PO–RAS can be found.  Solutions for the MT–NO–RAS can be found in Banker’s like approaches. For example [KTJK97, TCE00]. In this work, we are going to present different solutions for the deadlock problem for MT–PO–RAS (Chapter 3) and for the MT–NO–RAS (Chapter 4). The previous review has been constrained to the case of S–RAS, and less attention has been paid to the case of NS–RAS. Nevertheless, let us note here that there are some alternative approaches, exploring the problem different models. Some examples can be found in [RR92a, FTM99, JXH00]. 1.3.2 Petri nets and other formalisms to model and control  In previous sections we have seen FMS’s as complex systems. To deal with this complexity, and given the special characteristics of the type of systems we are considering, the use of formal methods is highly desirable. Formal methods improve the understanding of the system, giving tools for the analysis and implementation 1.3. Flexible manufacturing systems 19 steps. They also help in the dialog between the different people related to the design, construction and system management [ST97]. Although the processing of parts in machines and the transport across different handling devices can be continuous processes, the system can be seen as a Discrete Event System (DES) when we concentrate on the use of resources: we have to consider the events related to the allocation/deallocation of resources (or the events of sending/receiving messages) which occur in a discrete way. Different formalisms have been used to deal with the modeling and control of flexible manufacturing systems (and concurrent systems in general.) Some examples of models used with similar objectives are:  Models based on formal languages [RW87];  Models based on finite state automata [RF96];  Models based on temporal logic [Ost89];  Finitely recursive processes [IV88], which are based on Hoare’s communicating sequential processes [Hoa85];  Graph theoretic tools [CKW95, FMT00, Law99];  Finally, the approach used here, Petri nets, that have been widely used (see, for example, [Giu96, HKG97, ST96], for some survey papers. For some recent work see, for example, [ECM95, BCZ97, Che00, TCE00, TGVCE00, PR01, Ge03].) The first three approaches are mainly based on finite state automata: formal language models use automata in order to model discrete event processes; and models based on temporal logic use finite state transition systems plus temporal logic formulae in order to specify and verify some behavioral properties. All of these approaches have the main disadvantage of the state space explosion problem. There have been some approaches to overcome this problem. Some examples are the use of some subclasses of Petri nets to model the system in [Sre00], the use of a modular and decentralized control [RW92], or the application of a modular and algebraic manipulation for component interaction [XHD99]. The graph theoretic tools have also the same problems of lack of modularity and state space explosion. Finitely recursive processes allow to model the system as a set of recursive equations. However, as stated in [ZD93a], it is not clear how to use them to design supervisory controllers for real–time systems. 20 1. Introduction We are going to use Petri nets in order to model and control the systems considered here. Petri nets are effective for modeling DESs and FMSs for the following reasons [SV89, ZD93b, ST97]:  Easy representation of concurrency, resource sharing, conflicts, mutual exclusions, and non–determinism.  Availability of different levels of abstraction, allowing to adopt different classes of Petri nets at different phases of the production process.  A well–defined semantics, which allows the system validation and property verification by means of the model analysis.  The possibility of code generation from the Petri net model in order to get a prototype of the control program.  A nice and intuitive graphical representation, which in some cases can be a great help for the people involved in the modeling of the system. In consequence Petri nets can be used in all aspects of the design and operation of a  : modeling and verification, performance analysis, scheduling, control and monitoring, implementation, etc. The study of a general concurrent system is a difficult task because of the variety of situations that can appear. Fortunately, the class of systems that we are considering will be modeled with special subclasses of Petri nets, which will be introduced and studied in the following chapters. The special characteristics of such classes of nets will allow us to obtain very useful system behavioral properties which will be used to control the system. These properties will be obtained in a structural way; that is, using the structure of the model instead of the set of reachable states, avoiding the state explosion problem. 1.3.3 Characterizing deadlock problems When trying to eliminate deadlock problems, it is very important to be able to characterize what causes these problems. Let us concentrate now on the most usual methods used to study deadlock problems in concurrent systems. These methods depend on the model used to represent the system, and most of them take advantage of some structural limitations imposed to the way processes can interact. Anyway, in some cases models take advantage of methods proposed in other frameworks. The different methods used to deal with deadlock problems can be classified as follows: 1.3. Flexible manufacturing systems 21  Methods based on the reachability set: They construct, either in a total or partial way, the set of states the system can reach. This makes possible to exactly know which are the undesirable markings and, in consequence, avoid them. This approach can give, in general, more accurate results. However, it is very expensive and, in some cases, unaffordable due to the size of the reachability set. Most of the supervisory–based work [RW89], some Petri nets–based work, and other studies using model checking, use the total or partial construction of the reachability graph [VNJ90, CKW95, BLP96, CG96, OH00, Giu96, RJ96, LRF97, BCG98, XHD99, MBSD99, QJ99, LMB97, Sre00, YB00].  Methods based on structural characterizations: Several approaches try to capture the hold and wait situations using the structure of the involved processes: –The first approach, which will be called based on cycles, looks for cycles of resources that can reach a hold and wait situation. Some of the work following this line lack of a complete characterization of the problem; cycles of resources do not completely represent all the hold and wait situations than can appear. Some work following this approach can be found in [RYJ91, FNTS94, JD95, HSBM96, FMMT97]. –The second approach, which will be called based on siphons, is related to some structural components of the Petri net model, called siphons. The previous approach can be considered as a partial version of the siphon based methods. Although in some cases ([EGVC98a]) cycles and siphons are equivalent, the approaches based on siphons can deal with more general classes of systems. There exist also some algebraic– based approaches [PR00b, PR00a, Law00] that, in most cases, are closely related to siphons, and will be considered as siphon–based. Some work following this approach can be found in [ECM95, BPP96, CX97, Jen96, AE98, LRF98b, LGB  98, XJ99, Che00, MV00, PR00a, TGVCE00].  Look–ahead based methods. These methods are based on some knowledge about the future needs of resources of each active process. These approaches do not focus on the set of ‘bad states’; the goal is to keep the system in ‘safe’ states. That is, given a state that is known to be ‘good’, the control policy will only allow the system evolution into another ‘good’ state. The problem for 22 1. Introduction these methods is to establish whether a state is safe or not. For this, several approaches have been considered in the literature, being the main difference the knowledge about the future states used to define a state as ‘safe’: –an estimation of the future maximal needs of resources used in the original Banker’s proposal [Dij65, Hab69, SPG91], –information about the resources needed to finish the processing in a zone (zones are usually defined as subsequences of the available processing sequences. These zones are selected in such a way that at the beginning and the end of each zone, the use of resources does not interfere with the use of resources of other processes.) In this way, if the system can be partitioned taking advantage of intermediate points, better policies can be obtained [BK90, RR92b, EH93, RF96, Lan99]. –detailed information about where and when resources will be needed, used in [TCE00, Rev98]. –finally, some approaches use a partial look–ahead policy [VNJ90]. A number of steps is fixed, and before allowing any system evolution, they simulate the advance of these steps. If they do not find problems, the system is allowed to evolve. As they only look forward a fixed number of steps, these control policies need to have a deadlock detection algorithm because the absence of problems in a fixed number of steps does not guarantee the absence of problems in further steps. Of course, it is always possible to do a complete look-ahead checking, trying to see if there are system evolutions from a given state that allow to finish all the active processes [YB00]. Clearly, this approach is very time consuming since in some cases it can be equivalent to compute the whole reachability graph. 1.4 Work Outline Chapter 2 is devoted to the introduction of a new class of nets, named    , that will be used for the modeling of flexible manufacturing systems. The class is introduced in a compositional way, which allows a simple and useful model construction. The class of models considered is able to deal with the multiple type, partially ordered resource allocation systems (MT–PO–RAS.) For this class, a liveness characterization will be established, followed by some results that will be applicable for deadlock prevention. It will be presented in three different forms: the first one is 1.4. Work Outline 23 a characterization of the deadlock problem in terms of the marking of some places related to the set of transitions directly involved in a deadlock; the second and third characterizations show how liveness problems are related to the existence of a special kind of siphons, which will be used to select some ‘representative’ markings in order to prevent deadlock related problems. In Chapter 3 the siphon–related liveness characterization presented in Chapter 2 is used to prevent deadlocks. The process behind the control method is as follows. The liveness characterization relates siphons and deadlocked markings. The system behavior is represented by the state equation and some integer programming problems that allow to obtain a (potential) deadlocked marking. We introduce a way for preventing such markings by means of the addition to the some new place which makes the considered marking unreachable. It is then proved that the behavior of the added place is like a virtual resource, and it is then concluded that the net controlled in this way is a    . Therefore, the method can be iterated. It is also proven that the algorithm terminates, obtaining a final controlled    which is live and whose language is a subset of the language of the original system. Chapter 4 concentrates on deadlock problems, but from an avoidance point of view, and using the ideas behind the well–known Banker’s algorithm proposed by Dijkstra [Dij65]. The avoidance approach we propose is able to deal with the multiple–type, non–ordered resource allocation systems (NO-RAS. In order to get a better understanding of the method, a general framework and an algorithm based on this general framework are presented. The framework is based on the definition and parametrisation of a set of functions, used to establish a bound of the future needs of resources for each active process. This framework allows us to present and study several solutions for the problem as special cases of the general case. Some particular solutions, together with the study of their runtime costs, are proposed, being one of them the classical Banker’s algorithm. Since some of the proposed methods for the deadlock prevention rely on the computation of sets of siphons ([TCE99, IMA02]), some research has been done to obtain better solutions for this problem. These results are shown in Chapter 5. We will show a review of the available methods, trying to establish a classification for them. Later, one of these methods will be selected, having in mind the kind of problem we need to solve (siphons that contain resource places in    nets), and the way we expect to reach the improvements (parallel computing). Finally, some numeric computations have been done in order to test the proposed approach and to compare it with some recently proposed efficient solutions. Chapter 2 The Ë  ÈÊ class: definition and properties Abstract A new class of systems is going to be presented. This class, named    ,is adequate for the modeling of a wide variety of RAS. The special syntactic characteristics of the nets of this new class make possible the study of the modeled systems from a structural perspective. The chapter introduces the class, first by means of an an example, and then in a formal way. The main structural properties of the nets belonging to this class are studied. Finally, a characterization of deadlock situations and several re–formulations in terms of siphons are presented. These characterizations will be used in the next chapter in order to control the system to prevent deadlock problems. 2.1 Introduction As stated in the introductory chapter, the variety of elements involved in a typical  makes necessary the use of some formalism in order to manage this complexity and to improve the understanding of the system. We are going to use Petri nets to model and control the systems considered here. In the previous chapter we made a classification of the systems based on two main characteristics: the routing of parts and the restrictions on the use of resources. The class that will be presented later allows to model on–line routing flexibility (that is, a part can 32 2. The    class: definition and properties the resources need to be taken one copy at a time until the total amount of needed copies is reached. 2.2 The Class of Ë  ÈÊ Nets    nets will be used to model the concurrent processing of a set of parts of different types. All the parts of the same type have the same processing possibilities. The whole model will be obtained by means of the composition of the process Petri net modeling the processing of the different types of parts. 2.2.1 Modeling processes: process Petri nets Let us remember, before defining it, that the class of S–RAS allows flexible routing (which means that on–line, real–time routing decisions can be modeled) and the use of any number of reusable, non–consumable resources at each state. Definition 1 Aprocess Petri net is a generalized strongly connected self–loop free Petri net         where: 1.  is a partition as follows:            . 2. The subnet generated by         ,      ¼      , is a strongly connected state machine such that every cycle contains   . 3.      , there exists a unique minimal P–Semiflow    IN    such that           ,          ,          and      . 4.                 . ¾ From the application point of view, a process Petri net will be used to model the processing of a type of part. Place   is the idle state place (or idle place); we will use        . It models a raw part before entering the system. Places in   are the state places (or process places) and model the states for a part of the considered type. Transitions of  model the state changes. A change in the state can correspond to two different kinds of events: either the part changes its location in the system (moving from one resource to a different one), or a transformation has been done in the part (as 2.2. The Class of    Nets 33 the result of a system operation inside a machine.) Arcs joining places of      with transitions correspond to the state changes in the processing of each part. Places in   are the resource places and model the state of the system resources. Arcs joining resource places and transitions of the Petri net model how the state of the resources change when the parts evolve in the system. Arcs related to resource places model how resources are used for the processing of parts: outgoing arcs from resource places to transitions model the acquisition of resources; arcs from transitions to resource places model their release. Let us do some comments about the three last points of Definition 1:  Point 2 establishes the structure allowed for the set of states that a part can follow during its processing, as commented before. The fact of imposing that each cycle must contain place   corresponds to the idea of “processing evolution” in the system: if transitions are executed, the processing of a part will eventually terminate. This forbids the existence of parts evolving in a limited subset of states inside the system.  Point 3 establishes that each resource must be serially reusable (it cannot be created nor destroyed in the system.)  Point 4 imposes that each processing step requires the use of at least one resource. This represents that when a part is being processed, it must be “somewhere” in the system using, at least, some buffer space of it. From a theoretical point of view, this constraint is not needed, and could be withdrawn. The results we are going to present will also be valid if constraint 4 is suppressed: it can be easily seen that for each place     not belonging to the support of any   its complementary place can be added, with an initial marking equal to the one of   . These added complementary places are implicit and behave as ‘virtual’ resources. Moreover, the resulting net is a process Petri net with the same firing sequences as the initial one. The process Petri net that represents the processing of parts following the working plan  in the cell depicted in Figure 2.1 is shown in Figure 2.4. There, the following elements can be identified:                                                                   34 2. The    class: definition and properties In order to complete the modeling of the dynamics of a process Petri net, an initial marking must be provided. The tokens in a reachable marking can have different meanings:  A token in a place     will model an active process (a part being processed) whose state is modeled by means of place  (the part is at the state represented by this node.) Several tokens in the same process place will represent several active processes (several parts being processed) whose respective states are modeled by means of place  .  Tokens in a place     will model the available buffering capacity of resource  at the system state modeled by the considered marking (remember that, as previously said, buffering capacity will be used to represent either capacity or availability.) Markings need to represent states that have a physical meaning. In this sense, only acceptable initial markings, as defined in the following, will be considered. If the system is well defined, and its initial marking is “correct”, all the markings that are reachable from it will represent possible states of the system, and will have a physical meaning. Definition 2 Let               be a process Petri net. An initial marking   is acceptable for  if and only if: 1.         ; 2.            ; 3.                        . ¾ A process Petri net with its marking will be used to represent the processing of a set of parts of the same type. Let us remark the following facts:  The initial marking of   (condition (1)) represents the maximal number of parts of the type modeled with this net that are allowed to be concurrently processed in the system. This initial marking can be chosen in such a manner that   becomes implicit [Sil85, CS89], making this kind of systems suitable for the modeling of open systems (the maximal number of parts of the type modeled by the process Petri net concurrently processed is limited by the system itself via the capacities of the system resources.) 2.2. The Class of    Nets 35 P1R1 P1M1 P1M3 P1R2 P1M2 R1 M1 M3 R2 M2 P1R3 R3 P1_0 10 h1 h3 h2 h4 T2 T3 T4 T4 T6 T7 T1 T8 Figure 2.4: The process Petri net model of the system whose layout is shown in Figure 2.1 when the two types of parts to be produced are considered  No process is active at the initial state (condition (2).)  The buffering capacity of each resource is such that each processing step can be executed when the isolated execution of one process is considered (condition (3).) This property will be proved later. Some basic structural properties of process Petri nets Let us now present some structural properties of process Petri nets relating structure components and its physical meaning. 36 2. The    class: definition and properties We are going to show how the minimal P–Semiflows induced by the structure of these nets are, and how can be intrepreted from the application domain point of view. Let us first consider the P–Semiflows related to resources as they appear in Definition 2. These minimal P–Semiflows induce marking invariant relations of the form                     . They can be interpreted in the following way: 1. For every reachable state, the buffering capacity of a resource type,  ,is constant and it is equal to the buffering capacity at the initial state:            . Notice that this property establishes an important feature of the class of systems considered: resources are re–usable. Re–usability implies that the utilization of the resources by the processes does not change them. Then, the buffering capacity of each resource is invariant. 2. At a reachable marking  , the initial capacity of a resource  is distributed in the following way:     is the capacity of  available at  ; for any     ,      is the buffering capacity of resource  used by a process at state  , and           is the capacity of resource  used by processes at  . Considering resource  in Figure 2.4, the associated P–Semiflow is           , which induces the invariant relation                    for every reachable marking         . In consequence, one of the following expressions is true:                                                 which means that  can be processing two, one, or zero parts, respectively. When       , two parts are being processed at machine  , modeled by the tokens allocated in  (         .) For a given resource,  , and based on the minimal P–Semiflow   , the holders of resource  are going to be introduced as the set of process places using this resource. Definition 3 Let               be a process Petri net. Let     . The set of holders of r is the support of the minimal P–Semiflow   without the 2.2. The Class of    Nets 37 place  :          . This definition can be extended in the natural way to sets of resources     :          . ¾ Why the name “holder”? Let us consider the net in Figure 2.4 and the resource place  . For it,           ; considering          , each time a token enters place  , a token “disappears” from  (maintaining the invariant relation), i.e., an active process in  is “holding” one capacity unit of the physical resource represented by place  . Notice that the invariant induced by   also states that                         . In each process Petri net one more P–Semiflow can be identified; it is related to the process structure and its configuration as a state machine. Proposition 4 Let               be a process Petri net.Then,       ¼      ¼        is a minimal P–Semiflow. Proof Let us show that       ¼      ¼        is a P–Semiflow. The net     ¼      is a strongly connected state machine and then, it has a unique minimal P–Semiflow whose support is      . Moreover, since              ,   is a P–Semiflow of  . Furthermore, being a minimal P–Semiflow of     ¼      and being a P–Semiflow of  , it also needs to be minimal in  :if   was a minimal P–Semiflow whose support is strictly included in the support of   , and as far as   does not contain places of   ,it also would be a minimal P–Semiflow of the net     ¼      , and then      . ¾ This last minimal P–Semiflowinduces a marking invariant relations ofthe form                     . This invariant can be interpreted in the following way: 1. For every reachable marking, the number of tokens representing processes of the type modeled by the net is constant and it is equal to the number of tokens in the idle place at the initial state:             . This constrain is related to the idea that a token that represents a part in the system cannot generate several parts or, reversely, disappear. 2. The number of parts of the considered type that can be concurrently processed is bounded by       . However, as previously commented, this is not a limitation since the initial marking of   can be big enough to allow the modeling of open systems. 38 2. The    class: definition and properties Let us consider once again the net in Figure 2.4. The minimal P–Semiflow                               generates the following invariant relation:                                                               , imposing that a part following  in the cell of Figure 2.1 can be either held by a robot (places             ) or processed in one of the machines (places             .) The next lemma presents a result relating rows representing resources in the flow matrix and rows representing the other places of the net. This lemma will be used later on to relate net circuits and T–Semiflows. Lemma 5 Let               be a process Petri net.                ¼                                  where              . Proof 1. The net     ¼      is a strongly connected state machine. Then, there exists only one minimal P–Semiflow which establishes the following invariant relation     ¼               ¼                     2. By definition of process Petri net,                           . 3. Then:      ¼                           . Then,                          ¼                           and then:          ¼                                  ¾ In fact, since                       , this lemma has proved that each resource place is a structural implicit place (SIP) [Sil85, CS89]. Let us now concentrate on another interesting set of Semiflows related to the sequencing of processing states: T–Semiflows. In order to simplify the notation some conventions are going to be used. 2.2. The Class of    Nets 39 Note 6 Let               be a process Petri net.  Let  be a T–Semiflow of  .  induces the following sets:       , and                            .  Let  be a simple circuit of  .  induces the following sets:             , and       . ¾ For example, in the net in Figure 2.5 the minimal T–Semiflow                induces the sets                   and                             The following lemma shows the relation between minimal T–Semiflows and simple circuits of the embedded state machine corresponding to the complete processing sequences. Lemma 7 Let               be a process Petri net.  Let  be a circuit of  not containing places of   .   induces the minimal T–Semiflow           .  Conversely, let  be a minimal T–Semiflow of  .      generates a simple circuit Proof First of all, since the net     ¼      is a strongly connected state machine, each minimal T–Semiflow of such net induces a simple circuit and vice versa, (because in a strongly connected state machine the set of transitions in a directed simple circuit is a minimal T–Semiflow. See [Mur89], where the property is presented for marked graphs and P– Semiflows.) Moreover, according to Lemma 5,                        ¼                                                      ¼                                                      40 2. The    class: definition and properties which implies that it is also a T–Semiflow of  . Let us prove that minimal T–Semiflows of     ¼      are also minimal in  . Let us consider a minimal T–Semiflow of     ¼      , that is not minimal for  . Since               ,if   is non minimal, this implies that there exists anotherT–Semiflow,   , such that               and        . Let us consider           . Since   induces a simple circuit,                 . This reasoning can be iterated, allowing us to conclude that      . ¾ Notice that any T–Semiflow  , if fireable, corresponds to a firing sequence   such that          , and then,     . From the application point of view, minimal T–Semiflows are related to firing sequences moving a token from   to   following a path in the process Petri net, which corresponds to a complete processing of a part. Any minimal T–Semiflow corresponds to a possible processing sequence. Proposition 11 below shows that any T–Semiflow induces an effective production sequence for parts of the considered type, provided they can be executed in isolation. For example, in the net in Figure 2.5, the previously presented T–Semiflow   models the complete processing of a  –part. Note 8 If  is a process Petri net, and being      simple circuit of  such that it does not contain places of    , the set of minimal T–Semiflows is         . ¾ Note 9 In a process Petri net each transition has a unique input process state place (whose weight is equal to one) and zero or more input resource places. Extending the definitions presented in [XHC96] for SU–RAS, and given a marking,         , a transition  is said to be   –process–enabled (or, process–enabled at  ) if, and only if:              , and               That is, the transition is enabled by the corresponding process place (an active process is ready to fire it.) A transition that is no  –process–enabled is  –process–disabled.   –resource–enabled (or, resource–enabled at  ) if, and only if:         and                     That is, no resource place is preventing the firing of  . A transition that is no  –resource–enabled is  –resource–disabled. ¾ 2.2. The Class of    Nets 41 Let us now prove a lemma relating the resources used by a state place and the resource enabling condition. Lemma 10 Let      ,               be a marked process Petri net. Let         and let    such that               and               . Then,  enables  if and only if       and                       . Moreover, if      ,   is as follows:                                  ,                                     ,      Proof First of all, let us remember that                 ¼                                  where               (Lemma 5.) Then, in this case,                                                   . But              , and then:                                        . Therefore, the first part of the Lemma is a direct translation of the enabling conditions for general Petri nets to the considered class of systems, and the second part is a direct translation of the firing rule. ¾ Based on the previous properties, the following proposition proves that when an acceptable initial marking is considered, a part can be processed in isolation, i.e. the system is well–defined. Proposition 11 Let      ,               be a marked process Petri net. Let                    be a simple circuit containing   . Then    ½  ¾   ·½    Proof Let us prove this result by contradiction. Let us assume that there exists       such that    ½      and such that   does not enable    . Notice that, according to Lemma 10,   is as follows:                ;       ;      ,          ,(        ), 48 2. The    class: definition and properties T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 P1 0 -10000001 P1R1 1-1-100000 P1M1 010-10000 P1M3 0010-1000 P1R2 00011-100 P1M2 000001-10 P1R3 0000001-1 P2 0 -100001 P2R3 1-10000 P2M4 01-1000 P2R2 001-100 P2M3 0001-10 P2R1 00001-1 R1 -111000000000-11 R2 0 0 0 -1 -1 1 0 0 00-1100 R3 000000-11-110000 M1 0-1010000000000 M2 0 0 0 -1 -1 1 0 0 000000 M3 00-101000000-110 M4 000000000-11000 h1 00-101000000-110 h2 00-101000000-110 h3 00000-1100-11000 h4 00000-1100-11000 Table 2.1: Incidence matrix of net in Figure 2.5 We are going to see which properties presented for process Petri nets are also valid for    . In this sense, let us recall a simplified version of a property presented in [NV86] relating P–Semiflows of the composed net and the ones of the individual component nets. Theorem 18 Let             and             two composable Petri nets. Let     Æ  be the net obtained by composition of them by means of of the subset of common places (         .) Let   and   be two P– Semiflows of   and   , respectively, and such that                  . Then,       ½   ½¾   ½   ¾       ¾   ½¾   ½   ¾       ½¾   ½   ¾  is a P–Semiflow of  (          .) ¾ The next lemma shows that minimal P–Semiflows related to state places for each process Petri net are also minimal P–Semiflows of the composed net. Lemma 19 Let                       be a    . Then,            ¼            ¼        is a minimal P–Semiflow of  . Proof Clearly, according to Theorem 18,      ¼            ¼        is a P–Semiflow of  . 2.3. Some properties of    nets. 49 Let us proceed by contradiction: let us suppose that      such thatthe P–Semiflow     ¼            ¼        is not minimal (we can suppose that    without lost of generality.) Then, there exists     ,            ¼ ½    ½    ½   ¼         , such that        . Then,        ½    ½    ½      and this is a contradiction with the fact that    is minimal in   . ¾ The following lemma helps us to see that the use of resources is also conservative in    nets. Lemma 20 Let                       be a    . Let     , and let    ,     , be the minimal P–Semiflows associated to  in each   . Then          ¼                   ¼        ¼        is a minimal P–Semiflow of  . Proof According to Theorem 18   is clearly a P–Semiflow of  . We have to prove that it is a minimal one. Let us assume that   is not minimal. Since      , this means that there exists another P–Semiflow    such that         . Let us consider                 , for some     . Notice that                                , which implies that                 is a P–Semiflow of   such that                        , which contradicts the hypothesis of    being minimal in   . ¾ The next proposition shows a basis of the left annuler space for the incidence matrix of the net. Proposition 21 Let                       be a    . Then, the set                     is a basis of the left annuller space1. Proof We are going to proceed in three steps: 1. First of all, we are going to show that          . Each net     ¼         is a strongly connected state machine, and the rows that model resources in each net   are linear combinations of the rows of the correspondingprocess places. Then looking atthe structure of the matrix, we can trivially say that                           . 1In order to define a vectorial space, we need a group, so using this terminology here is an abuse of language. We could use linear combinations with coefficients in  · (see, for example, [AT85].) 50 2. The    class: definition and properties 2. Now we are going to see that the elements of  are linearly independent. The elements of          are mutually linearly independent because each one of them contains in its support an element     not belonging to the support of any other of them. The elements of          are linearly independent with respect to the ones in           because these ones do not contain elements from   . Finally, the elements of           are linearly independent one respect to each other because their supports have empty intersection. 3. Let us now prove that                     is a basis of the left annuller space. Let  be the left annuller space of  .      number of rows of the matrix                                                  Therefore, we can conclude. ¾ Now, a similar result about T–Semiflows is going to be presented. Lemma 22 Let                       be a    . 1.      ,if   is a minimal T–Semiflow of   , then         is a minimal T–Semiflow of  . 2. If  is a minimal T–Semiflow of  , then there exists     , such that           . Proof 1. Let   be a minimal T–Semiflow of   ; then,       . Therefore,         is such that            . Let us assume that it is not minimal. Then there exists another T–Semiflow of  whose support is contained in the support of   . Since all the components corresponding to transitions not belonging to   are zero, it is also a T–Semiflow of   which contradicts the the hypothesis of   being minimal in   . 2.3. Some properties of    nets. 51 i Support of the P–Semiflow Projection over  ¼ ½    ½    ½ Projection over  ¼ ¾    ¾    ¾ 1  P1R1, P1M1, P1M3, P1R2, P1M2, P1R3, P1 0   P1R1, P1M1, P1M3, P1R2, P1M2, P1R3, P1 0  2  P2M4, P2R2, P2M3, P2R1, P2R3, P2 0   P2M4, P2R2, P2M3, P2R1, P2R3, P2 0  3  P1R1, P2R1, R1   P1R1, R1   P2R1, R1  4  P1R2, P2R2, R2   P1R2, R2   P2R2, R2  5  P1R3, P2R3, R3   P1R3, R3   P2R3, R3  6  P1M1, M1   P1M1, M1  7  P1M2, M2   P1M2, M2  8  P2M4, M4   P2M4, M4  9  P1M3, P2M3, M3   P1M3, M3   P2M3, M3  10  P1M1, P1M3, P2M3, h1   P1M1, P1M3, h1   P2M3, h1  11  P1M2, P2M4, h2   P1M2, h2   P2M4, h2  12  P1M3, P2M3, h3   P1M3, h3   P2M3, h3  13  P1M2, P2M4, h4   P1M2, h4   P2M4, h4  Table 2.2: Minimal P–Semiflows of the    depicted in Figure 2.5 2. Let  be a minimal T–Semiflow of  ; then     . Considering the structure of  ,           for each     , and considering that                 , it is obvious. ¾ Finally, the next proposition establishes which are the sets of minimal P– and T–Semiflows of a    net. Proposition 23 Let                       be a    . Then, 1.         ¼            ¼                  ¼            ¼               is the set of minimal P–Semiflows of  . 2.                    is a minimal T–Semiflow of    is the set of minimal T–Semiflows of  . ¾ Let us see these structural components for the considered example. Table 2.2 shows the list of minimal P–Semiflows for the net in Figure 2.5. The two minimal 52 2. The    class: definition and properties i Support of the T–Semiflow 1  T1, T3, T5, T6, T7, T13  2  T2, T4, T5, T6, T7, T13  3  T8, T9, T10, T11, T12, T14  Table 2.3: Minimal T–Semiflows of the    depicted in Figure 2.5 P–Semiflows numbered 1 and 2 are related to the state machines associated to each process Petri net. The others are related to the system resources. The table also shows in the third and fourth columns the minimal P–Semiflows of each one of the process Petri nets. Table 2.3 shows the T–Semiflowsof the net depicted in Figure 2.5. The twofirst T–Semiflows are associated to the process Petri net on the left, and they correspond to the first working plan; the other T–Semiflow is related to the process Petri net on the right, and it corresponds to the type  . T–Semiflow                induces the circuit whose nodes are:                                               . These results will be used to study the behavior of    nets. In order to complete this section, let us finally present an alternative definition for the    class of nets. Definition 24 Let   be a finite set of indices. A    is a connected generalized self–loop free Petri net         where: 1.           is a partition such that: (a)            , where for each           , and for each          ,          . (b)              . (c)             ,   . 2.           where for each          , and for each          ,        . 3. For each     , the subnet     ¼         is a strongly connected state machine such that every cycle contains    . 4. For each     there exists a unique minimal P–Semiflow    IN    such that           ,         ,          , and      . 2.4. Liveness Analysis of    Models 53 5.                 . ¾ It is easy to see that this definition is equivalent to the one presented previously in a constructive way. 2.4 Liveness Analysis of Ë  ÈÊ Models One of the desirable properties of the systems we are considering is that the processing of each part, once started, will finish. When talking about concurrent systems this is related to the deadlock freeness property. Since each started processing will terminate, the initial state of the system (the idle state) can be reached from any reachable state. Moreover, since only acceptable initial markings are considered (adequate initial states from which every transition is fireable), it is clear that the behavioral property needed from the Petri net point of view is liveness. Liveness in systems modeled by means of    nets also implies that, provided that new raw materials arrive, their processing will be also possible. In this section some important behavioral properties of    nets are presented. Having to deal with this class of nets, one would feel inclined to use similar results to the ones introduced in previous analogous approaches [ECM95, TGVCE98]. In [ECM95] the    class was presented and for it, empty siphons were used to detect deadlock problems. Another approach based on siphons for a class of ordinary nets are process nets with resources ([JXH00, PR01].) An alternative approach, based on transforming a weighted Petri net in an ordinary one (at least for the arcs that are output of the places of the net) and using the empty siphon characterization [LR96, IMA02]. However, since most of the previous work are applied tonets whose arc weights are always one, they use the same liveness characterization as in [ECM95]: a deadlock situation is related to some empty siphon. Since the structure of    nets is similar to the    , the question is whether siphons are useful in order to characterize deadlock problems or not.    nets, and in general, nets with weighted arcs present some differences when dealing with deadlock problems: as it will be shown, it is possible to have deadlock problems with no related empty siphons. This introduces a new dimension: the distribution of tokens in places related with the siphons must be considered. Several definitions have been introduced in the literature studying siphons 54 2. The    class: definition and properties P1_1 P1_2 P2_1 P2_2 R1 R2 P1_3 P1_0 P2_0 T7 T6 T5 T4 T1 T2 T3 _3 _2 _5 Figure 2.6: A    with deadlock problems. (structural component) and the token distribution in places related to them (behavioral information) to relate deadlock situations and siphons in weighted Petri nets:  In [Bra83] the concept of empty siphon in ordinary Petri nets is extended to the notion of insufficiently marked siphon: a siphon,  , is insufficiently marked at marking  if                           . This definition extends one of the most important behaviorral properties based on siphons (a total deadlock in an ordinary Petri net implies an empty siphon, while a total deadlock in a weighted Petri net implies an insufficiently marked siphon.) This approach seemed promising when moving from    (if an active process cannot terminate, an empty siphon is reachable) to    . However, this property is not enough. Let us take a look at the    in Figure 2.6: marking                is reachable; for it, transitions   and   are dead, but no siphon insufficiently marked exists.  [BPP96, AE98] used siphons to deal with deadlock problems in S–RAS, giving a sufficient condition to ensure that no deadlock can occur. The objective 2.4. Liveness Analysis of    Models 55 is to keep all the minimal siphons “marked”. Asiphon  is said to be marked if and only if                              , that is, a siphon is “marked” if there exists a place enabling all of its output transitions. As it will be shown later this property is too strong, and reducing the requirements more permissive approaches can be obtained.  [TCE99] presented a necessary condition for deadlock situations in terms of siphons for    nets. A deadlock prevention algorithm was proposed controlling the system so that the necessary condition cannot hold in the controlled system, obtaining live controlled systems. The proposed solution was similar to the one presented here but it has some inefficiencies that have been removed here.  In [PR01] the idea of resource–induced deadly marked siphons for    nets is proposed: a siphon  is a resource–induced deadly marked siphon at         when each transition     is disabled by some place belonging to  . In order to forbid deadlock problems no resource–induced deadly marked siphon should be allowed. They also presented a liveness characterization for    nets based on siphons but they do not use it for deadlock prevention. In the rest of the chapter we are going to present a set of liveness characterizations for    nets. The first one (Theorem 26) does not use siphons, but concentrates on states where circular wait situations appear. The second one (Theorem 28), obtained from the first one, characterizes deadlock problems in terms of siphons and some related markings. Finally, the last one (Theorem 32) is also based on siphons, but establishes in a more clear way how deadlocked processes can be located around siphon components. We will see that all the proposed characterizations are equivalent and also equivalent to the one proposed in [PR01]. The main advantage of the one proposed in Theorem 32 is that, as shown in the next chapter, it induces an efficient way of preventing deadlocks in    nets. Let us present a lemma proving that the activation of a new process at a given reachable marking cannot increment the number of available resources. Later, a liveness characterization for    nets (Theorem 26) will be introduced. Lemma 25 Let      ,  =             , be a marked    . Let            such that                 . Then,                 . 56 2. The    class: definition and properties Proof Let     . The invariant relation induced by   and the fact that                   allows us to write                                                      ¾ The following theorem presents a liveness characterization for    nets in terms of a property of circular waits. Theorem 26 Let      ,  =             , be a marked    . The system is non–live if and only if there exists a marking         such that the set of  –process–enabled transitions is non–empty and each one of these transitions is  –resource–disabled. Proof  )If      is non–live, there exists at least a transition,  , that is dead at a marking          . Let         obtained by moving forward all the active processes (firing transitions of      ) until no process enabled transition can fire. At this marking,        holds (i.e. there are some active processes and, in consequence, some  –process–enabled transitions.) On the contrary,     , and then   could be reached from   . But, since the system is well defined, any minimal T–Semiflow containing  would be fireable from   (Lemma 7 and Proposition 11) and, in consequence, a firing sequence containing  would exist from   , which is a contradiction with  being dead at   . Therefore, any transition         for any     is  –process–enabled and  –resource–disabled.  ) Let         for     . In order to fire  some more tokens are needed in some places belonging to      . Since  –active processes cannot progress, the only way to change the marking of such resources is by moving other processes, and the only possibility is to activate some idle processes. Let               denote the set of  –process–enabled transitions and              denote the set of state places with some  –active-process,and let      . We are going to prove, by induction over the length of  that: 1.       . 2.                . Doing so, and since        , it can be deduced that                   . Taking into account Lemma 25,                 . Therefore, no transition of  can be  ’–resource enabled. 2.4. Liveness Analysis of    Models 57  Case    . Since no transition of  is enabled at  , then      and then,    . On the other hand, if     ,               .If     , let           . In this case          and the equality holds for the marking of the rest of places belonging to  . In both cases, point 2 holds.  General case.           , where      verify the induction hypothesis:        and                . Applying Lemma 25 (taking also into account that        ) we can conclude that    , and point 1 holds. Moreover, the fact that    implies that                      , and we can conclude. ¾ In the example of Figure 2.6, at marking                   ,   is the only   –process–enabled transition, which is disabled by   . Therefore, it is dead. Resource   has only one token at   ,so   is a   –resource–disabled transition. Note 27 A marking         verifying the conditions of Theorem 26 will be called a deadlocked marking. The term bad marking will also be used. ¾ Theorem 26 relates non–liveness to the existence of a marking where active processes are blocked. Their output transitions need resources that are not available. These needed resources cannot be generated (released by the corresponding processes) by the system (the transitions are dead) because there exist a set of circular waits between the blocked processes. This concept of circular waits can be captured by the existence of a siphon (in Petri Net terms) whose resource places are the places preventing the firing of the process–enabled transitions. The following theorem shows that, when a bad marking as in Theorem 26 exists, a related siphon can be constructed; the reverse is also true. This establishes the bridge between behavior and model structure. Theorem 28 Let      ,  =             , be a marked    . The net is non–live if, and only if, there exists a marking         , and a siphon  such that        and the firing of each  –process–enabled transition is prevented by a set of resource places belonging to  . Moreover, the siphon  is such that: 1.                    such that          and               ; 64 2. The    class: definition and properties Theorem 32 Let      ,  =             , be a marked    . The net is non–live if, and only if, there exists a siphon  , and a marking          , such that: 1.         . 2.          . 3.       such that        , the firing of each     is prevented by a set of resource places belonging to  . Proof  ) According to Theorem 28, the net is non–live if, and only if, there exists a marking         , with        , and a siphon        such that the firing of each  –process–enabled transition is prevented by a set of resource places belonging to  .Now, we are going to prove that there exists a marking   that characterizes the non–liveness of the net system being all the active processes in the set of thieves of   , i.e.          . Since      , and      ,         (if       ,           ; then, no process is using resources of   (then,                ), while   is preventing the firing of some  –process–enabled transitions which is a contradiction with the fact of being   an acceptable initial marking.) Let us now consider the following partition of the set of  –marked state places:                                            Notice that:  The first subset is non–empty.  No process of the second subset uses resources of   . Now, we can apply Proposition 31 to each one of the processes of the second subset. In this way we will obtain a marking   such that:                   ;                     ;                       ; (there are no active processes out of the siphon related state places.)       ,                            (the active processes in state places not related to the siphon are at the corresponding idle state.) 2.5. Conclusions 65 Then,   verifies                ; since the set of   –process–enabled transitions is a subset of the set of  –process–enabled transitions and the resources of   were preventingthe firing of the  –process–enabledtransitions of thefirst subset, and                , clearly each   –process–enabled transition is still disabled at   by resources belonging to   .  ) Since         and       such that        , the firing of each     is prevented by a set of resource places belonging to  ,   and  verify conditions of Theorem 26, which is sufficient to conclude that      is non–live. ¾ This liveness characterization directly relates bad markings with system states in which all the active processes stay in thief places of a bad siphon. This will be specially useful when trying to control the system in order to ensure a live behaviour since the potencial problems are located around siphons. This aspect will be developed in the following chapter. 2.5 Conclusions In this chapter, the class of    nets has been introduced. The syntactic characteristics of the nets of such class are derived from the domain to which they are devoted: sequential resource allocation systems, in which a set of sequential processes must share a set of (conservative) resources. It has been shown how the model properties (Petri net properties, in this case) map into domain characteristics. In this sense, token conservation laws induced by (minimal) P–Semiflows correspond to the conservative nature of system resources or to the closed structure of the processes running in the system. On the other side, executable (minimal) T– Semiflows correspond to complete possible executions of the involved processes. Using this well defined mapping into model and system structures, the deadlock problem analysis has been studied from the Petri net model structural point of view, leading to a complete liveness characterization. From the domain point of view, the    nets allowed to remove some of the restrictions (syntactic from the Petri net point of view, but related to the number and variety of real systems able to deal with, from the application point of view) imposed by previous classes of Petri net models devoted to the analysis and control of S–RAS. In this sense, the only constraint still maintained in    nets is that no inner cycle is allowed in the behavior of a process. In the second part of the chapter a liveness study for    systems has been presented, showing a characterization for deadlock problems. This characterization is based on the existence of circular waits (involving resource places) related to the 66 2. The    class: definition and properties existence of problematic system states, re-establishing a classical result related to deadlock situations for the class of models considered here. Later, the relation of problematic markings with some special siphons has been shown, providing a way to study these bad markings in terms of some net siphons. As it will be shown in the next chapter, the siphon–based characterizations can be used to prevent deadlock problems. Chapter 3 Deadlock Prevention Policies for Ë  ÈÊ nets Abstract One of the advantages of the use of formal models as    is that the model can be used both to analyze the system behavior, and to control it. In the present chapter we are going to use the liveness characterizations introduced in Chapter 2 in order to prevent deadlock problems. 3.1 Introduction The objective of the present chapter is to concentrate on how to add control to the system to ensure that no deadlock situations can happen. For this task the departure state is promising: the system is modeled by means of a    , and for this class some liveness characterizations have been introduced in the previous chapter. In consequence, we are going to concentrate on how to use these characterizations to reach the objective. We need to ensure not only that no deadlock will be reachable but also that the resulting system is as permissive as possible. Permissiveness here is related to the number of reachable states in the controlled system. The quality (based on the permissiveness) of a prevention approach relies in two main aspects:  A good identification (a characterization if possible) of deadlock related states. 68 3. Deadlock Prevention Policies for    nets  A good control method able to forbid the deadlock related states (without forbidding too many of the good ones). Considering the first point, most of the previously proposed methods lack of a full liveness characterization, providing only necessary conditions. Then, the prevention approach for them will need to ensure that such conditions cannot occur. This is the case of [LT79, ECM95, TM95, KTJK97, TGVCE98, AE98, TE99, GL01]. With respect to the second one, the proposed methods usually apply the control at the level of process activation; that is, if the activation of an idle process could lead to deadlock, such activation is forbidden. This kind of prevention is easy to implement, but it usually gives controlled systems with poor use of the system resources ([IM80, Sin89b]). From this point of view the objective would be to look for a way to control the system in such a way that only deadlock related states are forbidden. In this way, the undesired states would be eliminated, while allowing as many concurrency as possible in the execution of processes in the controlled system. As it will be shown, the key issue will be to look for “bad states” that are “around” the siphons of the Petri net model, obtaining quite good solutions. 3.2 What a maximally permissive control policy should do? The final objective of a deadlock prevention policy is to constrain the allowable firing sequences so that only non–deadlocked states are reachable. A way of doing that consists in the addition of new preconditions to the firing of transitions by means of new places and arcs, with an adequate initial marking. Let us give some intuition about this using the reachability graph of the    of Figure 2.6 (page 54), which is depicted in Figure 3.1. The reachable states can be classified into three categories: 1. The first one (type 1) contains those markings from which   is reachable. These markings are not involved in deadlock problems (the shadowed states in Figure 3.1). 2. The second class (type 2) is composed of those markings that are not  – deadlocked for any siphon, and such that   is not reachable from them. 3. Finally, the third class (type 3) is composed of those markings that are  – deadlocked for some siphon  (depicted as black boxes in the Figure). 3.2. What a maximally permissive control policy should do? 69 daVinci V2.1 #2:P1_1+5R2 #1:R1+5R2 Markings of type 2 Markings of type 3 #10:P1_2+P2_1+R1+2R2 #9:P1_1+P1_2+3R2 #18:P1_2+P2_2+3R2 #16:P1_1+P1_2+P2_1+2R2 #15:2P1_2+R1+R2 #23:2P1_2+P2_1+R1 #31:2P1_2+P2_2+R2 #22:P1_1+2P1_2+R2 #4:P1_2+R1+3R2 #7:P2_2+5R2 #27:P2_2+P1_3 #8:R1+P1_3 #14:P1_1+P1_3#13:P2_1+P2_2+4R2 #21:2P2_1+P2_2+3R2 #3:P2_1+R1+4R2 #29:3P2_1+P2_2+2R2 #6:2P2_1+R1+3R2 #5:P1_1+P2_1+4R2 #12:3P2_1+R1+2R2 #11:P1_1+2P2_1+3R2 #20:4P2_1+R1+R2 #19:P1_1+3P2_1+2R2 #17:P1_2+2P2_1+R1+R2 #28:P1_1+4P2_1+R2 #25:P1_2+3P2_1+R1 #26:P1_2+P2_1+P2_2+2R2 #24:P1_1+P1_2+2P2_1+R2 #33:P1_2+2P2_1+P2_2+R2 #35:P1_2+3P2_1+P2_2 #30:P1_1+2P1_2+P2_1 #34:2P1_2+P2_1+P2_2 #32:P1_1+P1_2+3P2_1 Markings of type 1 Figure 3.1: Reachability graph of the net of Figure 2.6 (marking of the idle places not shown for the sake of clarity) 70 3. Deadlock Prevention Policies for    nets P1_0 P2_1 P1_1 P1_2 P2_2 R1 R2 P2_0 T1 T2 T3 T4 T5 T6 Figure 3.2:    net that can reach a deadlocked marking For example, marking                is a   –deadlocked marking, where the siphon is               , while the marking                   is not  –deadlocked, for any siphon  . Nevertheless, from marking  we will reach in an inevitable way a  –deadlocked marking (both successor markings  and  are  –deadlocked). Let us concentrate on how a bad situation can be controlled and all the related bad markings forbidden. Let us now consider the net in Figure 3.2. Its reachability graph is depicted in Figure 3.3. There, marking            is a deadlock. This deadlock occurs because the process in place   is waiting for the resource  which is being held by process in place   ; this process is waiting for resource  that is being held by process in place   . In this case, it is easy to modify the system in such a way that the marking   is not reachable anymore: a place,   (Figure 3.4), establishing a mutual exclusion between places   and   in such a way that they cannot be simultaneously marked solves the problem. This place will be called control place. While in this example the addition of just one place is enough to have a controlled system, this will not be always the case. For other systems, more control places will be needed. This way of adding control is related to the generalized mutual exclusion constraints (GMEC) introduced in [GDS92]. The problem with adding control for each deadlocked state is that too many control places could be needed: in the worst case, one for each marking of types one and two. Fortunately, Theorems 28 and 32 relate bad states with some special 3.2. What a maximally permissive control policy should do? 71 daVinci V2.1 #7:P2_1+P2_2 #4:P2_2+R2 #5:P1_1+P2_1 #2:P2_1+R1 #8:P1_1+P1_2 #6:P1_2+R1 #3:P1_1+R2 #1:R1+R2 Figure 3.3: Reachability graph of net of Figure 3.2 (the markings of the idle state places is not shown for the sake of brevity). siphons, allowing to establish a middle point between the control based exclusively on the information provided by deadlocked markings and the control based on process activation. Another important question is the way in which bad markings are forbidden; in the example it is obvious that the addition of   strictly avoids the problematic marking; the general case will be much more complicated. The addition of a place and its corresponding arcs introduces a new row in the incidence matrix, that is, a linear restriction. We are interested in control policies based on the addition of Petri net components: places and arcs (which we will use to forbid some bad states). The main reason for this is that the control via the addition of Petri net elements will allow us the study of the new system in the same terms of the original one. In consequence, the approach proposed in the following sections corresponds to the addition of a set of linear restrictions to the initial system, “cutting” a set of markings of the reachability set. As an example of this, notice that the net of Figure 3.4, resulting from the addition of the control place to the net in Figure 3.2 is a new    net: the added place   follows the restrictions about resource places. The use of linear restrictions has a drawback: in some cases they forbid not only the desired bad states but also some good ones. This fact has been previously shown in [Val99, GVTCE00]. A maximally permissive control policy should prevent all the bad markings (types 2 and 3), forbidding no good markings. Forbidding deadlocked markings by means of the addition of linear restrictions can be done according to the following two main perspectives:  First approach: to cut as few states as possible; that is, once the states that 72 3. Deadlock Prevention Policies for    nets P1_0 P2_1 P1_1 P1_2 P2_2 R1 R2 P2_0 PC_1 T1 T2 T3 T4 T5 T6 Figure 3.4: Controlled net are  –deadlocked have been characterized, a linear restriction can be added that avoids just these bad states. The problem with this approach is that it is not able to deal with the markings of type three (remember that they are not  –deadlocked). Then, once the original system has been controlled, a new system is obtained (the old one plus a linear restriction) that can have deadlock problems: further work is needed to obtain a “good” one. For this reason this approach will be called in several steps. This approach is local, oriented to the control of the transitions closely related to bad siphons. In this way, new linear restrictions can be added in consecutive iterations in order to get a live system.  Second approach: to cut ‘enough’ states to avoid all the problems; that is, for each siphon that can have  –deadlocked markings, the set of linear restrictions to be added can be computed in such a way that neither  –deadlocked markings nor markings that in an inevitable way conduct to  –deadlocked ones can be reached. This way of controlling is usually closely related to the idea of process activation. The objective is to cut all the  –deadlocked markings (markings of type 2), all the ones of type 3 and, perhaps, some of the good ones (without introducing new problems). We can expect that this way of controlling the system will be more restrictive but more simple and faster to compute. 3.2. What a maximally permissive control policy should do? 73 Let us comment on the main previous prevention solutions based on the addition of linear restrictions.  In [LT79], a resource–oriented approach is considered: for each resource, as many control places as output transitions are added (except for the last one). They control the system in such a way that once a part starts requesting tokens from a given resource place (that is, the firing of one of its output transitions occurs), there will be enough available tokens in the resource to grant all the future requests and terminate. This is one of the first control policies that proposed the modification of existing nets with the addition of linear restrictions in order to get live models. The main drawbacks are that it is based on the control of each resource and that it is not easy to generalize the policy to deal with systems with several different concurrent processes.  In [ECM95] the control policy is based on the detection of deadlock problems by means of siphons. It is also an approach in one step. The way to apply the control was to add a control place for each minimal siphon constraining the system evolution in such a way that each part entering into the system makes a ‘reservation’ of enough copies of the resources related to the siphon to be sure that it will not reach an empty state. There are some further evolutions of this control policy for more general classes of nets in [TM95, TGVCE98, TE99].  In [BCZ97, AE98] the class of nets is similar to the one used here. It is an approach in several steps. The control is based on siphons, and the way to add the control places (one for each siphon) has similarities to the one used in [LT79], but considering the siphon as a whole; that is, control place arcs reproduce the total number of tokens that the process has withdrawn from the resource places belonging to the siphon. The method guarantees that at each reachable marking there is always a place in the siphon with enough tokens to fire any of its output transitions.  In [PR01] the approach in one step is followed. It is based on the division of the processing paths in zones (neighborhoods) defined by means of the imposition of a partial order in the set of resources. The authors claim that it is very efficient and the policy is proposed as an avoidance policy; however, it can be implemented as a prevention one. The proposed solution is too constraining. 80 3. Deadlock Prevention Policies for    nets The addition of    generates the following marking invariant:                                                This P–Semiflow is forbidding the previously cited marking  . The reason is that, at  ,                              In the same way, any other   –deadlocked markings is also forbidden. 2. When considering the processes point of view, we will need to ensure that there are not “too many” active processes in     . For this, place    can be added, in such a way that its marking is equal to the number of such active processes. This is a more simple approach, since counting the number of tokens that enter in relevant places is quite easy to implement. The initial marking for this place will be       , generating an invariant relation similar to the one shown in the previous case, ensuring that no more than this number of parts can enter     . In the example, since      , we want to impose that for each marking,      ¾       . To do that, place    is added with marking  . (Definition 43 establishes how this place is added.) This place generates the following new marking invariant:                                         This P–Semiflow is forbidding marking  . This is so because at  ,                   Of course, it also forbids any other   –deadlocked marking. 3.3. An iterative control policy 81 Given a siphon,   , two possible control places have been suggested. Obviously, just one of them is needed for each bad siphon. Let us present some final remarks to this intuitive introduction:  A control place (using any of the two alternative approaches) is computed from a given bad siphon. Then, to control the whole system, a first direct solution would consist in computing all the bad siphons and then to control each one of them. This can be very time consuming. A different approach is going to be used: a bad siphon is computed and controlled, then a second one, and so on. In general, this approach will reach a controlled system in a faster way, since it is possible that controlling one bad siphon, other siphons become also controlled at the same time.  Controlling all the bad siphons of the original net can be insufficient to ensure a live behavior. As previously stated, markings of type 2 can be the source of new problems. From the structure point of view this fact will be shown by (new) bad siphons involving some of the added control places. Luckily, each time a control place is added, the controlled net also belongs to    class. This allows to follow an iterative approach. Moreover, since the addition of a control place forbids some (potentially) reachable marking and the set of (potentially) reachable markings is finite, it is ensured that the iterative method terminates.  Two alternative ways of controlling a bad siphon have been presented. They both are adequate to control a given siphon, but they are not equivalent, since the set of reachable markings (after the addition of the control place) can be different. Let us consider again  .If   is controlled using the resource point of view, the obtained system can reach 138 states. If it is controlled using the process point of view, only 98 states are reachable in the resulting system.  The method starts computing and controlling a bad siphon, using an integer linear programming problem. If such problem has no solution, the system is live and no control is needed. This is an important advantage of the proposed deadlock prevention method, when it is compared with any deadlock avoidance method. In the following all these ideas will be presented in a formal way. 82 3. Deadlock Prevention Policies for    nets 3.3.2 Computation of deadlocked markings The following proposition relates liveness with the existence of a solution for the presented system of inequalities. The systems is a linear representation of a bad marking given a known bad siphon introduced in the statement of Theorem 28. Proposition 33 Let      ,  =             , be a marked    . The net is non–live if and only if there exist a siphon  and a marking         such that the following set of inequalities has, at least, one solution:                                                                being                         !                         !                     !                                                                                                      (3.1) where     denotes the structural bound of  [CS91]. Proof First of all, let us make some comments about the variables used in these inequalities. 1. For each        ,   indicates whether  is  –process–enabledor not. It follows immediately from the following facts:  since       ,       if, and only if,            , which is equivalent to state that    (remember that        )      if, and only if,    2. Let     , and         . Let us prove that   indicates whether  is enabled by  at  :  If  is enabled by  at  (          ),            and                           ; therefore,   must be  . 3.3. An iterative control policy 83  If  is not enabled by  (          ),            and                         ; then,   must be  . 3. If        , and         ,    (that is, resources not belonging to the siphon enable their output transitions). 4. The system of inequalities without the last one has always a solution, and the value of variables   ,   is determined only by  . Therefore, the existence of a solution of the complete system depends on the last inequality. Two cases can be distinguished:  If        is not  –process–enabled,    and the inequality for  is trivially fulfilled, because                  .  If        is  –process–enabled,     and the inequality becomes                   . Therefore, there is a solution if, and only if,         such that  is not enabled by  . Let us use these points in order to show the truth of the Theorem.   ) If the net is non–live, Theorem 28 ensures that there exists a marking         , with        , and a siphon  such that the firing of each  –process– enabled transition is prevented by a set of resource places belonging to  . This means that there exist places with    . Since each one of these transitions is prevented by a set of resource places belonging to  , there exists        such that          , and then,    . In consequence, for these transitions,                       , is true.   ) Let us consider  ,         , and the set of variables          and              , solutions of the set of inequalities. Since        , let     such that       . For each     ,    , and then,                               . Therefore, there must exist        such that    which means that  is  –resource disabled. Moreover,     since for each        , each      ,     . Therefore, any  –process enabled transition is disabled by a resource place belonging to   and Theorem 28 allows us to conclude. ¾ The existing bad siphons and their related bad markings need to be computed in order to control the system. Our next goal is to reformulate the above system of inequalities in order to be able to obtain a bad siphon, together with its related bad markings. The characterization presented in Theorem 28 allows a simple reformulation of these equations. To do that, an algebraic characterization of siphon is necessary. In [AT85, Sil85] a characterization of this kind is given for traps. It is straightforward to adapt it to the case of siphons. 84 3. Deadlock Prevention Policies for    nets The result establishes that each solution of the following set of inequalities: "        "   "                 is a siphon (whose components are those places such that the value of variable "  equal to  ). As it will become clear later, this result is not adequate in this original form, and it has to be transformed into an equivalent form using negated logic (this approach is similar to the one proposed in [Sil85] and also in [XJ99].) A siphon is the set of places whose associated variables in the following set of inequalities is 0: "        "        "                 In order to compute a bad siphon, conditions of Proposition 33 can be completed by the addition of the following equations:  A set of constraints representing the siphon, "        "        "                  A restriction that avoids the whole net as solution:       ¼ "          A set of restrictions relating resource places that are avoiding the firing of a process–enabled transition and the siphon. For this,   ,   , as in previous proposition are used together with the new introduced variables. Let us show how this extension can be used to compute bad siphons and related bad markings. Proposition 34 Let      ,  =             , be a marked    . The net is non–live if and only if there exist a siphon  and a marking         such that the system of inequalities (3.2) has a solution with            "    : 3.3. An iterative control policy 85                                                                           "        "             ¼ "                         being                         !                         !     "                  !               "                                         "                                             (3.2) Proof The truth of this proposition is immediate taking into account Proposition 33 and the following considerations: 1. The two first inequalities, and the fact that        , define a non–empty siphon as stated before. Let  be such siphon. 2. The inequality related to the marking of   is the same as in Proposition 33. 3. The inequalities related to   are the same as in Proposition 33. Remember that    if, and only if,  is  –process–enabled. 4. The inequalities involving   are:  The same as in Proposition 33 when    ; that is, if resource  belongs to the siphon  . In this case, restriction      becomes     , which is redundant.  If resource     does not belong to  ,(    ), these inequalities make   to be  . They become: –     , with    –     , with                       , and 86 3. Deadlock Prevention Policies for    nets –     These inequalities always have a unique solution,     . (Notice that in Proposition 33,   was explicitly made equal to  for        , because the siphon was known a priori.) 5. The last inequality is the same as in Proposition 33, and its meaning is exactly the same (see the proof of the previous proposition for details). ¾ The characterization introduced in this proposition is not directly applicable to control the system, since a reachable marking is needed and we do not want to use reachable markings (our goal is to avoid the enumeration of the set of reachable markings). Therefore, we are going to propose an alternative approach using the set of potentially reachable markings (markings obtained as solutions of the state equation). Proposition 35 Let      ,  =             , be a marked    .If net is non–live, there exists a marking         , with        , and a siphon  such that the following system of inequalities has, at least, one solution with            "    :                    ZZ      # $    (3.3) ¾ This proposition does not provide a complete characterization (as it was the case in Proposition 34). It only provides a necessary condition for deadlock. The reason is the existence of spurious solutions: markings that are solution of the state equation but are not reachable. This is not a problem when the objective is to control the system looking for a live system: the only consequence can be that control places also forbid some marking which are not reachable. In this way, a system with more control than needed can be obtained which will be, in any case, live.Finally, it must also be pointed out that, when possible, adding non necessary or redundant control should be avoided, since some good markings can be eliminated together with the bad ones, which is not desirable. 3.3. An iterative control policy 87 Note 36 A siphon and the corresponding marking fulfilling conditions in Proposition 35 will be called a potential bad siphon and a potential  –deadlocked marking, respectively. However, and for the sake of simplicity, they will be called bad siphon and  –deadlocked marking. ¾ The approach we are going to propose does not obtain all the solutions of the system of Proposition 35. The considered method will obtain a bad siphon, for later controlling it by means of the addition of the adequate place, and iteratively continue computing and controlling new bad siphons. The reason for this is clear: the added control will modify the system behavior and some bad markings associated to another siphons can be forbidden (also some good states). The obtained system will have different deadlock problems than the original one. To do that we are going to transform the system of equations into another one that will obtain just one siphon as solution. This raises the question of how to decide which siphon to control. The proposed approach selects the siphon with a minimal number of places in the hope that controlling first smaller siphons may help to avoid the control of the bigger ones. The following corollary introduces the problem. Corollary 37 Let      ,  =             , be a marked    .If the net is non–live, then there exist a siphon  and a marking         such that the following set of inequalities has, at at least, one solution with            "    :  maximize       ¼ "  s.t. #$    (3.4) ¾ The solution of this problem is a bad siphon,  , and a  –deadlocked marking,  . No special consideration has been done about the  –deadlocked marking associated to the siphon, while some restrictions about minimality have been done for  . Nevertheless, we do not want to avoid only just this  –deadlocked marking but also all the deadlocked markings related to the siphon. In consequence, a new problem needs to be solved: once the siphon is known, which are the deadlocked markings for it? This question has a clear theoretical interest but, if we look at it 88 3. Deadlock Prevention Policies for    nets carefully, we discover that its practical application can be very expensive, depending on the number of such markings. The approach considered here is to compute some selected ‘representative’ markings that can be used to avoid all the related  –deadlocked markings. This will be accomplished here in two alternative ways, as presented in the intuitive introduction:  Looking at the maximal number of resources available at  –deadlocked markings.  Looking at the minimal number of active processes at  –deadlocked markings. For this, the characterization of Theorem 32 (page 64) and Proposition 31 (page 62) will be used, that allows us concentrate on different markings, once a bad siphon is known. In this sense, it will be useful to return to Proposition 33 (page 33). The equations presented there were constructed supposing that the siphon was known. Let us use them in order to construct the associated  – restrictions. The restriction           from Theorem 32 can be added since the siphon is now known. Definition 38 Let      ,  =             , be a marked    . Let  be a bad siphon. The set of  –restrictions is:                          ZZ              # $    (3.5) ¾ These restrictions represent the conditions related to the ones shown in Theorem 32 once the bad siphon is known. With them, we can now select the adequate bad markings. Definition 39 Let      ,  =             , be a marked    . Let  be a bad siphon,    and    are defined as follows:          maximize          s.t. restrictions    3.3. An iterative control policy 89          minimize          s.t. restrictions    ¾ Note 40 These two problems are, in some way, equivalent: either both have solution or none of them has solution: they search for deadlocked markings, concentrating on different points of view. That is, while    looks at the number of tokens in   at deadlocked markings,    looks at the number of active processes inplaces belonging to    that are “stealing” tokens from  at deadlocked markings. When referring to a particular  problem of the ones presented in Definition 39,     or     will be used. When referring to any of them    will be used. ¾ The way to control these systems in order to avoid deadlock problems is based on the addition of control places, as sketched in the intuitive introduction. Let us present some terminology to deal with this. Note 41 Once a bad siphon  has been computed, it can be controlled using     or     in order to prevent  –deadlocked markings in two different ways:  Adding one control place ensuring that processes in    are not using more resources than           . If this is the adopted approach (called the  –resource approach), the system will be said to be  –resource–controlled.  Adding a control place ensuring that there will be no more than      active process in places belonging to    . If this is the adopted approach (called the  –process approach), the system will be said to be  –process– controlled. If the adopted method is not specified, the resulting system will be said to be  – controlled. ¾ Let us now present a basic property that will be needed later in order to see that the added control is correct. The result is related to the minimal number of active processes at a deadlocked state. 96 3. Deadlock Prevention Policies for    nets P1_1 P1_2 P2_1 P2_2 P3_1 P3_2 R1 R2 T1 T2 T3 T4 T5 T6 T7 T8 T9 _2 _2 _2 _2 Figure 3.8: A (partial)    with a bad siphon that is no controllable using the  –resource approach (idle places have been omitted for the sake of clarity).  If   is a  –process place,                                          In consequence, no  –deadlocked marking can exists in           , since at least one  –deadlocked marking existed in       ¾ In our experience, the use of the  –resource approach gives more permissive controlled systems. In consequence, the approach we are going to propose will try to first apply the  –resource–control; if the resulting initial marking is not acceptable, then apply the  –process–control. Notice that no potential reachable marking in           can be  – deadlocked, which implies the same property for any reachable marking, since                      . 3.4 Preventing deadlock problems in Ë  ÈÊ We have concentrated on the prevention of the bad markings related to a given bad siphon. An iterative algorithm is going to be proposed to control the whole system. It is structured in the following steps: 3.4. Preventing deadlock problems in    97 daVinci V2.1 #12:2P1_1+P2_1+R2 Markings of type 1 Markings of type 2 Markings of type 3 #16:2P1_2 #17:P1_1+P1_2+P2_1 #10:P1_1+P1_2+R2 #18:2P1_1+2P2_1 #5:2P1_1+2R2 #20:2P1_1+P1_3 #15:P1_1+R1+P1_3 #9:2R1+P1_3 #11:P1_2+P2_1+R1 #4:P1_2+R1+R2 #13:P1_1+2P2_1+R1 #6:P1_1+P2_1+R1+R2 #2:P1_1+R1+2R2 #19:2P2_1+P2_2 #14:P2_1+P2_2+R2 #7:2P2_1+2R1 #3:P2_1+2R1+R2 #1:2R1+2R2 #8:P2_2+2R2 Figure 3.9: Reachability graph of the first net of Figure 3.10 98 3. Deadlock Prevention Policies for    nets Algorithm 3.1 Function controlNet(In      : a marked    )Return        –—Pre: TRUE –—Post:        is a live    obtained controlling      Begin        :=      Repeat Compute a bad siphon for        ,  , using system (3.4) If   , solution Then Compute    as stated in Definition 39 If    is acceptable Then Add the corresponding resource–control–place as stated in Definition. 43 Else Compute    as stated in Def. 39 Add the corresponding process–control–place as stated in Definition. 43 End If End If Until No new control place is added End 1. Compute a bad siphon. 2. Compute    .  If the corresponding control place has an acceptable marking, go to the following step.  If not, compute    . 3. Add the control place. 4. Go to the first step, taking as input the partially controlled system, until no bad siphons exist. Algorithm 3.1 corresponds to a more detailed implementation of these ideas. The following theorem proves the correctness of the proposed algorithm. Theorem 47 Let      ,  =             , be a marked    3.4. Preventing deadlock problems in    99  The Algorithm 3.1 applied to      terminates.  The resulting controlled system,        , is live. Proof  Termination: it is a direct consequence of the following facts. 1. If      is a marked    ,         is finite. 2. When a siphon is controlled, the resulting system is a    (Lemma 45). 3. The addition of a control place strictly decreases the number of potentially reachable states of the controlled system (Lemma 46).  When the algorithm terminates the controlled net system        is a    with an acceptable initial marking (by Lemma 45) and it has no bad siphon. Then, no marking           can be  –deadlocked for any bad siphon and then, no marking            can have a dead transition (Theorem 28). Moreover, since the initial marking is acceptable,               . ¾ Example 3 Let us use the    in Figure 3.10 to see how the Algorithm 3.1 works. In order to see the effect of the control policy, its reachability graph is depicted in Figure 3.9. The figure shows the deadlocked states (#16, #17, #18), the ones that lead in an inevitable way to them (#6, #11, #12, #13), and the ones a maximally permissive control policy should left (the rest). Notice that the original system has 20 reachable markings from which the policy should left 13. The markings forbidden by each restriction are shown in the figure by means of lines labeled with the name of the control place: the control place forbids the markings under the corresponding line.  Iteration 1: The first bad siphon computed is             . Solving the associated ILPP problem,      , which generates the control place  whose associated invariant is:                     It has an acceptable initial marking and it is added to the system. 100 3. Deadlock Prevention Policies for    nets P1_1 P1_2 P2_1 P2_2 R1 R2 P1_3 P1_0 100 P2_0 100 T7 T6 T5 T4 T1 T2 T3 _2 _2 _2 Figure 3.10: A    net. 3.5. A comparison 101  Iteration 2: System 3.4 obtains the siphon               . Solving the associated ILPP problems,     , which generates the control place  whose associated invariant is:                          It has an acceptable initial marking and it is added to the system.  Iteration 3: A new siphon obtained using System 3.4 is                . Solving the associated ILPP problems,     , which generates the control place  whose associated invariant is:                     It has an acceptable initial marking and it is added to the system.  Iteration 4: The next siphon obtained solving System 3.4 is                . Solving the associated ILPP problems,      , which generates the control place  whose associated invariant is:                         It has an acceptable initial marking and it is added to the system. No new bad siphon appears and the algorithm terminates. This system has 10 reachable states. To control the original    , four siphons have been computed and four new places have been added. In Figure 3.11 we can see the resulting    . In Figure 3.12 we can see the effect of the four control places added. 3.5 A comparison This section introduces a set of empirical results in which a set of different control policies solve the problem of controlling a    net. The two versions of the control policy presented in this chapter (process-oriented and resource-oriented) are compared with two control policies able to deal with this general class of systems from a prevention point of view, have been implemented. These policies were introduced in [BCZ97], and in [EH93], respectively. 102 3. Deadlock Prevention Policies for    nets RCP2D P1_1 P1_2 P2_1 P2_2 R1 P1_3 P1_0 100 P2_0 10 0 RCP1D RCP3D RCP4D T7 T6 T5 T4 T1 T2 T3 _2 _2 _2 _2 _2 _2 _2 _2 0011 00 00 11 11 0 0 1 1 00 00 00 00 11 11 11 11 01 000 000 000 000 111 111 111 111 0011 000 000 111 111 01 0011 0000 0000 0000 1111 1111 1111 01 01 0 0 1 1 0 0 1 1 R2 Figure 3.11: The    net obtained by controlling the system in Figure 3.10 3.5. A comparison 103 daVinci V2.1 #16:2P1_2 #17:P1_1+P1_2+P2_1 #10:P1_1+P1_2+R2 #18:2P1_1+2P2_1 #12:2P1_1+P2_1+R2 #5:2P1_1+2R2 #20:2P1_1+P1_3 #15:P1_1+R1+P1_3 #9:2R1+P1_3 #11:P1_2+P2_1+R1 #4:P1_2+R1+R2 #13:P1_1+2P2_1+R1 #6:P1_1+P2_1+R1+R2 #2:P1_1+R1+2R2 #19:2P2_1+P2_2 #14:P2_1+P2_2+R2 #7:2P2_1+2R1 #8:P2_2+2R2 #3:P2_1+2R1+R2 #1:2R1+2R2 RCP2D RCP1D RCP3D RCP4D Figure 3.12: Reachability set of the net in Figure 3.10 . The states under the lines are prevented by the addition of the respective control places 104 3. Deadlock Prevention Policies for    nets [BCZ97] [EH93] D–resource D–process NM NB NMC NMC NMC NMC Net 3 471 427 94.38% 88.29% 100.00% 96.25% Net 4 140 124 91.94% 78.23% 79.03% 79.03% Net 5 47 42 100.00% 50.00% 100.00% 100.00% Net 6 151 143 100.00% 47.55% 100.00% 100.00% Net 7 1200 1149 94.34% 94.34% 94.34% 76.50% Net 8 696 653 90.66% 86.68% 90.96% 71.82% Table 3.3: Number of states and percentage of states left after application of control policies for the selected nets. The first one is based on siphons, and it adds restrictions to the net such that at each reachable marking it is guaranteed that there will exist a resource of each siphon enabling all its output transitions. The second one was originally introduced as an avoidance approach for a more restricted class of nets, but it can be implemented using the prevention point of view and can be applied to    . It is based on establishing a set of control points in the processes. When a process is going to leave one of these control points, it looks if the multi–set of resources it needs in order to reach one of its closest control points is available. In order to carry out the comparison, the methods have been run with a set of nets. The examples presented here have been chosen in order to show a variety of results, and cannot be considered as a true statistical sample. Table 3.3 shows the results corresponding to the nets in Figures 3.10,3.13(a)–3.13(f). The columns of the table are as follows. NM: is the number of states of the uncontrolled system; NB: is the number of states that a maximally permissive control policy would allow (that is, the number of elements of the strongly connected component that contains the initial marking); NMC: is the percentage states allowed by the control policy with respect to the number of states of the maximally permissive policy. We would like to point out the following remarks;  The new control policies proposed here have a good balance between computational cost and permissiveness. In fact, their behavior is as permissive as the approach in [BCZ97], but with a clear advantage: this methods requires, at each iteration, the computation and control of each minimal siphon, which implies the necessity of computing all the minimal siphons at each iteration. 3.5. A comparison 105 R2 R1 P2_0 25 P2_3 P2_2 P2_1 P1_0 25 P1_3 P1_2 P1_1 T8 T7 T6 T5T4 T3 T2 T1 _2 _3 _5 (a) Net 3 P2_21 P1_1 P1_2 P1_3 P2_3 P1_0 P2_0 P1_4 P2_11 P2_12 R2 P2_1 R1 T2_22 T2_21 T2_13 T2_11 T2_12 TO1_5 T1_4 TO2_4 T1_1 T1_3 T1_2 T12 _3 _3 _2 _5 _3 _3 _2 _2 _3 (b) Net 4 112 4. Deadlock avoidance policies for    nets. 4.1 Introduction In this chapter we propose a model that covers the previously introduced subclasses of S–RAS removing all the previously enumerated constraints (except, obviously, the one related to the conservation/reusability of the resources), the    class of nets. This class extends    in the sense that no constraint is imposed to the process structure: any strongly connected state machine is allowed. A deadlock avoidance approach based on Banker’s algorithm [Dij65, Hab75] will be used. In the case of manufacturing systems, a Banker’s approach has already been applied in the following works:  In [LRF98a] a control policy is obtained for the SU–RAS class. The authors present an adapted version of the Banker’s algorithm, obtaining an efficient solution. The improvement is not only based on the knowledge of the process structure, but also on the concept of “partially ordered set of active processes”: it is not necessary to find an ordered termination for all the active processes, but just for some subsets of them.  Forthe same class of RAS,[KTJK97]evaluates, from a performance point of view, a set of different methods for manufacturing systems with Automated Guided Vehicles (AGV), one of which is the classical Banker’s approach.  In [Rev98] and [Law00] an adaptation of the Banker’s method is presented, obtaining polynomial solutions for an extension of the SU–RAS class, where each processing step can be executed in any resource from a given set.  Finally, [Rev00] removes some of the constraints usually imposed to the process structure, developing a Banker’s solution for AGV systems where controlled recirculation is allowed in the routing of guided vehicles. Outside the scope of  the work in[Lan99] extended the Banker’s approach to a class of systems where a multi–set of resources can be used at each processing step and flexible routing is allowed. However, in order to obtain a polynomial solution, the process structure is constrained so that the set of states has a tree structure. In a deadlock avoidance approach, before the evolution of a process is allowed, the first step is to check if such authorization will lead to a “safe” state, i.e., a state from which all the parts being processed can terminate. In this context, the decision procedure of Banker’s algorithm needs to know for each active process its maximal needs of resources along all its life. This information is static and is used together 4.2. The class of    nets 113 with the dynamic information about the resources assigned to each process and the set of available resources in order to determine if an ordering for the sequential termination of the active processes exists, where sequential termination means that a process is able to terminate if the rest of active processes do not move from their current states. If such an ordering can be found, the decision procedure concludes that the state is safe and the resource request can be granted. In this chapter we define a general framework to develop Banker’s-like control policies for deadlock avoidance taking advantage of the knowledge about the structure of the processes (for more restricted classes of systems, see [LRF98b, Lan99]). Two approaches are going to be considered: one that is computable in a static way, and a second one where only dynamic computations are feasible. The concept of (global) maximal needs for a whole process is transformed into the concept of maximal needs of resources related to a process state. The maximal needs of resources of a process are defined as a function depending on the needs of resources to terminate the process execution from the current state, and also on the set of execution sequences that must be preserved by the control policy. As it will be shown, in most cases this approach will lead to more permissive controlled systems. The chapter is organized as follows. Section 4.2 introduces the class of systems and models we are considering. Section 4.3 gives an intuitive presentation of Banker’s algorithm. Section 4.4 is devoted to the main results, presenting the general framework for Banker’s-like algorithms for deadlock avoidance together with some particular solutions. In Section 4.5 some empirical results about the application of different Banker’s–like algorithms are presented. Finally, some conclusions are presented. 4.2 The class of Ë  ÈÊ nets Let us introduce the class of    nets in a formal way. For an intuitive presentation of the main ideas, let us recall the one presented in Chapter 2, where    nets were introduced in an informal way. Here, we are going to present the class in a formal way. Then, we will show the differences with    . First of all, the structure of individual processes is defined. Definition 48 Aextended process Petri net is a generalized strongly connected self–loop free Petri net         where: 1.  is a partition as follows:            . 114 4. Deadlock avoidance policies for    nets. 2. The subnet generated by         ,      ¼      , is a strongly connected state machine. 3.      , there exists a unique minimal P–Semiflow    IN    such that           ,          ,          and      . 4.                 . ¾ An extended process Petri net is a simple specification of the processing of a type of part. Notice that the only difference with a process Petri net as presented in Definition 1 (Chapter 2, page 32) is that there can exist circuits that do not contain place   . With this, the modeling of more complex systems providing tools to represent, for example, unlimited recirculation of parts. We will show this later but, in order to complete the modeling of the dynamics of an extended process Petri net, the introduction of an initial marking is needed. Only acceptable initial markings, as defined in the following, will be considered. Notice that this definition and the following results are the same as in    nets. Definition 49 Let               be an extended process Petri net. An initial marking   is acceptable for  if and only if: 1.         ; 2.            ; 3.                        . ¾ In the following, when considering a marked extended process Petri net we will assume   to be acceptable for it. Some basic structural properties of extended process Petri nets The structural properties of process Petri nets in Chapter 2 are also true for extended process Petri nets. In this section we will only remark the more important ones. The results shown in Proposition 4 (page 37) and Lemma 7 (page 7) presented in Chapter 2 can be trivially extended for this class of nets. They are not reproduced here. Let us present here the definition of the    class. It is analogous to the one presented in Definition 24 (page 52), the only difference being the underlying process structure. 4.3. The Banker’s algorithm for deadlock avoidance 115 Definition 50 The class of    systems is defined recursively as follows: 1. An extended process Petri net is a    . 2. The composition of two    by fusion of the common resource places is also a    . 3. All the    systems are generated using the previous rules. ¾ The classical Banker’s algorithm will be presented in terms of multi–sets. For this reason, let us comment about some well–known concepts in terms of this formalism. Let us recall the net shown in Figure 2.9 (page 61) and the FMS shown in Figure 1.4(b)-(b) whose production routes are depicted in Figure 1.5(b) (pages 15 and 16, respectively). There we can see the main difference between    and    nets: as introduced in Section 1.3.1, the circuits that do not contain places of   are related to the part recirculation capabilities. For example, in Figure 2.9 we can see that parts reaching place    can be processed by resource   , moving to the state represented by place     . At this state, they can return to place    , and this sequence of steps can be repeated as many times as needed. All the results concerning the structure of    nets presented in Chapter 2 are directly extended to this new class. However it is not the case for the liveness characterizations, as it was shown there by means of the counterexample in Figure 2.9 (page 61). The term    does not have any specific meaning. It has been chosen since this class of nets is a generalization of previous introduced classes named as    [ECM95],      [EGVC98b] and    [TCE99]. In fact,                  . Let us also remark the fact that    is the most general class of S–RAS. 4.3 The Banker’s algorithm for deadlock avoidance A deadlock avoidance algorithm controls the system evolutions in such a way that only safe sequences are allowed. A sequence is safe if each state reached during its execution is safe. A state is considered safe if all active processes can finish. The classical Banker’s algorithm is, perhaps, the best known algorithm adopting the deadlock avoidance approach. It is based on the following idea: at the activation moment, each process must declare the maximal number of instances of 116 4. Deadlock avoidance policies for    nets. each type of resource it may need during its execution (the multi–set of maximal needs). In order to ensure that a state is safe, the Banker’s algorithm uses the following sufficient condition: a state is considered to be safe if an ordering in the “sequential termination” of the active processes can be found such that the needs of each active process could be granted using the current free resources and those released by the previously terminated processes (previously terminated according to the ordering selected). Sequential termination means that it is possible to find an ordering for the set of active processes in such a way that if we freeze the system and let them evolve alone according to this order, each process can terminate with the available resources plus the ones released by the processes that have finished before. Let us consider a state               , which has to be tested for safeness and let    be the number of active processes. The method uses the following data structures:     :The multi–set of available resources at the considered state.        means that there are  available copies of resource type  .  :A    –indexed vector of multi–sets of resources. For each active process   ,      is the multi–set of maximal needs of the process, declared at the process activation moment.          means that the process   may request at most  copies of resource  .   :A    –indexed vector of multi–sets of resources. For each active process,   ,          , is the number of copies of the resource  it is using at the state  .  :A    –indexed vector of multi–sets of resources, representing, for each process, the resources that it would need in the future from the current state  . For each process   ,                    . The Banker’s algorithm considers that a given state is safe when there exists an ordering of the active processes allowing all of them to terminate in the following way: the first one can terminate with the resources it is holding plus the      ones; the second one should be able to terminate when the first one terminates, increasing      with the resources allocated to the first process (which are assumed to be freed once the first process terminates), and so on for the rest of active processes. Formally, it can be formulated as follows: let 4.3. The Banker’s algorithm for deadlock avoidance 117 d ae P1_0 P2_0 br2 c r1 f r3 t9 t8 t7 t5 t6 t4 t3 t2 t1 _5 _5 _4 _4 _3 _5 _3 _5 _4 _5 Figure 4.1: A    that will be used to show the policies 118 4. Deadlock avoidance policies for    nets.  be a system state with    active processes,         . The Banker’s algorithm considers the state  to be safe if and only if there exists an ordering function (a bijective mapping) &                  such that, for each        ,                ½                              Let us now relate the Banker’s algorithm and the    models. In the algorithm, each process has to be identified. As stated before, in a    model an active process is a token in a state place. If we consider, for instance, the    in Figure 4.1, marking   '             can be described as the set of processes  '  '     , where '  '  correspond to the processes modeled by the tokens in the state corresponding to place ' and   to the one modeled by the token in  . To conclude this introduction, let us see these values for the net of Figure 4.1. At marking    '             we have:           '              '                            '           '                     '              '                     Let us consider a system with    active processes, each one with a multi– set of  types of resources (representing the global maximal needs). As proved in [Gol78], to test if such a state is safe for the original version of the Banker’s algorithm is               . 4.3.1 A general schema for Banker’s like algorithms We are going to present a general framework to study algorithms that are similar to the classical Banker’s approach. For this, let us introduce the Algorithm 4.2. It shows the general schema of the ‘core’ of what we will consider here Banker’s based method: the algorithm to decide if a given state is considered safe or not. 4.3. The Banker’s algorithm for deadlock avoidance 119 daVinci V2.1 #1: 6r2+5r1+r3(−) #3: c+3r2+5r1+r3(−) #6: 2c+5r1+r3(*) #11: e+c+3r2+r3(+) #13: c+f+3r2+5r1(+) #17: 2c+f+5r1(*) #19: d+f+2r2(+) #8: d+2r2+r3(−) #18: e+f+6r2(+) #22: e+c+f+3r2(+) #24: e+2c+f(*) #7: e+6r2+r3(−) #12: f+6r2+5r1(−) #14: e+2c+r3(*) #16: a+c+f+3r2 a+6r2+r3(−) #2: a+f+6r2(−) #15: #20: b+f+2r2+5r1(−) #5: b+2r2+5r1+r3(−)a+b+f+2r2(+) #23:#4: a+c+3r2+r3 #21: a+2c+f #9: a+2c+r3 #10: a+b+2r2+r3(+) Figure 4.2: Reachability graph of the net in Fig. 4.1. 120 4. Deadlock avoidance policies for    nets. Depending on the function  !" , different policies will be obtained; in this way a family of Banker’s like algorithms can be represented. In this chapter we will explore several alternative proposals for the function  !" , comparing them in terms of cost and taking advantage of the special structure of the    nets. Let us first study the complexity of the Algorithm 4.2 in terms of the complexity of the function  !" . The number of while iterations is bounded by     (it corresponds to the worst case: the state with at least one token in each state place). The cost of each iteration is dominated by the statement looking for a terminable process among those in  1. Therefore, the cost is             , where   is the cost of looking for a terminable process among  different processes. Moreover, if ' is a bound for the cost of checking if any process is terminable with a given set of free resources, # is            '    '       . In the case of    nets it is important to remark the following fact: all the tokens (processes) in the same state place can be considered as “equivalent”. This means that once it can be guaranteed that one of them can terminate (adopting a Banker’s strategy), it is obvious that all these processes represented by tokens in the same state place can terminate one after the other, without additional checking. Notice that the presented algorithm uses this property: when it finds a $ !" process, it eliminates all the processes that are at the same state from the set of processes pending in the ordering process. Then, given a set of active processes, the algorithm only needs to check for the ones that are essentially “different”. This means that, at a reachable marking  , when looking for an ordering &  we will have to “order” as much items as marked state places (     ). 4.4 Several different “Banker’s–like” approaches The original Banker’s algorithm was applied to a class of systems where each process had not a known structure representing the set of its possible execution paths mainly because the algorithm was conceived for operating systems where the possible execution sequences can depend on external values, and then can hardly be known a priori. This means that, when a a process needs to move to a successor state, the controller has to take the decision of allowing or not the state change based on:  the set of available system resources, 1Let us recall the definitions in Note 16 (page 46), where this notation was introduced for    . They can be extended in the obvious way to    . 4.4. Several different “Banker’s–like” approaches 121 Algorithm 4.2 Function isSafe(In      : a marked    ; In               Return (iS:boolean) –—Pre: TRUE –—Post:   Is  a safe state? Begin     ;     ;   TRUE While       look for a process   s.t. isTerminable(  ,   ,a) If such  exists Then For Each  s.t.                      –—    represents a state where the process b has terminated –— and the others remain at the same state as in   –— (Notation in Definition 64) End For Else   FALSE End If End While Return (iS) End 128 4. Deadlock avoidance policies for    nets. Note 56 In the following, for a given     and   (    ,       will denote the set of all the paths verifying last point of Definition 55, that is, the set of all the paths bounded by  . ¾ Definition 57 Let      ,  =             , be a marked    . Let ( be a !% for it, let         and let            be the set of active processes at  .  is said to be a f-safe state if, and only if:      ,or       , and: 1. there exists an ordering &           2. there exists             (         (          such that, for each        ,                  ½                             ¾ So, a state will be considered f–safe if, and only if:  there are no active processes, or  there exists an ordering for the active processes and there exist bounds associated to them in such a way that, for each active process, the bound is less or equal than the multi–set of resources available at marking  , plus the multi–sets of resources held by this process and all the other active processes previous to it in the ordering. Note 58 In the sequel, given a    ,      , and a !% for it, ( ,  The set                     is f–safe  , will denote the set of reachable states that are f–safe (these states will be also called f– reachable states).  A    system, controlled in such a way that only f–reachable states are allowed, is called the f–controlled system. ¾ Obviously, a way of avoiding deadlocks could consist in forbidding any process activation. But this has no sense from the point of view of a physical system. Next lemma proves that the !% ´s based approach is less constraining. 4.4. Several different “Banker’s–like” approaches 129 Lemma 59 Let      ,  =             , be a marked    . Let ( be a !% for it. Then: 1.            . 2.            . Proof 1. From Definition 57, point 1 trivially holds. 2. Let        , and let us assume that      (notice that, because of the structure of a    ,      ). Let          . Let    !    . Condition 2 of Definition 57 becomes             , which is equivalent to                   which holds by condition 2 in Definition 55. ¾ The following lemma proves that when a system is controlled using a !% function, there is always an active process able to evolve in one of its production sequences. Lemma 60 Let      ,  =             , be a marked    . Let ( be a !% for it, and let               . Then, there exists at least one active process   such that           and a transition      such that 1.   ½    . 2.           . Proof Let           ,      . First, we are going to prove that  enables at least a transition,   . Then, we will prove that in case of firing   , the reached marking belongs to         . Since      , let                 , and let us also consider "  ,   and             as in Definition 57. Without lost of generality, let us assume that "    ½   and let        . Let us first prove that  enables   . Since       ,   is process–enabled. If       , since in    nets         ,   is also resource–enabled. Let us now assume that       . Since           , inequality in Definition 57 for   is             . According to Definition 55, let us consider the path   130 4. Deadlock avoidance policies for    nets.                      . Since     , there exists    !     such that             , and then,                 . So, for each     ,                             . Then,   is also resource–enabled, and point 1) can be concluded. Let us now prove that           .  if       ,   ½                 ; let us consider the mapping "  ½    ½         defined as "       "        (where    is   constrained to   ½ ), and   ½          . Then, inequality in Definition 57 is now                            ¾                             Taking into account that               and that        , the previous set of inequalities is just a subset of the set of inequalities corresponding to           , which are then verified.  if       , then      ½ ; let us consider the mapping "    "  defined as           ½           , while   ½       , and   ½             , where   is such that      . –For    , inequality in Definition 57 is               ; this is equivalent to                         , which is true since                and                 . –                    ½         ½       ½       ½          ½        which is equivalent to                                               ¾                             or, in other way,                            ½                             which is true since           . ¾ 4.4. Several different “Banker’s–like” approaches 131 As a consequence we can show that the initial marking is always reachable from any f–reachable state. The algorithm simply checks the conditions of Definition 57. Theorem 61 Let      ,  =             , be a marked    . Let ( be a !% for it, and let               . Then           . Proof Let                 ; for each         , let us consider a path            ,                     ¼ . Let us proceed by induction over #                             . Notice that since      , #    . If #   , Lemma 60 ensures that   ½ ½    , and we can conclude. If #    , let us assume that    "    . Lemma 60 ensures that   ½     ,            . Considering for   the same paths considered for  , #  ½  #    from which, by induction hypothesis, we can conclude. ¾ An immediate corollary is that in a f–controlled system each active process can terminate and, in consequence, no deadlock problem can exist. Let us present the last technical result, which establishes a kind of monotonic relation among !% ’s and the set of reachable states of the controlled systems. Proposition 62 Let      ,  =             , be a marked    . Let (  (  be two !% for it such that for each     , for each    (     , there exists    (     ,      . Then,   ½          ¾       . Proof Let     ½       ; let us consider            , "  ,   and             . Inequality in Definition 57 is                           ½                             Accordingto the hypothesis,let us choose,for each        ,a     !         such that       ; then, using "                  , we have that                           ½                                 and then,     ¾       . ¾ Note 63 In the sequel, (   (  will denote that two !% ’s, (  and (  , verify conditions of Proposition 62. ¾ Algorithm 4.3 shows an adaptation of Algorithm 4.2 to the framework of the !% formalism. 132 4. Deadlock avoidance policies for    nets. Algorithm 4.3 Function isFSafe(In      : a marked    ;In             ; In f: a  for  )Return (iFS:boolean) –—Pre:               –—Post:              Begin               FALSE options :=         !        While     $$    choose         $$ If there exists an ordering "  as in Definition 57 Then    TRUE Else $$  $$   End If End While Return (iFS) End Computational cost Testing the if–guard in Algorithm 4.3 is like applying a classical Banker’s algorithm being (         ) the maximal needs of resources for such processes. According to [Gol78], this is                   . Moreover, the loop will be executed, at most         (       times. So, the worst–case time complexity of the previous algorithm is                       (      . Once this general framework for Banker’s–like solutions has been introduced, let us now concentrate on providing some specific instances of !% ’s For each case, two time costs are estimated. 1. The cost of testing if a given state is safe with respect to the considered !% function. 2. The cost of computing the considered !% itself. This last computation has to be carried outline just once for each state place, and the result has to be stored in such a way that there is a set of multi–set of resources associated to each state place. The critical cost is the first one, since it corresponds 4.4. Several different “Banker’s–like” approaches 133 to the on–line computing needed to decide if the firing of an enabled transition should be accepted or not. The classical Banker’s approach Let us consider the !% (  defined as        (                                (            That is, each place has associated the multi–set of maximal needs of each type of resource, along all the processing path. Notice that (  trivially verifies conditions to be a !% for  . Clearly,          corresponds to the controlled system using the Banker’s approach. Let us now see the costs. 1. Since        (       , then       (       and the time cost of checking (  –safeness is                  . 2. In order to compute the (  function, each     has to be visited and for it,      needs to be processed. Therefore, computing the (  function is           . The global look–ahead version This version corresponds to the first intuitive improvement shown and developed in Section 4.4.1 ([TCE00]). Let us consider the function (  defined as  (                               (            This function associates to each state place  the supremum of the resources needed along all the paths (composed of state places) joining  and the corresponding idle state place. Obviously (  also verifies conditions to be a !% for  . Let us now see the computation costs. 1. As in the previous case, (  –safeness checking is                  . 2. The computation of (  for each state place      needs the computation of the set of paths composed of state places in   , and for each one of them,      must be compared. This can be done in                              , using any breadth–first search algorithm [CLR90]. 134 4. Deadlock avoidance policies for    nets. Notice that in both cases the cost is polynomial. A partial look–ahead version This version corresponds to the second intuitive improvement developed in section 4.4.1, and was also presented in [TCE00]. Let us consider the function (  defined as  (                         (            Then, a multi–set is associated for each simple path joining  and the corresponding idle state place, ensuring resources to follow such path, for each state place     . Clearly, (  is a !% for  . Let us now see the costs. 1. Checking (  –safeness is                         (        . It is important to remark the fact that this time can be non–polynomial, as opposed to the two previous cases. In any case, a bound for the safeness– checking time is known a–priori and, then, it can be used to know if this time is enough to meet the real–time constraints imposed by the system. 2. In order to compute (  , the algorithm of Johnson [Joh75] can be adapted to suit our needs. This algorithm was proposed for the computation of all the elementary circuits of a directed graph. The algorithm can be adapted as follows. Let      ; we need to compute all the simple paths joining  and    . Consider the state machine containing  . Remove every transition     . Add a new transition   joining    and  (adding the arcs        and      ). Apply the algorithm of Johnson to compute the elementary circuits in the transformed state machines and discard those not containing    . According to [Joh75] the cost for a given      is                            , which gives.                                 for the whole net. Then, since for each     , (   (   (  and according to Proposition 62,                              . Figure 4.2 shows the reachability graph of the net in Figure 4.1. Each node corresponds to a reachable state in the uncontrolled system. Notice that some deadlocks are reachable (for instance, marking  ). Some markings leading inevitably to a deadlock are also reachable (for instance, markings  and  ). Among the set of reachable markings: 4.4. Several different “Banker’s–like” approaches 135  those with a “  ” mark form the set of reachable markings when the (  !% is used (the original version),  those with a “  ” mark must be added to them in order to obtain the states reachable when (  is used,  finally, the markings with a “ ” mark must be added to obtain the set of reachable markings for the (  function. Let us now present how this framework allows the introduction and study of alternative approaches. Another polynomial versions The general framework that has been presented allows the development of a wide family of deadlock avoidance control policies, as many as !% ’s we are able to establish. Let us consider now the function (  defined as        (               the shortest path joining               (           Function (  associates to each place the supremum of the multi–set of resources needed if a part follows the shortest path joining  and the corresponding idle state place. Let us now see the costs. 1. Since for each state place  ,  (       , (  –safeness checking complexity is the same as for (  and (  . 2. The computation of (  , needs the shortest path between  and the corresponding idle state place for each     . This can be done applying the single–source shortest path algorithm [CLR90]. So, computation of the (  function is                         . In a similar way, we could consider the function mapping to each state place the longest path, or the path corresponding to the shortest processing time, or the path corresponding to the use of the cheapest resources, any of them, etc. All of them would require a polynomial time for safeness checking. Moreover, the computation of the !% will also be of polynomial complexity (they correspond to graph algorithms of polynomial complexity). 136 4. Deadlock avoidance policies for    nets. Finally, notice that (   (   (   (  and in consequence, we can state that                                        . Another interesting remark is that adopting the concept of Banker’s–like algorithm presented in this chapter, no !% can be more permissive than (  . 4.4.3 A dynamic approach A !% function is a way to associate information to each place about the needs of resources ensuring that a set of paths can be followed until sequential termination using the set of free resources. This set of paths is chosen in a static way, independently of any reachable marking. However, there is an alternative way which consists in choosing the paths in a dynamic way, depending on the current marking of the set of resources. For this, we are going to present an alternative way of testing if at a reachable marking a process can terminate, based on a graph algorithm. The algorithm determines at a given reachable marking if there exists a path that can be followed with the current free resources. As it will be shown, this new method will be as permissive as the partial look–ahead solution, but with a polynomial cost. Let us first introduce some more terminology. Definition 64 Let      ,  =             , be a marked    . Let         . An active process     is   –Terminable if, and only if, there exists a path                        ,                , such that   ½  ¾      . ¾ Note 65 The reached marking,   , will be as follows:               ,             ,   ,                    ,               . ¾ A path like   is said to be   –Executable for the process  . Notice that a process is   –terminable (at marking  ) if there exists a path joining the state place where the process stay with the corresponding idle state, and this path can be followed by the part using the available free resources plus those that at present are allocated to the process itself. 4.4. Several different “Banker’s–like” approaches 137 In the partial look–ahead approach the selection of the route that the part needed to follow in order to finish its processing was done considering all the different available paths from a given place to the end of the processing; with the information about all of these paths, one of them can be chosen as in Definition 64. Let us now show the conditions under which a path is executable. Proposition 66 Let      ,  =             , be a marked    . Let         , let    and let                        ,                .   is   -Executable for  if, and only if,  &                         . Proof   ) Let us assume that   ½     ¾        ½            . By contradiction, let  be the minimal index such that                   . Firing         ,     is reached, and                          . Notice that     enables   ,                         , which is equivalent to say that                                    . This is clearly a contradiction.   ) Let us prove by induction over the prefix of     which is fireable from  that   is   -Executable. 1. Since                   ,   is both process– and resource–enabled. Therefore,   can be fired. 2. Let us now assume that   ½     ¾        ½      . First, since         ,           (   is process–enabled). Moreover,     ½                      . To prove that   is also resource–enabled, we must ensure that     ½                   . This is equivalent to                                    , which is true by hypothesis. ¾ The Algorithm 4.4 checks if an active process corresponding to a reachable marking  is   -Executable. Or, in other words, if the free resources are enough for the process to terminate when the rest of active processes do not move from their current states. Complexity of Algorithm 4.4: The cost of the for loop is            , while the cost of looking for a simple path joining two nodes in the graph of marked nodes is              [CLR90]. Then, the cost of the function is                          . Since         and      , the cost is           . Let             . Therefore, taking into account the cost computed in Section 4.3.1, checking for safety of a given marking is              