Les réseaux de transport multimodaux modernes sont essentiels pour la durabilité écologique et l’aisance économique des agglomérations urbaines, par conséquent aussi pour la qualité de vie de leurs habitants. D’ailleurs, le bon fonctionnement sur le plan de la compatibilité entre les différents services et lignes est essentiel pour leur acceptation, étant donné que (i) la plupart des trajets nécessitent des changements entre les lignes et que (ii) des investissements coûteux, dans le but de créer des liens plus directs avec la construction de nouvelles lignes ou l’extension de lignes existantes, ne sont pas à débattre. Une meilleure compréhension des interactions entre les modes et les lignes dans le contexte des transferts de passagers est ainsi d’une importance cruciale. Toutefois, comprendre ces transferts est singulièrement difficile dans le cas de situations inhabituelles comme des incidents de passagers et/ou si la demande dévie des plans statistiques à long terme. Ici le développement et l’intégration de modèles mathématiques sophistiqués peuvent remédier à ces inconvénients. À ce propos, la supervision via des modèles prévoyants représente un champ d’application très prometteur, analysée ici. La supervision selon des modèles prévoyants peut prendre différentes formes. Dans le présent travail, nous nous intéressons à l’analyse de l’impact basé sur des modèles de différentes actions, comme des départs en retard de certains véhicules après un arrêt, appliqué sur le fonctionnement du réseau de transport et sa gestion de situations de stress qui ne font pas partie des données statistiques. C’est pourquoi nous introduisons un nouveau modèle, un automate hybride avec une dynamique probabiliste, et nous montrons comment ce modèle profondément mathématique peut prédire le nombre de passagers dans et l’état de fonctionnement du véhicule en question du réseau de transport, d’abord par de simples estimations du nombre de tous les passagers et la connaissance exacte de l’état du véhicule au moment de l’incident. Ce nouvel automate réunit sous un même regard les passagers demandeurs de services de transport à parcours fixes ainsi que les véhicules capables de les assurer. Il prend en compte la capacité maximale et le fait que les passagers n’empruntent pas nécessairement des chemins efficaces, dont la représentation sous la forme d’une fonction de coût facilement compréhensible devient nécessaire. Chaque passager possède son propre profil de voyage qui définit un chemin fixe dans l’infrastructure du réseau de transport, et une préférence pour les différents services de transport sur son chemin. Les mouvements de véhicules sont inclus dans la dynamique du modèle, ce qui est essentiel pour l’analyse de l’impact de chaque action liée aux mouvements de véhicule. De surcroît, notre modèle prend en compte l’incertitude qui résulte du nombre inconnu de passagers au début et de passagers arrivant au fur et à mesure. Comparé aux modèles classiques d’automates hybrides, notre approche inspirée du style des réseaux de Pétri ne requiert pas le calcul de ces équations différentielles à la main. Ces systèmes peuvent être dérivés de la représentation essentiellement graphique d’une manière automatique pour le calcul en temps discret d’une prévision. Cette propriété de notre modèle réduit le risque de précisions faites par des humains et les erreurs qui en résulteraient. Après avoir introduit notre nouveau modèle, nous développons dans ce rapport également quelques éléments constitutifs sous la forme d'algorithmes qui visent les deux types d'impasses qui sont probables d'occurir pendant la simulation faisant un pronostic, c-à-d l'intégration numérique des systèmes de haute dimension d'équations différentielles et l'explosion combinatoire de son état discret. En plus, nous prouvons la faisabilité des calculs et nous montrons les bénéfices prospectifs de notre approche dans la forme de quelques tests simplistes et quelques cas plus réalistes. / Without any doubt, modern multimodal transportation systems are vital to the ecological sustainability and the economic prosperity of urban agglomerations, and in doing so to the quality of life of their many inhabitants. Moreover it is known that a well-functioning interoperability of the different modes and lines in such networked systems is key to their acceptance given the fact that (i) many if not most trips between different origin/destination pairs require transfers, and (ii) costly infrastructure investments targeting the creation of more direct links through the construction of new or the extension of existing lines are not open to debate. Thus, a better understanding of how the different modes and lines in these systems interact through passenger transfers is of utmost importance. However, acquiring this understanding is particularly tricky in degraded situations where some or all transportation services cannot be provided as planned due to e.g. some passenger incident, and/or where the demand for these scheduled services deviates from any statistical long term-plannings. Here, the development for and integration of sophisticated mathematical models into the operation of such systems may provide remedy, where model-predictive supervision seems to be one very promising area of application which we consider here. Model-predictive supervision can take several forms. In this work, we focus on the model-based impact analysis of different actions, such as the delayed departure of some vehicle from a stop, applied to the operation of the considered transportation system upon some downgrading situation occurs which lacks statistical data. For this purpose, we introduce a new stochastic hybrid automaton model, and show how this mathematically profound model can be used to forecast the passenger numbers in and the vehicle operational state of this transportation system starting from estimations of all passenger numbers and an exact knowledge of the vehicle operational state at the time of the incident occurrence. Our new automaton model brings under the same roof, all passengers who demand fixed-route transportation services, and all vehicles which provide them. It explicitly accounts for all capacity-limits and the fact that passengers do not necessarily follow efficient paths which must be mapped to some simple to understand cost function. Instead, every passenger has a trip profile which defines a fixed route in the infrastructure of the transportation system, and a preference for the different transportation services along this route. Moreover, our model does not abstract away from all vehicle movements but explicitly includes them in its dynamics, which latter property is crucial to the impact analysis of any vehicle movement-related action. In addition our model accounts for uncertainty; resulting from unknown initial passenger numbers and unknown passenger arrival flows. Compared to classical modelling approaches for hybrid automata, our Petri net-styled approach does not require the end user to specify our model's many differential equations systems by hand. Instead, all these systems can be derived from the model's predominantly graphical specification in a fully automated manner for the discrete time computation of any forecast. This latter property of our model in turn reduces the risk of man-made specification and thus forecasting errors. Besides introducing our new model, we also develop in this report some algorithmic bricks which target two major bottlenecks which are likely to occur during its forecast-producing simulation, namely the numerical integration of the many high-dimensional systems of stochastic differential equations and the combinatorial explosion of its discrete state. Moreover, we proof the computational feasibility and show the prospective benefits of our approach in form of some simplistic test- and some more realistic use case.

