Dentro do conceito de "Edifício Inteligente", que tem como objetivo a otimização da infra-estrutura física e do ambiente em relação a aspectos de produtividade e comportamentais, este trabalho apresenta uma metodologia para modelagem e simulação de estratégias de gerenciamento de sistemas de ar condicionado onde focaliza-se a integração do ar condicionado com os demais sistemas de um edifício. Para tanto introduz-se uma abordagem híbrida onde são considerados aspectos de Sistemas a Eventos Discretos e de Sistemas de Variáveis Contínuas. Como estudo de caso apresenta-se a modelagem do sistema de ar condicionado do Prédio dos Ambulatórios do Hospital das Clínicas da Faculdade de Medicina de São Paulo, para o qual se aplica o método proposto para análise do tratamento de perturbações no sistema de ar condicionado resultantes de variações da carga térmica. / Considering "Intelligent Buildings", which have as one of its purpose to improve its structure and environment in order maximise the effectiveness of its occupants, this work introduce a methodology for modelling and simulation of HVAC systems. The focus is on the integration of the HVAC system with other building systems. A hybrid approach is introduced to consider both discrete and continuous aspects. As case study, we present the models for the Ambulatory Building of Hospital of the Medical School of São Paulo University. Particularly, the proposed methodology is used to analyse if the response of the HVAC system to thermal load variations can be enhanced, improving the thermal comfort, when integration between systems is considered.

O sistema de elevadores como equipamento para o transporte vertical de pessoas e bens é um componente fundamental no projeto de edifícios e, neste âmbito, a disponibilidade e eficiência do seu serviço deve ser objeto de cuidadosa análise em função de sua influência no desempenho e produtividade das atividades dos usuários do prédio. Neste contexto e considerando especificamente os edifícios inteligentes cuja finalidade é a otimização a nível estrutural e funcional do edifício como um todo, e onde a integração entre seus sistemas cumpre um papel fundamental para atingir estes objetivos, o presente trabalho propõe uma metodologia para a modelagem de sistemas de elevadores nestes prédios, que considera a sua integração com outros sistemas prediais. A abordagem empregada no desenvolvimento deste trabalho baseia-se na caracterização dos sistemas de elevadores como sistemas a eventos discretos (SED), pois sua dinâmica é definida através da ocorrência de eventos e a manutenção de estados discretos. Assim, na metodologia utiliza-se técnicas derivadas das redes de Petri (redes de Petri interpretadas), de comprovada eficiência para a modelagem, análise e controle de SEDs. Estas ferramentas são usadas através de uma abordagem estrutural, onde o sistema é modelado em diferentes níveis de abstração: um modelo conceitual obtido pelo uso da técnica PFS (Production Flow Schema) em um primeiro nível, e o refinamento deste para modelos funcionais através do uso do MFG (Mark Flow Graph) e suas extensões, onde são preservadas as estruturas das atividades do nível superior e são descritos os detalhes em um nível funcional. A metodologia proposta confirmou ser útil e eficiente para a modelagem do sistema de elevadores em edifícios inteligentes, ao permitir a especificação do modelo funcional de todo o sistema (objeto de controle e sistema de controle) e das estratégias que facilitam a sua integração com outros sistemas prediais / The elevator system as mean for the vertical transport of people and goods is a fundamental component in the design of buildings. The availability and efficiency of this service must be object of careful analysis due to its influence on the performance and productivity of the building users' activities. In intelligent buildings, the purpose is the optimization of its structural and functional levels and where also the integration between all building systems accomplishes a fundamental role to reach these objectives. In this context, this work proposes a methodology for the modeling of elevator systems in these buildings, which consider your integration with others buildings systems. The approach developed in this work is based on the characterization of elevator systems as Discrete Event Systems (DES), since the dynamic behavior is defined through the discrete events and discrete states. The proposed methodology uses techniques, that are derived of interpreted Petri nets, which has been proven as an efficient tool for modeling, analysis and control of DES. In this context, systems are modeled in different levels of abstraction: a conceptual model which is obtained by using the PFS (Production Flow Schema) technique level, and a functional model by using MFG (Mark Flow Graph) and its extensions. The MFG abstraction level describes details in a functional form, where are preserved the description activities of previous levels. The methodology proposal confirmed to be useful and efficient to elevator systems modeling, when allowing the functional specification of the whole system (object of control and control system), and strategies that facilitate its integration with others building systems.

