nÃo hà / Esse trabalho propÃe um novo mÃtodo para sÃntese de supervisores em sistemas a eventos discretos, utilizando redes de Petri coloridas, baseado no contexto da teoria de controle supervisÃrio. Como aspecto principal, tem-se a formalizaÃÃo teÃrica e a prova matemÃtica do mÃtodo para sÃntese desses supervisores, denominado RestriÃÃes de Controle sobre Cores Decompostas (RCCD). AlÃmdisso, como consequÃncia, à apresentado ummÃtodo para reduÃÃo do nÃmero de lugares de controle denominado FusÃo de Controladores (FC). Os mÃtodos RCCD e FC sÃo uma extensÃo do trabalho de Moody e Antsaklis, que propÃem, originalmente, um Teorema comprovando a sÃntese de supervisores usando redes de Petri ordinÃrias e, dessa forma, sÃo propostas aqui as extensÃes desse Teorema, para o contexto das redes de Petri coloridas. Nesse caso, explora-se a decomposiÃÃo da matriz de incidÃncia de uma rede de Petri colorida para de…nir lugares de controle que nÃo sÃo con‡itantes em suas aÃÃes, usando o soft CPNTools como ferramenta. A seguir, à realizada a fusÃo desses lugares de controle, obtidos com o RCCD, com a aplicaÃÃo do mÃtodo FC, em que o lugar de controle encontrado, denominado supervisor resultante da fusÃo, atende as mesmas restriÃÃes e contribui com a mesma performance de controle do sistema. / This work proposes a newmethod for synthesis of supervisors in discrete event systems using coloured Petri nets, based in the theory of supervisory control. As a main aspect, there is the theoretical and formal mathematical proof of the method for synthesis of supervisors, called Control Constraints on Decomposed Colors (CCDC). In addition, as a consequence, it is presented a method for reducing the number of control places called Fusion of Controllers (FC). The CCDC and FC methods are an extension of the work of Moody and Antsaklis, they propose, originally a theorem proving the synthesis of supervisors using Petri nets thus are proposed here extensions of this theorem to the context of coloured Petri nets. In this case, it is explored the decomposition of the incidence matrix of a coloured Petri net to de…ne control places that are not con‡icting in their actions, using the soft CPNTools. The following is realized the fusion of these control places obtained with CCDC, with the aplication of the FC method. The obtained place is called the resulting fusion supervisor, where it is found the same constraints and contributes with the same control system performance.

Em geral a avaliação de desempenho dos sistemas produtivos considera critério normalizado de uso eficiente de recursos de transformação tecnológica (como máquinas e matérias-primas), processamento de informações e operações de manuseio/transporte. No entanto, não existem critérios ou regras normalizadas para avaliar o desempenho de um sistema produtivo no contexto da sustentabilidade. Assim, este trabalho introduz uma abordagem para identificar e avaliar os indicadores de desempenho relacionados à sustentabilidade dos sistemas produtivos, especificamente para casos geograficamente dispersos, ou seja, Sistema Produtivo Disperso (SPD), no qual os processos ocorrem de forma distribuída e dispersa. A abordagem proposta baseia-se em um framework destinado a medir os indicadores-chave de desempenho de sustentabilidade (KPIs - Key Performance Indicators) que avaliam a sustentabilidade de um sistema. O framework considera a norma ANSI/ISA-95 e os processos produtivos modelados usando a rede de Petri. A metodologia de avaliação de sustentabilidade considera o equilíbrio dos indicadores de sustentabilidade, os quais dependem dos aspectos econômicos, ambientais, sociais e tecnológicos, além do comprometimento de todos os colaboradores envolvidos. / In general, the performance evaluation of productive systems considers normalized criteria of the efficient use of technological transformation resources (such as machines and raw materials), information processing and handling/transportation operations. However, there are no normalized criteria or rules to evaluate the performance of a productive system in the context of sustainability. Thus, this paper introduces an approach to identify and to evaluate the performance indicators related to the sustainability of productive systems, specifically for geographically disperse cases, i.e., disperse productive system (DPS), in which the processes are in a distributed and disperse architecture. The proposed approach is based on a framework aimed to measure sustainability key-performance-indicators (KPIs) that evaluate the sustainability of a system. The framework considers the ANSI/ISA-95 standard and productive processes modeled using Petri net. The sustainability assessment methodology considers the balance of sustainability indicators, which depend on economic, environmental, social, and technological aspects, besides the commitment of all the partners involved.