Indiana University-Purdue University Indianapolis (IUPUI) / This thesis proposed an algorithm that can find optimized Petri nets from given observation sequences according to some rules of optimization. The basic idea of this algorithm is that although the length of the observation sequences can keep growing, we can think of the growing as periodic and algorithm deals with fixed observations at different time. And the algorithm developed has polynomial complexity. A segment of example code programed according to this algorithm has also been shown. Furthermore, we modify this algorithm and it can check whether a Petri net could fit the observation sequences after several steps. The modified algorithm could work in constant time. These algorithms could be used in optimization of the control systems and communication networks to simplify their structures.

Indiana University-Purdue University Indianapolis (IUPUI) / In the healthcare industry, several modern patient identification and patient matching systems have been introduced. Most of these implement patient identification by their first, middle and last names. They also use Social Security Number and other similar national identifiers. These methods may not work for many developing and underdeveloped countries where identifying a patient is a challenge with highly redundant and interchangeable first and last names of the patient, this is aggravated by the absence of a national identification system. In order to make the patient identification more efficient, Muzima, an interface of OpenMRS (Open source medical records system) introduced an additional identifier, fingerprint, through a module to the system. Ordinary and Time Petri nets are used to analyze this module. Chapter 1 introduces Muzima fingerprint module and describes the workflow of this interface followed by the related work, importance and applications of Petri nets. Chapter 2 introduces Ordinary and Time Petri nets using examples. Chapter 3 discusses about the mathematical modeling of the Muzima Fingerprint module using Petri nets. Chapter 4 explains the qualitative and quantitative analysis done on the Muzima fingerprint module. Chapter 5 discusses about the programming and simulation done to prove the theoretical results obtained. Chapter 6 provides the conclusion and future work for the thesis.