Ao longo das últimas décadas, o paradigma de sistemas críticos em segurança vem sofrendo transformações como forma de se adequar às novas necessidades demandadas, tais como redução de custos e aumento da produtividade. No Sistema de Gerenciamento de Tráfego Aéreo, esta transformação é preconizada pelo paradigma CNS/ATM (Communication, Navigation, Surveillance / Air Traffic Management), baseado no uso de novas tecnologias digitais, sobretudo satélites, aplicadas à comunicação, à vigilância, à navegação e ao gerenciamento do tráfego aéreo. O CNS/ATM visa reduzir as restrições do atual paradigma de tráfego aéreo como forma de atender sua crescente demanda, mantendo (ou melhorando) os atuais níveis de segurança. Porém, esta mudança de paradigma traz consigo novos desafios e necessidades, sobretudo, quanto à forma de se avaliar os sistemas resultantes. Em face destes novos desafios e problemas enfrentados, este trabalho propôs um método de avaliação de risco, constituído pela união dos métodos \"absoluto\" e \"relativo\" preconizados pela Organização da Aviação Civil Internacional (OACI), pelo emprego do formalismo das redes de Petri Fluidas e Estocásticas (RPFE) na modelagem dos sistemas, e pela comparação entre os valores de métricas de segurança estimados para o sistema avaliado e para um sistema legado. Este método foi aplicado para avaliar a segurança na mudança do atual paradigma de vigilância aérea, baseado em equipamentos Radar, para o paradigma de Vigilância Dependente Automática por Radiodifusão (ADS-B). Como conclusões, o método proposto mostrou-se promissor para avaliar a segurança de sistemas baseados nos atuais paradigmas de sistema críticos em segurança, especialmente o CNS/ATM, onde o formalismo das RPFE proporcionou modelar suas principais características, e a simulação por eventos discretos permitiu estimar as métricas desejadas. Além disso, a ADS-B mostrou-se uma aplicação viável para a vigilância no Sistema de Controle de Tráfego Aéreo, sendo capaz de reduzir o nível de exposição das aeronaves a eventos de perda de separação e, assim, melhorar os níveis de segurança do tráfego aéreo. / In last decades, the safety critical systems paradigm has changing to adapt itself to new necessities, such as costs reduction and productivity demand growth. In the Air Traffic System, those changes are ruled by CNS/ATM paradigm (Communication, Navigation, Surveillance / Air Traffic Management), based on new digital Technologies, mainly Satellites, applied to Communication, Surveillance, Navigation and Air Traffic Management. CNS/ATM intends to reduce the restrictions of current air traffic paradigm, enabling the growth of air traffic capacity without affecting current safety levels. However, this new paradigm brings together new challenges and needs, mainly related to safety assessment. In face of these new challenges, this work proposed a method of risk assessment constituted by the union of the \"absolute\" and \"relative\" assessment methods adopted by the International Civil Aviation Organization (ICAO), by modeling systems using Fluid Stochastic Petri Nets (FSPN) formalism, and by comparison between safety metrics obtained from proposed and legacy system simulations. This method was applied to assess a new concept of air traffic surveillance, named \"Automatic Dependent Surveillance - Broadcasting\" (ADS-B). As main conclusions, the proposed method was promising to assess system safety properties based on current safety critical system paradigm, especially the CNS/ATM, where FSPN formalism provided important modeling capabilities and discrete event simulation allowed estimating the desired safety metric. Besides, ADS-B has meaningfully reduced the separation losses risks and, therefore, it could be used to air traffic control surveillance system to improve capacity and/or safety levels of air traffic system.

O sistema de elevadores como equipamento para o transporte vertical de pessoas e bens é um componente fundamental no projeto de edifícios e, neste âmbito, a disponibilidade e eficiência do seu serviço deve ser objeto de cuidadosa análise em função de sua influência no desempenho e produtividade das atividades dos usuários do prédio. Neste contexto e considerando especificamente os edifícios inteligentes cuja finalidade é a otimização a nível estrutural e funcional do edifício como um todo, e onde a integração entre seus sistemas cumpre um papel fundamental para atingir estes objetivos, o presente trabalho propõe uma metodologia para a modelagem de sistemas de elevadores nestes prédios, que considera a sua integração com outros sistemas prediais. A abordagem empregada no desenvolvimento deste trabalho baseia-se na caracterização dos sistemas de elevadores como sistemas a eventos discretos (SED), pois sua dinâmica é definida através da ocorrência de eventos e a manutenção de estados discretos. Assim, na metodologia utiliza-se técnicas derivadas das redes de Petri (redes de Petri interpretadas), de comprovada eficiência para a modelagem, análise e controle de SEDs. Estas ferramentas são usadas através de uma abordagem estrutural, onde o sistema é modelado em diferentes níveis de abstração: um modelo conceitual obtido pelo uso da técnica PFS (Production Flow Schema) em um primeiro nível, e o refinamento deste para modelos funcionais através do uso do MFG (Mark Flow Graph) e suas extensões, onde são preservadas as estruturas das atividades do nível superior e são descritos os detalhes em um nível funcional. A metodologia proposta confirmou ser útil e eficiente para a modelagem do sistema de elevadores em edifícios inteligentes, ao permitir a especificação do modelo funcional de todo o sistema (objeto de controle e sistema de controle) e das estratégias que facilitam a sua integração com outros sistemas prediais / The elevator system as mean for the vertical transport of people and goods is a fundamental component in the design of buildings. The availability and efficiency of this service must be object of careful analysis due to its influence on the performance and productivity of the building users' activities. In intelligent buildings, the purpose is the optimization of its structural and functional levels and where also the integration between all building systems accomplishes a fundamental role to reach these objectives. In this context, this work proposes a methodology for the modeling of elevator systems in these buildings, which consider your integration with others buildings systems. The approach developed in this work is based on the characterization of elevator systems as Discrete Event Systems (DES), since the dynamic behavior is defined through the discrete events and discrete states. The proposed methodology uses techniques, that are derived of interpreted Petri nets, which has been proven as an efficient tool for modeling, analysis and control of DES. In this context, systems are modeled in different levels of abstraction: a conceptual model which is obtained by using the PFS (Production Flow Schema) technique level, and a functional model by using MFG (Mark Flow Graph) and its extensions. The MFG abstraction level describes details in a functional form, where are preserved the description activities of previous levels. The methodology proposal confirmed to be useful and efficient to elevator systems modeling, when allowing the functional specification of the whole system (object of control and control system), and strategies that facilitate its integration with others building systems.