Cette thèse traite de la vérification formelle de systèmes critiques où la correction du système dépend du respect des contraintes temporelles. La première partie étudie la modélisation et la vérification formelle par model-checking de systèmes temps réel dans le contexte de l’industrie aéronautique et spatiale. La deuxième partie décrit notre méthode d’exploitation des symétries pour les réseaux de Petri temporels. Nous définissons un opérateur de composition symétrique pour la construction de réseaux. Puis nous proposons des solutions pour la construction d’espaces d’états quotients par la relation d’équivalence induite par les symétries. Notre méthode s’applique aux réseaux de Petri, temporels ou non. A notre connaissance il s’agit de la première méthode applicable aux réseaux de Petri temporels. Des résultats expérimentaux encourageants sont présentés. / This thesis deals with formal verification of critical systems where the system’s correction depends on compliance with time constraints. The first part studies the formal modeling and verification by model-checking of realtime systems in the context of the aerospace industry. The second part describes our method for symmetry reduction of Time Petri Net. We define a symmetric composition operator for building Net. Then we present our solution for construction of quotients of the state spaces by the equivalence relation induced by symmetries. Our method applies to Petri nets, temporal or not, but to our knowledge this is the first methodology for Time Petri Nets. Encouraging experimental results are presented.

De nos jours, les workflows sont largement utilisés par les entreprises et les organisations en vue d’améliorer l’efficacité organisationnelle, la réactivité et la rentabilité en gérant les tâches et les étapes de processus opérationnels. La vérification des spécifications est devenue obligatoire afin d’assurer que ces processus sont correctement conçus et atteignent le niveau de confiance et de qualité attendu.Dans ce contexte, cette thèse porte sur la vérification de spécifications modales – comportements nécessaires ou recevables impliquant plusieurs activités et leurs causalités – de workflows nets – une classe de réseaux de Petri adaptés à la description de workflows. En particulier, cette thèse définit un cadre novateur permettant de modéliser les exécutions de workflow nets,avec ou sans données, et de vérifier des spécifications modales à l’aide de systèmes de contraintes. Elle présente également deux méthodes de réduction préservant la "generalised soundness" et la validité d’une spécification modale donnée. Ces méthodes de réduction sont ensuite présentées comme des étapes de prétraitement réduisant la taille des workflow nets, de sorte que la vérification des propriétés conservées puisse être effectuée sur de plus petites instances. Enfin, cette thèse présente les outils qui ont été mis en oeuvre ainsi que des expérimentations qui ont été menées sur un grand nombre de workflows industriels afin de valider les approches proposées dans cette thèse. Ces résultats expérimentaux convaincants mettent en évidence l’efficacité, l’efficience et le passage à l’échelle de la méthode vérification de spécification modales ainsi que des méthodes de réduction introduites dans cette thèse. / Nowadays workflows are extensively used by companies and organisations in order to improve organizationaleffciency, responsiveness and profitability by managing the tasks and steps of business processes. Theverification of specifications has become mandatory to ensure that such processes are properly designedand reach the expected level of trust and quality. In this context, this thesis addresses the verification ofmodal specifications – necessary or admissible behaviour involving several activities and their causalities –of workflow nets – a Petri nets class suited for the description of workflows.In particular, it defines an innovative constraint system based framework to model executions of ordinary as wellas coloured workflow nets, and verify modal specifications. Further, it presents powerful reduction methodspreserving properties of interest such as generalised soundness and correctness of a given modal specification.Such reduction methods are then portrayed as pre-processing steps reducing workflow nets size, so that theverification of preserved properties can be carried out on smaller instances.Finally, as a practical contribution, this thesis introduces the tools that have been implemented as well asexperimentations that have been carried out over industrial workflow nets in order to validate the approachesproposed in this thesis. The convincing experimental results highlight the effectiveness, effciency andscalability of the modal specification verification method and reduction methods introduced in this thesis.