[pt] Business Process Management é a ciência de observar como o trabalho é realizado em determinada organização garantindo produtos consistentes e se aproveitando de oportunidades de melhoria. Atualmente, boa parte dos processos são realizados em frameworks, muitos com armazenamento de arquivos de log, no qual é disponibilizada uma grande quantidade de informação que pode ser explorada de diferentes formas e com diferentes objetivos, área denominada como Mineração de Processos. Apesar de muitos desses dados contemplarem o modo como os recursos são alocados para cada atividade, o foco maior dos trabalhos nessa área é na descoberta do processo e na verificação de conformidade do mesmo. Nesta dissertação é proposto um modelo em petri net que incorpora a alocação de recurso, de forma a poder explorar as propriedades deste tipo de modelagem, como por exemplo a definição de todos os estados possíveis. Como aplicação do modelo, realizou-se um estudo comparativo entre duas políticas, uma mais especialista, de alocação de recurso, e outra mais generalista usando simulações de Monte Carlo com distribuição de probabilidade exponencial para o início de novos casos do processo e para estimação do tempo de execução do par recurso atividade. Sendo assim, para avaliação de cada política foi usado um sistema de pontuação que considera o andamento do processo e o tempo total de execução do mesmo. / [en] Business Process Management is the science of observing how the work is performed in a given organization ensuring consistent products and seeking opportunities for improvement. Currently, most of the processes are performed in frameworks, many with log files, in which a large amount of data is available. These data can be explored in different ways and with different objectives, giving rise to the Process Mining area. Although many of these data informs how resources are allocated for each activity, the major focus of previous work is on the discovery process techniques and process compliance. In this thesis a petri net model that incorporates resource allocation is proposed exploring the properties of this type of modeling, such as the definition of all possible states. As a model validation, it is applied in a comparative study between two resource allocation policies, one considering the expertise of each resource and other with a more generalist allocation. The arrival of new cases and the resource-activity pair execution time were estimated by Monte Carlo simulations with exponential probability distribution. Thus, for the evaluation of each policy a scoring system was used considering the progress of the process and the total execution time.

Presently information systems are increasingly penetrating to our daily life. Recently it is relevant to integrate the newest technologies. In that way traditional system becomes “smart” who are more economical, optimal, and self-sufficient. The biggest problem is to make a model of “smart” system. There were analyzed modeling methods, heating and cooling control systems in this job. Mathematical model for heating and cooling controller using timed Petri nets was presented. According to analyzed problems it was made verification with Matlab during experimental phase. There was made comparison evaluation of mathematical model made with timed Petri nets and fuzzy logic.