Well-behaved SNC covers well-behaved and various classes of FC (free-choice) and is not included in AC (asymmetric choice). An SNC allows internal choices and concurrency and hence is powerful for irodeling. Any SNC is bounded and its liveness conditions are simple. An integrated algorithm, has been presented for verification of a net being SNC and its liveness with polynomial time complexity. Scholars often need to verify properties on nets appearing in literatures. Verification by CAD tool is less desirable than that by hand due to the extra efforts to input the model aid learn to use the tool. We propose to manually search the maximum SNC component followed by locating bad siphons in an incremental manner. We then apply Lautenback's Maridng Condition (MC) for liveness to berify the property of liveness. But there are two drawbacks associated with the above MC. First, it guarantees only deadlock-freeness, and not necessary liveness. We have identified the structure cause for this and developed its livess conditions correspondingly. Second a net may be live even if the MC is not satisfied. We have identified the structure cause for this. The MC has been readjusted based on our proposed new theorey.

The presented work focuses on the theoretical and practical aspects concerning the design and development of a formal method to build a mission control system for autonomous underwater vehicles bringing systematic design principles for the formal description of missions using Petri nets. The proposed methodology compounds Petri net building blocks within it to de_ne a mission plan for which it is proved that formal properties, such as reachability and reusability, hold as long as these same properties are also guaranteed by each Petri net building block. To simplify the de_nition of these Petri net blocks as well as their composition, a high level language called Mission Control Language has been developed. Moreover, a methodology to ensure coordination constraints for teams of multiple robots as well as the de_nition of an interface between the proposed system and an on-board planner able to plan/replan sequences of prede_ned mission plans is included as well. Results of experiments with several real underwater vehicles and simulations involving an autonomous surface craft and an autonomous underwater vehicles are presented to show the system's capabilities. / El treball presentat en aquesta tesi està centrat en el disseny i desenvolupament d'un mètode formal per a construir un sistema de control de missió per a vehicles submarins autònoms, que aporta principis sistemàtics de disseny per a la descripció formal de missions. La metodologia proposada parteix d'uns blocs elementals de construcció, descrits mitjançant xarxes de Petri. La composició d'aquests blocs entre si genera un pla de missió per el qual diverses propietats, com ara accessibilitat o reutilització, són garantides sempre i quan aquestes mateixes propietats siguin també garantides per a cada un dels blocs elementals de construcció. Per simplificar la definició d'aquests blocs, així com per simplificar-ne la seva composició, s'ha desenvolupat un llenguatge d'alt nivell anomenat Mission Control Language. A més, s'ha inclòs una metodologia per assegurar la coordinació de restriccions entre equips de múltiples robots. També s'ha establert una interfície entre el sistema proposat i un planificador a bord del vehicle capaç de planificar/replanificar seqü_encies de plans de missió prèviament definits. Per tal de demostrar les capacitats del sistema, s'han presentat resultats d'experiments amb diversos vehicles submarins reals, així com simulacions amb vehicles autònoms submarins i en superfície.

An important consideration in discrete event dynamic systems control theory is the selection of a suitable modeling formalism that can capture the complex characteristics of the system and the capability to automatically synthesize a controller based on the system model. Net condition event systems are well suited for modeling complex discrete event dynamic systems owing to their input and output structure, which effectively captures the behavior of the physical devices to be monitored and/or controlled. To date, net condition event systems control models have not been extensively applied to highly automated manufacturing systems and there are few guidelines on how to automatically generate Programmable Logic Controller programming languages from net condition event systems models. This research automatically converted net condition event systems control models into Programmable Logic Controller programming language and evaluated the applicability of the proposed methodology in highly automated manufacturing systems using HAS-200 as a test bed.