Orientador: Rafael Santos Mendes / Tese (doutorado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica e de Computação / Made available in DSpace on 2018-08-07T23:46:24Z (GMT). No. of bitstreams: 1 Portugal_DeniseSoderoVinhas_D.pdf: 1731980 bytes, checksum: 98f3bdce8b6d0d6e00e2c6c96ba968f7 (MD5) Previous issue date: 2006 / Resumo: Uma metodologia para obter um escalonamento cíclico em Sistemas a Eventos Discretos é proposta neste trabalho. Esta metodologia parte de uma rede de Petri que modela minimamente um sistema a eventos discretos funcionando em regime periódico. O método identifica quais são as redes que podem ser tratadas por ele. As redes de Petri tratáveis serão decompostas em subredes identificadas por processos, que são classificados de acordo com suas topologias, o que permite a modelagemdo escalonamento cíclico do sistema através de uma modelagem em programação linear inteira mista. Este modelo em MILP será implementado no software GAMS. Alguns exemplos tirados da literatura serão usados para mostrar e testar a aplicação desta metodologia / Abstract: A methodology to obtain a cyclic scheduling in Discrete Events Systems is proposed in this work. This methodology initializes with a Petri netmodeling a discrete events system functioning with periodic processing. The method identifieswhich are the nets that can be treaties by him. The ¿tractable¿ Petri nets will be decomposed in subnets identified by process, which are classified according to its topologies, that permits us tomodel the cyclic scheduling of the systemby amixed integer linear programming model. This model in MILP will be implemented using software GAMS. Some examples from the literature will be used to show and to test the application of this methodology / Doutorado / Automação Industrial / Doutor em Engenharia Elétrica

The purpose of this master's thesis was to design and implement the simulation server for the DEVS that is using already existing SmallDEVS system. The work is aimed to description of the DEVS formalism, SmallDEVS and implemented simulation server. This server provides functions to create new DEVS models, edit already existing models and control simulation. In addition server saves information about state changes during the simulation process, so we can find out the state of the model at any simulation time. It allows to analyze this data and get more information about the simulation process, which was not possible until now. There is a complete description of the communication protocol between client and server in this document. If a new function is implemented in the SmallDEVS system, this protocol can be easily updated. A prototype of client was implemented during this project to test the implemented simulation server. The client implements this communication protocol and allows the user to work with the SmallDEVS system on the server.

The main subject of this Master's thesis is risk management with emphasis on risk analysis stage. All important stages, definitions and techniques are introduced in the context of risk management. There are several risk analysis methods discussed in this thesis, especially the Markov analysis and the Petri net analysis. After the thorough analysis of the subject, the system to support the risk management was designed and implemented, while precisely Markov analysis was chosen.

<div>Petri net (PN) is a useful tool for the modeling and analysis of complex systems and has been widely used in a variety of practical systems. This dissertation aims at studying highway transportation systems using Petri nets and investigating several fundamental problems related to the modeling, state/structure estimation, and control of highway traffic.</div><div>This dissertation starts with two kinds of modeling schemes. The first one uses the Probabilistic Petri net to model a highway segment. The traffic movement probabilities have also been shown. The second scheme uses the traditional Petri net structure to model the traffic network around a city’s metropolitan area, where places represent the destinations of interests and tokens represent time units.</div><div>After that, two estimation algorithms and one control algorithm have been proposed, respectively, based on external observations. The first algorithm deals with labeled Petri nets and the objective is to estimate the minimum initial marking that has (have) the smallest token sum. The second algorithm estimates the Petri net structures from the observations of finite token change sequences in terms of the minimum number of transitions and connections. At last, the traffic volume control algorithm is to keep the traffic volume within capacity. The controller will be applied in each evolution step depending on observation.</div><div>Since we have been focusing on the optimization problems of the structure and markings of the Petri net, it is directly related to the optimal route planning problems in highway traffic scenarios. Thus, we can obtain optimized traveling routes by applying proposed algorithms to the traffic systems.</div>

Nos travaux portent sur l'analyse des systèmes de production automatisée à l'aide de réseaux de Petri. Le problème posé est de savoir si un système peut se bloquer complètement ou partiellement et si besoin de calculer un contrôleur garantissant son bon fonctionnement. Les systèmes de production se modélisent naturellement à l'aide d'une sous-classe des réseaux de Petri, les S3PRs. Ce modèle a été très largement étudie par le passe conduisant à des méthodes basées uniquement sur la structure du modèle. Dans ce travail, nous généralisons ces travaux aux modèles des WS3PR, une extension des S3PR ou la réalisation d'une active nécessite non par une ressource mais plusieurs ressources d'un même type et pour lesquels nous proposons des techniques originales combinant des éléments de Théorie des graphes et de théorie des nombres, améliorant même les méthodes du passe sur le modèle simple des S3PR.On présente une caractérisation fine de la vivacité d'un tel modèle basée la notion d'attente circulaire. Une attente circulaire peut être vue comme une composante connexe du sous graphe réduit aux transitions et aux places ressources du modèle. Puis nous démontrons que la non vivacité d'un WS3PR est équivalente a l'existence d' ≪ un blocage circulaire dans une attente circulaire ≫. Ce résultat généralise finement la caractérisation de la vivacité d'un S3PR. Apres avoir introduit la notion de ≪ circuits du graphe de ressources ≫ (WSDC), on construit une méthode de contrôle de ces verrous garantissant la vivacité du modèle d'autant plus efficace qu'une méthode de décomposition du réseau est proposée. Enfin, une traduction de traduit la condition de vivacité des WS3PR sous la forme d'un programme linéaire en nombres entiers est établie et des expérimentations ont démontré l'intérêt de la méthode pour contrôle de systèmes l'allocation des ressources. / As an indispensable component of contemporary advanced manufacturing systems, flexible manufacturing systems (FMSs) possess flexibility and agility that traditional manufacturing systems lack. An FMS usually consists of picking and placing robots, machining centers, logistic systems, and advanced control systems. Some of them can be recognized as its shared resources, which result in its flexibility but may lead to its deadlocks. As a classic problem in resource allocation systems, deadlocks may arise in a fully automated FMS and bring about a series of disturbing issues, from degraded and deteriorated system productivity and performance to low utilization of some critical and expensive resources and even long system downtime. Therefore, the analysis of and solution to deadlock problems are imperative for both a theoretical investigation and practical application of FMSs. Deadlock-freedom means that concurrent produc-tion processes in an FMS will never stagnate. Furthermore, liveness, another significant behavioral property, means that every production process can always be finished. Liveness implies deadlock-freedom, but not vice versa. The liveness-enforcement is a higher requirement than deadlock-freedom.From the perspective of the behavioral logic, the thesis focuses on the intrinsicallylive structures and deadlock control of generalized Petri nets modeling flexible manufacturing systems. Being different from the existing siphon-based methods, a concept of intrinsically live structures becomes the starting point to design, analyze, and optimize a series of novel deadlock control and liveness-enforcing methods in the work.The characteristics and essence of intrinsically live structures are identified and derived from subclasses of generalized Petri nets modeling FMSs with complex resource usage styles. In addition, the numerical relationship between initial markings and weights of connecting arcs is investigated and used to design restrictions that ensure the intrinsical liveness of global or local structures.With the structural theory, graph theory, and number theory, the thesis work achieves the goals of deadlock control and liveness-enforcement.The proposed methods are superior over the traditional siphon-based oneswith a lower computational complexity (or a higher computational efficiency),a lower structural complexity, and a better behavioral permissiveness of the controlled system.

Le contrôle de systèmes industriels à cause de l’automatisation et la réduction de nombre des opérateurs devient un enjeu crucial. Les systèmes de production automatisés (AMS) sont d’autant plus touchés car une défaillance du programme de contrôle peut réduire considérablement la productivité voire entraîner l’arrêt du système de production. Pour certains de ces systèmes où le partage des ressources est pondérant, la notion de blocage partiel ou global est fréquente et la validation avant implantation est préférable pour réduire les risques.En raison de la capacité des réseaux de Petri à décrire aisément l’exécution concurrente des processus et le partage des ressources, de nombreuses méthodes de vérification d’absence de blocage et de synthèse de contrôleurs basées sur la théorie structurelle ou le graphe d’accessibilité des réseaux de Petri ont été proposées au cours des deux dernières décennies.Traditionnellement, une méthode de prévention de blocage est évaluée selon trois critères de performance: la complexité structurelle, la permissivité comportementale, et la complexité de calcul. Les méthodes fondées sur l’espace d’état aboutissent généralement à un contrôle maximal permissif mais souffrent de l'explosion combinatoire de l'espace d'états. En revanche, les méthodes de synthèse de contrôleurs fondées sur l’analyse structurelle évitent le problème de l’explosion de l’espace d’état mais aboutissent à des superviseurs pouvant restreindre considérablement les comportements admissibles du système. De plus si la théorie structurelle de contrôle de siphons pour la synthèse des superviseurs est mature dans le cas des réseaux de Petri ordinaires, elle est en développement pour les réseaux de Petri généralises. Par ailleurs, la plupart des travaux existants partent du principe que les ressources sont constamment disponibles. Or l’indisponibilité de ressources est en réalité un phénomène ordinaire. Il serait donc judicieux de développer une politique de vérification de blocage qui soit efficace tout en considérant des ressources non fiables.Cette thèse vise principalement à faire face aux limitations mentionnées ci-dessus. Nos principales contributions à la fois théoriques et algorithmiques sont les suivantes.Premièrement, après avoir revisité les conditions de contrôlabilité des siphons (cs–propriété) et précisé les limitations de la max cs- propriété et max’ cs- propriété, nous définissons la max’’ cs-propriété et nous démontrons que cette nouvelle propriété est une condition non seulement suffisante mais aussi nécessaire pour la vivacité de la classe des GS3PR (Generalized Systems of SimpleSequential Processes with Resources).Par la suite nous montrons comment le problème de la vérification de cette propriété et donc la vivacité des GS3PR peut se ramener à la résolution d’un programme linéaire en nombre entiers.Dans une seconde partie, nous proposons une classe de réseaux de Petri appelée M-Nets dotée d’une forte capacité de modélisation des systèmes de production automatisés. En combinant la théorie du contrôle siphon avec la théorie des régions, nous développons une méthode de prévention de blocage ayant un bon compromis entre l'optimalité du comportement et la complexité de calcul. De plus, nous proposons une méthode de synthèse d'un contrôleur maximal permissif pour une sous-classe de réseaux notée b-nets.Enfin, nous proposons dans cette thèse une méthode de conception d’un superviseur de systèmes de production automatisés où les ressources ne sont pas toutes fiables et particulièrement efficace pour la classe des S3PR (Systems of Simple Sequential Processes with Resources). / Because of automation and reduction of the number of operators, the control of industrial systems is becoming a critical issue. For automated manufacturing systems (AMS) where resource sharing is preponderant, the notion of partial or total blocking is frequent and validation before implementation is preferable to reduce the risks.Due to the easy and concise description of the concurrent execution of processes and the resource sharing by Petri nets, many methods to verify deadlock-freeness and to synthesize controllers using structural theory or reachability graph have been proposed over the past two decades.Traditionally, a deadlock control policy can be evaluated by three performance criteria : structural complexity, behavioral permissiveness, and computational complexity. Generally, deadlock control policies based on the state space analysis can approach the maximal permissive behavior, but suffer from the state explosionproblem. On the contrary deadlock control policies based on the structural analysis of Petri nets avoid in general the state explosion problem successfully, but cannot lead to the maximally or near maximally permissive controller. Morover, the current Deadlock control theory based on siphons is fairly mature for ordinary Petri nets,while for generalized Petri nets, it is presently at an early stage.On the other hand, most deadlock control policies based on Petri nets for AMS proceed on the premise that the resources in a system under consideration are reliable. Actually, resource failures are inevitable and common in most AMS, which may also cause processes to halt. Therefore, it is judicious to develop an effective and robust deadlock control policy considering unreliable resources.This thesis aims to cope with the limitations mentioned above. Our main theoretical and algorithmic contributions are the following. Firstly, after revisiting the controllability conditions of siphons and limitations of max and max' controlled-siphon properties, we define the max'' cs property and we prove that this new cs-property is not only sufficient but also a necessary liveness condition forgeneralized systems of simple sequential processes with resources (GS3PR). Moreover, we show how the checking of this property and hence liveness of GS3PR nets can be translaled into resolution of an integer programming (IP) model.Secondly, we propose a class of manufacturing-oriented Petri nets, M-nets for short, with strong modeling capability. Combining siphon control and the theory of regions, we develop a deadlock prevention method that makes a good trade-off between behavioral optimality and computational tractability Moreover, this thesis proposes a maximally permissive control policy for a subclass of Petri nets (calledBéta-nets) based on the token distribution pattern of unmarked siphons.Finally, we propose a designs method for robust liveness-enforcingsupervisors for AMS with unreliable resources appropriate in particular for systems of simple sequential processes with resources(S3PR)