Made available in DSpace on 2016-06-02T19:06:15Z (GMT). No. of bitstreams: 1 6263.pdf: 2838494 bytes, checksum: 852261a244b09c47cc828522a799cc8d (MD5) Previous issue date: 2014-06-26 / Petri Net (PN) is a graphical mathematical tool used to create models that provide a formal specification of systems, creating the possibility of running behavior analysis and property verification. PN models can be used to model several system types, for example, Manufacturing Systems. In general, using PN to model systems with too many characteristics cause the so-called state-space explosion problem, in other words, a great element profusion in the model. In order to mitigate the referred problem researchers developed reduction rules to synthetize models. Reduced models maintain original system properties and can be easily analyzed and simulated. A method to automate reduction rules application is proposed on the present research. A Genetic Algorithm heuristic is responsible for applying six reductions rules on Place-Transition Petri Nets given as input. The proposed algorithm, presented as a Matlab toolbox, may contribute when simulating and running property verification methodologies on Petri Net models. / Rede de Petri (RP) é uma ferramenta de modelagem com rigor matemático usada para especificar e formalizar sistemas e suas características. Modelos de RP podem ser avaliados quanto à seu comportamento dinâmico e suas propriedades estruturais. Diversos tipos de modelos podem ser especificados usando RP s, por exemplo, modelos de Sistemas de Manufatura. De maneira geral, modelos de sistemas complexos sofrem do problema da grande profusão de elementos. Esse problema é um limitante para diversas metodologias de verificação de propriedades e simulação de comportamento dinâmico dos modelos. Frequentemente metodologias baseadas em regras de redução são propostas para superar o problema da grande profusão de elementos. O presente trabalho apresenta uma ferramenta para automatizar a aplicação de regras de redução em modelos de RP. Um conjunto de regras foi selecionado para montar uma base de regras de redução e uma heurística baseada em algoritmos genéticos foi criada para aplicar reduções em modelos de RP Lugar-Transição. Os resultados obtidos mostraram que a ferramenta proposta, apresentada como uma toolbox do Matlab, pode ser utilizada para auxiliar no processo de análise, simulação e verificação de propriedades de sistemas modelados por meio de RP s.