Humans make mistakes, especially when faced to complex tasks, such as the construction of modern hardware or software. This thesis focuses on machine-assisted techniques to guarantee that computers behave correctly. Modern computer systems are large and complex. Automated formal verification stands as an alternative to testing or simulation to ensuring their reliability. It essentially proposes to employ computers to exhaustively check the system behavior. Unfortunately, automated verification suffers from the state-space explosion problem: even relatively small systems can reach a huge number of states. Using the right representation for the system behavior seems to be a key step to tackle the inherent complexity of the problems that automated verification solves. The verification of concurrent systems poses additional issues, as their analysis requires to evaluate, conceptually, all possible execution orders of their concurrent actions. Petri net unfoldings are a well-established verification technique for concurrent systems. They represent behavior by partial orders, which not only is natural but also efficient for automatic verification. This dissertation focuses on the verification of concurrent systems, employing Petri nets to formalize them, and studies two prominent verification techniques: model checking and fault diagnosis. We investigate the unfoldings of Petri nets extended with read arcs. The unfoldings of these so-called contextual nets seem to be a better representation for systems exhibiting concurrent read access to shared resources: they can be exponentially smaller than conventional unfoldings on these cases. Theoretical and practical contributions are made. We first study the construction of contextual unfoldings, introducing algorithms and data structures that enable their efficient computation. We integrate contextual unfoldings with merged processes, another representation of concurrent behavior that alleviates the explosion caused by non-determinism. The resulting structure, called contextual merged processes, is often orders of magnitude smaller than unfoldings, as we experimentally demonstrate. Next, we develop verification techniques based on unfoldings. We define SAT encodings for the reachability problem in contextual unfoldings, thus solving the problem of detecting cycles of asymmetric conflict. Also, an unfolding-based decision procedure for fault diagnosis under fairness constraints is presented, in this case only for conventional unfoldings. Finally, we implement our verification algorithms, aiming at producing a competitive model checker intended to handle realistic benchmarks. We subsequently evaluate our methods over a standard set of benchmarks and compare them with existing unfolding-based techniques. The experiments demonstrate that reachability checking based on contextual unfoldings outperforms existing techniques on a wide number of cases. This suggests that contextual unfoldings, and asymmetric event structures in general, have a rightful place in research on concurrency, also from an efficiency point of view.

Situation recognition is a process with the goal of identifying a priori defined situations in a flow of data and information. The purpose is to aid decision makers with focusing on relevant information by filtering out situations of interest. This is an increasingly important and non trivial problem to solve since the amount of information in various decision making situations constantly grow. Situation recognition thus addresses the information gap, i.e. the problem of finding the correct information at the correct time. Interesting situations may also evolve over time and they may consist of multiple participating objects and their actions. This makes the problem even more complex to solve. This thesis explores situation recognition and provides a conceptualization and a definition of the problem, which allow for situations of partial temporal definition to be described. The thesis then focuses on investigating how Petri nets can be used for recognising situations. Existing Petri net based approaches for recognition have some limitations when it comes to fulfilling requirements that can be put on solutions to the situation recognition problem. An extended Petri net based technique that addresses these limitations is therefore introduced. It is shown that this technique can be as efficient as a rule based techniques using the Rete algorithm with extensions for explicitly representing temporal constraints. Such techniques are known to be efficient; hence, the Petri net based technique is efficient too. The thesis also looks at the problem of learning Petri net situation templates using genetic algorithms. Results points towards complex dynamic genome representations as being more suited for learning complex concepts, since these allow for promising solutions to be found more quickly compared with classical bit string based representations. In conclusion, the extended Petri net based technique is argued to offer a viable approach for situation recognition since it: (1) can achieve good recognition performance, (2) is efficient with respect to time, (3) allows for manually constructed situation templates to be improved and (4) can be used with real world data to find real world situations. / <p>Anders Dahlbom is also affiliated to Skövde Artificial Intelligence Lab (SAIL), Information Fusion Research Program, Högskolan i Skövde</p>

This paper presents a class of Stochastic Petri Nets with concurrent transition firings. It is assumed that transitions occur in steps and that for every step each enabled transition decides probabilistically whether it wants to participate in the step or not. Among the transitions which what to participate in a step, a maximal number is chosen to perform the firing step. The observable behavior is defined and equivalence relations are introduced. The equivalence relations extend the well-known trace and bisimulation equivalences for systems with step semantics to Stochastik Petri Nets with concurrent transition firing. It is shown that the equivalence notions form a lattice of interrelations.