Dentre as várias abordagens consagradas para análise de desempenho de algoritmos em termos de tempo de execução, destacam-se, por exemplo, a análise assintótica, as técnicas de recorrências e a análise probabilística. Entretanto, há algoritmos que apresentam certas peculiaridades que tornam o uso dessas técnicas puramente matemáticas de avaliação de desempenho inadequadas ou excessivamente árduas. É o caso, por exemplo, de algoritmos cujo tempo de execução pode variar significativamente para um mesmo dado de entrada em função da dinâmica de execução. O mesmo acontece no caso de algoritmos distribuídos em que, dependendo da complexidade da política de distribuição utilizada, a avaliação por meio de métodos analíticos do efeito de um gradual incremento de processadores no seu tempo de execução pode tornar-se impraticável. Em situações como essas, a fim de evitar a alta complexidade matemática envolvida na análise de desempenho desses algoritmos, algumas alternativas baseadas em métodos empíricos ou em modelagem visual vêm sendo adotada pelos pesquisadores. Contudo, ambas alternativas apresentam inconvenientes: no caso dos métodos empíricos, eles requerem a implementação dos algoritmos analisados, o que tem um efeito perverso particularmente no caso dos algoritmos distribuídos, uma vez que eles demandam a aquisição prévia de recursos de hardware dispendiosos de multi-processamento antes mesmo de saber se a proposta de distribuição investigada, de fato, vale a pena. Já as abordagens baseadas em modelos visuais atualmente utilizadas (baseadas em grafos, autômatos e Unified Modeling Language - UML) não contam com os recursos dinâmicos necessários para lidar com a avaliação do tempo de execução dos algoritmos. Neste cenário, o presente trabalho propõe uma abordagem visual formal para avaliar o tempo de execução de algoritmos baseada em simulações automáticas de modelos de Redes de Petri Coloridas Hierárquicas (RdPCH) no ambiente gráfico CPN Tools. A abordagem proposta é validada por meio de cálculo dos seguintes parâmetros associados aos algoritmos usados como estudo de caso: a função de complexidade, o tempo de execução real e, no caso dos algoritmos distribuídos, o speedup e a eficiência. Foram usados como estudos de caso os seguintes três relevantes algoritmos de busca usados nos agentes da Inteligência Artificial com a finalidade de definir as ações mais apropriadas que tais agentes devem executar de modo a cumprir seu objetivo, com êxito, em um ambiente em que um oponente tenta minimizar suas chances de sucesso: os algoritmos seriais Minimax e Alpha-Beta; e o algoritmo distribuído PVS. Os resultados obtidos confirmam a correção da abordagem proposta. / Among the various approaches established for analyzing the performance of algorithms in terms of runtime, one can highlight as examples, the asymptotic analysis, recurrence techniques, and probabilistic analysis. However, there are algorithms that present certain peculiarities, which make the use of these purely mathematical performance evaluation techniques inadequate or excessively difficult. This is the case of algorithms for which the runtime varies significantly for the same input data, due to its execution dynamics. The same happens in the case of distributed algorithms, where depending on the complexity of the distribution policy being used, the evaluation by means of analytical methods concerning the effect of a gradual increase in processors on runtime can become impractical. In situations such as these, in order to avoid the high mathematical complexity involved in the performance analysis, researchers have adopted alternatives based on empirical methods or visual modeling. However, both alternatives have drawbacks: in the case of empirical methods, they require the implementation of analyzed algorithms, which has a perverse effect especially in the case of distributed algorithms. This occurs, as they demand the acquisition beforehand of expensive multiprocessing hardware resources before knowing if the distribution proposal under investigation is in fact viable. On the other hand, those approaches based on visual models currently under use (based on graphs, automata and Unified Modeling Language) one notes that does not contain the necessary dynamic resources for dealing with the runtime evaluation of algorithms. In this scenario, the present study proposes a formal visual approach, in order to evaluate the algorithm runtime based on automatic simulations of Hierarchical Colored Petri Net models in the CPN Tools graphic environment. The proposed approach is validated through the calculation of the following parameters associated with the algorithms being used as a case study: the complexity function, real runtime, and in the case of distributed algorithms, speedup and efficiency. The cases studies were based on three relevant search algorithms used in the agents of the Artificial Intelligence, with the aim of defining the most appropriate actions that these agents need to execute in order to fulfil their objective, in an environment where the opponent tries to minimize their chances of success. The algorithms under consideration were the serial algorithms Minimax and Alpha-Beta; and the PVS distributed algorithm. The obtained results confirm the correction of the proposed approach. / Tese (Doutorado)

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / The majorities of industrial systems may be considered as dynamic hybrid systems, that is, described by variables in the continuous and discrete domains. Therefore, due to the need to obtain high quality products with losses minimization, to have safer and environmental friendly process operation, is what justies the development of tools for evaluating fault propagation eects. In this work, some tools for the representation of dynamic hybrid systems were studied in order to address the abnormal behavior propagation. The rst tools are Petri nets that allow a qualitative mathematical representation, the analysis of the models and supply useful information on the structure and the dynamic behavior of the system. Another tool is the signed directed graph - SDG that includes the mechanisms of fault propagation and the development of a theory of modeling based on the knowledge of complicated systems. In this context, it was presented the qualitative modeling of dynamic systems by using Petri nets and SDG, with the occurrence of faults and the evaluation of their propagation during process operation. These techniques were applied to Chemical Engineering problems such as mixing tanks and batch reactors for Petri nets, tank systems and faulty continuous reactors with the use of SDG. In those processes, simulations were performed and the faults eects were evaluated for several operational scenarios. SDGs were also used to determine the fault propagation path, with the evaluation of each aected process variable of interest both in open and closed-loop operation. / A maioria dos sistemas industriais pode ser classificada como pertencente _a classe de sistemas híbridos dinâmicos, ou seja, sistemas compostos por variáveis no domínio contínuo e discreto. Assim, devido à necessidade de se obter produtos de alta qualidade com mínimo de perdas possíveis, operar com segurança respeitando o meio ambiente, gerenciar ou tolerar falhas é que se tem a necessidade do desenvolvimento de ferramentas de investigação dos efeitos de falhas em processos. Neste trabalho foram estudadas algumas ferramentas para a representação de sistemas híbridos dinâmicos com a finalidade de representar o comportamento anormal desses sistemas. Uma dessas ferramentas _e a rede de Petri que permite a representação matemática, análise dos modelos e fornece informações úteis sobre a estrutura e o comportamento dinâmico dos sistemas modelados. Outra ferramenta estudada são os grafos orientados - SDG (Signed Directed Graph) que incluem os mecanismos de propagação de falhas e o desenvolvimento de uma teoria de modelagem baseada no conhecimento de sistemas. Nesse contexto, foram apresentados nesta dissertação a modelagem qualitativa dos sistemas discretos utilizando redes de Petri e SDG, com a ocorrência de falhas e a avaliação da sua propagação nos processos. Essas técnicas foram aplicadas em problemas simples da Engenharia Química como tanques de mistura e reator em batelada para redes de Petri e sistemas com um e três tanques e CSTR para o SDG. Em cada um dos processos estudados foram feitas as simulações acopladas aos modelos qualitativos em diversos cenários de falhas. Com isso comparam-se os resultados para o sistema operando sob diversos cenários e avaliam-se as informações do modelo qualitativo. Para ilustrar a aplicação das técnicas investigadas, esse trabalho avaliou, com a utilização de SDG, os caminhos de propagação das falhas, obtendo as variáveis afetadas em cada cenário operacional investigado. / Mestre em Engenharia Química

Made available in DSpace on 2015-04-11T14:03:05Z (GMT). No. of bitstreams: 1 Romulo Devezas Freitas.pdf: 818067 bytes, checksum: 48f8f5869d720e92b7dcb341d59a27a3 (MD5) Previous issue date: 2005-12-01 / No contexto restritivo dos sistemas embarcados de tempo real críticos, a geração de código escalonado mostra-se uma maneira eficiente de proporcionar previsibilidade e demais garantias exigidas por tais sistemas. Entretanto, a geração de código escalonado pressupõe conhecimento prévio da ordem em que as tarefas devem ser executadas. Assim, a síntese de escalonamento é peça chave em um metodologia para síntese de software neste ambiente. Este trabalho apresenta uma abordagem para síntese de escalonamento estático utilizando semântica de passo máximo em redes de Petri com temporização. Este trabalho está inserido no contexto de uma metodologia para síntese de software de sistemas embarcados de tempo real críticos. Em linhas gerais, essa metodologia compreende (i) a especificação do sistema; (ii) a transformação da especificação em um modelo formal baseado em rede de Petri; (iii) a síntese de escalonamento baseada neste modelo e (iv) a geração de código escalonado. No escopo da síntese de escalonamento, este trabalho propõe um conjunto de definições que caracterizam uma estratégia de disparo de passo máximo sobre redes de Petri com temporização, e aplica estas definições na síntese de escalonamento estático para sistemas embarcados de tempo real críticos. Os resultados obtidos nos experimentos apresentados indicam a viabilidade da aplicação da semântica de passo máximo proposta, demonstrando melhorias de desempenho relacionadas ao tempo de execução e ao volume de informação processada. Adicionalmente, além da apresentação de uma abordagem de passo máximo para síntese de escalonamento, este trabalho ainda propõe algumas melhorias e aperfeiçoamentos na metodologia e no modelo adotados como base.

Presently, most spacecraft are controlled from ground involving activities such as up-linking the schedule of daily operations and monitoring health parameters. These activities lead to a cognitive overload on human operators. Imaging/science opportunities are lost, if any discrepancies occur during the execution of pre-planned sequences. Consequently, advanced space exploration systems for future needs demand on-board intelligence and autonomy. This thesis attempts to solve the problem of providing an adequate degree of autonomy in future generation of spacecraft. The autonomous spacecraft accept high-level goals from users and make decisions on-board to generate detailed command schedules satisfying stringent constraints posed by the harsh environment of the space, visibility criteria and scarce on-board resources. They reconfigure themselves in case of any failure and re-plan when needed. Autonomy concepts are derived in the context of complex systems by drawing analogy to living organisms and social organisations. A general autonomy framework may be defined with a six level structure comprising of the following capabilities -reflexes, awareness, self-regulation, self-healing, self-adaptation and self-evolution. A generic and reusable software architecture is proposed using hybrid multi-agent systems, which are arranged in a hierarchical manner using two types of decomposition viz. stratum and layer. The software architecture of the autonomous spacecraft is modeled as a stratified agent with a deliberative stratum, which achieves adaptive behaviour and a reactive stratum, which achieves reactive behaviour. Each individual agent has a generic structure comprising of perception, action, communication and knowledge components. It achieves the specialist capability through model-based reasoning. The knowledge models encompass: Planning knowledge describing higher-level goals, task structure and method of achieving the goals, Control knowledge encompassing the static and dynamic models of the spacecraft and Diagnostic knowledge incorporating the cause-effect relationships. The deliberative stratum is capable of planning in different time horizons and is, in turn, organised into a hierarchical agent system with three layers corresponding to different time horizons. It is composed of a long-term, medium-term and short-term planning agents, focusing on strategic issues, spacecraft level resources and specific spacecraft states respectively. The power of Petri nets is exploited for knowledge modeling as well as for plan representation. The ability of Petri nets to represent causality, concurrency and conflict relations explicitly makes it an excellent tool for representing the planning problem. Hierarchical Timed Petri Net is chosen for our modeling, since it captures the temporal requirements of the real-time spacecraft operations as well as facilitates the modeling of the system with multiple levels of abstraction. The necessary primitives for the plan representation are defined. In hierarchical modeling using Petri nets, refinement is done by a compound (high-level) transition. A compound transition models either a complex activity, which corresponds to high-level operation on spacecraft or a method, which corresponds to the agent capability. At the lowest layer, a transition in the plan represents a primitive command to the spacecraft, such as ‘switch on camera’. The Petri net unfolding technique, which is a partial order approach, is applied to derive the plans from the dynamic knowledge models. This tackles the problem of combinatorial explosion. A hierarchical planning approach is followed, in which the abstract plan is recursively decomposed using the unfolding technique and refined by way of exercising the appropriate decisions in each layer. The reactive stratum is configured with three peer level agents. The control agent executes the command schedule and has the capability for reflex action. Structural properties of Petri nets are exploited by the execution-monitoring agent and the diagnostic agent for system level diagnosis. Fault tree method is applied for fine granularity diagnosis. The resultant architecture is a cost-effective solution, since it permits reusability of knowledge models across similar missions. The knowledge models are formally verified for ensuring the absence of deadlocks, buffer overflows, recoverability and detection of unreachable modules using Petri net properties such as reachability, liveness, boundedness, safeness, reversibility and home state. The high-risk components are subjected to safety property verification, which makes the system rugged. The hierarchical composition of Petri net models (which are independently verified), preserves liveness and boundedness characteristics and thus ensuring the reliability of the integrated models. This, in turn, ensures that reliable plans are generated on-board using these good quality models. The models of the system components viz. partial order plan, conditional plan, dynamic world model, reflex model, resource model and the hierarchical models are developed and demonstrated using HPSIM and Moses Tool Suite, using examples from spacecraft domain. The long-term planning agent, with hierarchical world models, for handling high-level goals is developed and simulated using Moses Tool Suite. The plan generation using unfolding approach is demonstrated using VIPTool, which has the partial order analysis capability. In summary, the main contributions include (a) Definition of a general framework for spacecraft autonomy; (b) design of a generic and reusable architecture for autonomous spacecraft using hybrid multi-agent concepts; (c) unified knowledge representation and reasoning using Petri nets across various strata/layers; (d) application of Petri net unfolding technique in a hierarchical manner for plan generation; (e) use of structural properties of Petri nets for fault identification and location; (f) verification and validation of Petri net models using Petri net properties and (g) simulation and demonstration of the system components viz. partial order plan, conditional plan, dynamic world model, reflex model, resource model and hierarchical models, by developing examples from spacecraft domain, using HPSIM and Moses Tool Suite and demonstration of plan generation using unfolding technique using VIPTool.