Biological network data is plentiful with practically every experimental methodology giving 'network views' into cellular function and behavior. Bioinformatic screens that yield network data include, for example, genome-wide deletion screens, protein-protein interaction assays, RNA interference experiments, and methods to probe metabolic pathways. Efficient and comprehensive computational approaches are required to model these screens and gain insight into the nature of biological networks. This thesis presents three new algorithms to model and mine network datasets. First, we present an algorithm that models genome-wide perturbation screens by deriving relations between phenotypes and subsequently using these relations in a local manner to derive genephenotype relationships. We show how this algorithm outperforms all previously described algorithms for gene-phenotype modeling. We also present theoretical insight into the convergence and accuracy properties of this approach. Second, we define a new data mining problem–constrained minimal separator mining—and propose algorithms as well as applications to modeling gene perturbation screens by viewing the perturbed genes as a graph separator. Both of these data mining applications are evaluated on network datasets from S. cerevisiae and C. elegans. Finally, we present an approach to model the relationship between metabolic pathways and operon structure in prokaryotic genomes. In this approach, we present a new pattern class—biclusters over domains with supplied partial orders—and present algorithms for systematically detecting such biclusters. Together, our data mining algorithms provide a comprehensive arsenal of techniques for modeling gene perturbation screens and metabolic pathways. / Ph. D.

Les systèmes distribués ont réussi à étendre la technologie de l’information à un public plus large, en termes d’emplacement et de nombre. Cependant, ces systèmes géo-répliqués doivent être évolutifs afin de répondre aux demandes toujours croissantes. De plus, le système doit pouvoir traiter les messages dans un ordre équivalent à celui de leur création afin d’éviter des effets indésirables. L’exécution suivant des ordres partiels fournit un ordonnancement d’événements que tous les nœuds suivront, ce qui permet donc le traitement des messages dans un ordre adéquat. Un système qui applique un ordre partiel simplifie le développement des applications distribuées et s’assure que l’utilisateur final n’observera pas des comportements défiant la causalité. Dans cette thèse, nous présentons des modèles statistiques pour différentes contraintes d’ordre partiel, en utilisant différentes distributions de modèles de latence. Étant donné un modèle de latence, qui donne le temps qu’il faut pour qu’un message passe d’un nœud à un autre, notre modèle s’appuie sur lui pour donner le temps supplémentaire qu’il faut pour appliquer un ordre partiel spécifique. Nous avons proposé les modèles suivants. Tout d’abord, dans une communication entre un et plusieurs nœuds, la probabilité que le message soit délivré dans tous les nœuds avant un temps donné. Deuxièmement, après la réception d’un message, la probabilité que tous les autres nœuds aient exécuté ce message avant temps donné. Troisièmement, dans une communication de un à plusieurs nœuds, la probabilité que le message soit arrivé à au moins un sous-ensemble d’entre eux avant un temps donné. Quatrièmement, l’ordre FIFO ou causal qui détermine si un message est prêt à être livré, dans un nœud ou plusieurs. Tout cela favorise la compréhension du comportement des systèmes distribués en présence d’ordres partiels. En outre, en utilisant cette connaissance, nous avons construit un algorithme qui utilise ces modèles de comportement du réseau pour établir un système de livraison causal fiable. Afin de valider nos modèles, nous avons développé un outil de simulation qui permet d’exécuter des scénarios adaptés à nos besoins. Nous pouvons définir les différents paramètres du modèle de latence, le nombre de clients et les charges de travail des clients. Cette simulation nous permet de comparer les valeurs générées de façon aléatoire pour chaque configuration spécifique avec les résultats prévus de notre modèle. Une des applications qui peuvent tirer profit de notre modèle, est un algorithme de livraison causale fiable. Il utilise l’information causale pour détecter les éléments manquants et réduit le besoin d’acquittement de message en contactant d’autres répliques seulement lorsque le message est supposé manquant. Cette information est fournie par notre modèle, qui définit les temporisateurs d’attente en fonction des statistiques du réseau et de la consommation des ressources. Enfin, cette application a été testée dans le même simulateur que les modèles, avec des résultats prometteurs, puis évaluée dans une expérience réelle utilisant Amazon EC2 comme plate-forme / Distributed systems have managed to extend technology to a broader audience, in both terms of location and numbers. However these geo-replicated systems need to be scalable in order to meet the ever growing demands. Moreover, the system has to be able to process messages in an equivalent order that they were created to avoid unwanted side effects. Partial order enforcement provides an ordering of events that all nodes will follow therefore processing the messages in an adequate order. A system that enforces a partial order simplifies the challenge of developing distributed applications, and ensures that the end-user will not observe causality defying behaviors. In this thesis we present models for different partial order enforcements, using different latency model distributions. While a latency model, which yields the time it takes for a message to go from one node to another, our model builds on it to give the additional time that it takes to enforce a given partial order. We have proposed the following models. First, in a one to many nodes communication, the probability for the message to be delivered in all the nodes before a given time. Second, in a one to many nodes communication from the receivers, the probability that all the other nodes have delivered the message after a given time of him receiving it. Third, in a one to many nodes communication, the probability that the message has arrived to at least a subset of them before a given time. Fourth, applying either FIFO or Causal ordering determining if a message is ready for being delivered, in one node or many. All of this furthers the understanding of how distributed systems with partial orders behave. Furthermore using this knowledge we have built an algorithm that uses the insight of network behavior to provide a reliable causal delivery system. In order to validate our models, we developed a simulation tool that allows to run scenarios tailored to our needs. We can define the different parameters of the latency model, the number of clients, and the clients workloads. This simulation allows us to compare the randomly generated values for each specific configuration with the predicted outcome from our model. One of the applications that can take advantage of our model, is a reliable causal delivery algorithm. It uses causal information to detect missing elements and removes the need of message acknowledgment by contacting other replicas only when the message is assumed missing. This information is provided by our model, that defines waiting timers according to the network statistics and resource consumption. Finally this application has been both tested in the same simulator as the models, with promising results, and then evaluated in a real-life experiment using Amazon EC2 for the platform

This thesis is concerned with the formulation of a suitable notion of monotonicity of discrete and continuous-time dynamical systems on Lie groups and homogeneous spaces. In a linear space, monotonicity refers to the property of a system that preserves an ordering of the elements of the space. Monotone systems have been studied in detail and are of great interest for their numerous applications, as well as their close connections to many physical and biological systems. In a linear space, a powerful local characterisation of monotonicity is provided by differential positivity with respect to a constant cone field, which combines positivity theory with a local analysis of nonlinear systems. Since many dynamical systems are naturally defined on nonlinear spaces, it is important to seek a suitable adaptation of monotonicity on such spaces. However, the question of how one can develop a suitable notion of monotonicity on a nonlinear manifold is complicated by the general absence of a clear and well-defined notion of order on such a space. Fortunately, for Lie groups and important examples of homogeneous spaces that are ubiquitous in many problems of engineering and applied mathematics, symmetry provides a way forward. Specifically, the existence of a notion of geometric invariance on such spaces allows for the generation of invariant cone fields, which in turn induce notions of conal orders. We propose differential positivity with respect to invariant cone fields as a natural and powerful generalisation of monotonicity to nonlinear spaces and develop the theory in this thesis. We illustrate the ideas with numerous examples and apply the theory to a number of areas, including the theory of consensus on Lie groups and order theory on the set of positive definite matrices.

<p>The method of forcing is widely used in set theory to obtain&nbsp;various consistency proofs. Complete Boolean algebras play the main role&nbsp;in applications of forcing. Therefore it is useful to define games on Boolean&nbsp;algebras that characterize their properties important for the method. The&nbsp;most investigated game is Jech&rsquo;s distributivity game, such that the first&nbsp;player has the winning strategy iff the algebra is not (&omega;, 2)-distributive.&nbsp;We define another game characterizing the collapsing of the continuum to&nbsp;&omega;, prove several sufficient conditions for the second player to have a winning&nbsp;strategy, and obtain a Boolean algebra on which the game is undetermined.&nbsp;</p> / <p>Forsing je metod &scaron;iroko kori&scaron;ćen u teoriji skupova za dokaze konsistentnosti. Kompletne&nbsp; Bulove algebre igraju glavnu ulogu u primenama forsinga. Stoga je korisno definisati igre na Bulovim algebrama koje karakteri&scaron;u njihove osobine od značaja za taj metod. Najbolje proučena je Jehova igra, koja ima osobinu da prvi igrač ima pobedničku strategiju akko algebra nije (&omega;, 2)-distributivna. U tezi defini&scaron;emo jo&scaron; jednu igru, koja karakteri&scaron;e kolaps kontinuuma na &omega;, dokazujemo nekoliko dovoljnih uslova da bi drugi igra&scaron; imao pobedničku strategiju, i konstrui&scaron;emo Bulovu algebru na kojoj je igra neodređena.</p>

No description available.

CoordenaÃÃo de AperfeiÃoamento de NÃvel Superior / A noÃÃo de DecomposiÃÃo em Ãrvore foi introduzida por Robertson e Seymour em sua sÃrie de artigos sobre menores de grafos e pode ser definida, intuitivamente, como uma organizaÃÃo dos vÃrtices e arestas do grafo em uma estrutura de Ãrvore, sendo a largura da decomposiÃÃo igual ao tamanho do maior subconjunto de vÃrtices relacionado a um nà desta estrutura menos um. A largura mÃnima de uma decomposiÃÃo em Ãrvore de um grafo G à chamada de largura em Ãrvore de G. VÃrios problemas difÃceis podem ser resolvidos em tempo polinomial, dada uma decomposiÃÃo em Ãrvore de largura limitada, como, por exemplo, Ciclo Hamiltoniano, Conjunto Independente MÃximo, Isomorfismo, ColoraÃÃo de VÃrtices, etc. A complexidade dos algoritmos que resolvem tais problemas sÃo geralmente exponenciais na largura da decomposiÃÃo fornecida. Logo, à esperado que encontrar uma decomposiÃÃo de largura mÃnima seja um problema difÃcil. De fato, Arnborg, Corneil e Proskurowski [2] mostraram que o problema à NP - difÃcil. O problema de encontrar a largura em Ãrvore de um grafo qualquer à o objeto de estudo da presente dissertaÃÃo de mestrado. Uma restriÃÃo desse problema à o de decidir, para um inteiro k fixo, se a largura em Ãrvore de G à no mÃximo k. Apresentamos a prova de que o problema para k fixo pode ser resolvido polinomialmente. Na Ãltima dÃcada foram propostas vÃrias heurÃsticas que fornecem limites superiores para o problema [3, 10], heurÃsticas para o cÃlculo de limites inferiores [6, 8, 11], alÃm de mÃtodos enumerativos [5] e algoritmos aproximativos [1, 7, 4]. PorÃm, nenhum resultado obtido pode ser considerado bom, uma vez que nÃo existe um benchmark para o qual se conhece a largura em Ãrvore e os limites inferiores e superiores tÃm se mostrado muito distantes. AlÃm disso, o algoritmo enumerativo existente mostrou-se ineficiente mesmo para o problema de decisÃo com k fixo em valores pequenos (por exemplo, k = 4) [12]. à neste quadro que propomos um mÃtodo enumerativo para o problema. Na verdade, abordamos o problema de triangularizaÃÃo, que à equivalente ao problema de decomposiÃÃo em Ãrvore. Isso nos permitiu a proposta de uma nova representaÃÃo para uma soluÃÃo do problema que utiliza o conceito de ordens totais. Uma vez que as soluÃÃes podem assim ser representadas, um algoritmo que enumere as extensÃes totais de uma dada ordem parcial pode ser utilizado para enumerar todas as soluÃÃes do problema, bastando que fornecemos uma ordem que contenha apenas os pares reflexivos vv, onde v à um vÃrtice do grafo de entrada. O mÃtodo enumerativo proposto à uma modificaÃÃo do algoritmo de CorrÃa e Szwarcfiter [9]. Esta modificaÃÃo faz com que apenas as extensÃes totais da ordem fornecida seja enumerada. O algoritmo apresenta duas principais vantagens com relaÃÃo ao mÃtodo enumerativo proposto por Bodlaender e Kloks: pode ser utilizado juntamente com o mÃtodo âbranch and boundâ; e pode enumerar um sub-espaÃo de soluÃÃes, o que pode ser Ãtil caso se conheÃa algumas relaÃÃes existentes na soluÃÃo Ãtima, ou mesmo para investigar determinados sub-espaÃos de soluÃÃes. Implementamos e testamos o algoritmo proposto, aplicando o mÃtodo âbranch and boundâ e restringindo o espaÃo de soluÃÃes. As ordens parciais utilizadas para definir os sub-espaÃos explorados foram obtidas baseando-se nas heurÃsticas de limite superior que utilizam rotulaÃÃo. Infelizmente, nÃo obtivemos bons resultados, pois, mesmo restringindo o espaÃo de busca, a quantidade de nÃs gerados da Ãrvore de âbranch and boundâ foi muito grande, excedendo a quantidade de memÃria disponÃvel da mÃquina utilizada para os testes. No texto da dissertaÃÃo apresentamos tambÃm um estudo da complexidade do problema, um algoritmo para calcular uma decomposiÃÃo em Ãrvore Ãtima de um grafo cordal, alÃm das vÃrias heurÃsticas para o cÃlculo de limites superiores e inferiores existentes. AlÃm disso, implementamos e testamos as heurÃsticas de limite superior que utilizam rotulaÃÃo e uma heurÃstica GRASP, tendo sido o primeiro estudo de uma aplicaÃÃo da meta-heurÃstica GRASP para o problema de decomposiÃÃo em Ãrvore. / The notion of Tree Decomposition was introduced by Robertson and Seymour in their seris of articles about graph minors and can be intuitively seen as an organization of the vertices and edges of the graph in a tree structure, being the treewidth equal to the size of the largest subset of vertices minus one. The minimum treewidth over all tree decompositions of a graph gives us the treewidth of the graph. Many hard problems can be polinomially solved for a graph G if a tree decomposition with bounded treewidth of G is given. For instance, hamiltonian cycle, maximum independent set isomorphism, vertex coloring, etc. The complexity of the algorithm that solves such problems are generally exponential on the width of the given tree decomposition. So, we can expect that finding a tree decomposition of minimum width is hard. In fact, Arnborg, Corneil and Proskurowski [2] showed that the problem os NP-hard. The problem of finding the treewidth of a graph is the subject of this thesis. The decision variation of the problem is, given a graph G and for a fixed integer k, deciding if the treewidth of G is at most k. We discuss a proof that the decision problem can be polynomially solved. In the last decade were proposed many heuristics for computing upper bounds [3, 10], lower bounds [6, 8, 11], enumeration methods [5] and approximative algorithms [1, 7, 4]. However, none of these results can be considered as good ones, since there is no benchmarks for with the treewidth is known, as well as the difference between the lower and upper bounds for the existing benchmarks is very large. Additionally, the enumeration method was showed to be inefficient even for the decision problem with k fixed in small values (e.g., k = 4) [12]. So, we propose another enumeration method for the problem that can be used along with branch and bound techniques. Actually, we work with the triangulation problem that is equivalent to the tree decomposition problem. We propose a new representation of a solution, wich uses the concept of total orders. Once a solution ca be represented like that, an algorithm that enumerates all the total extensions of a given partial order can be used to enumerate all solutions for the tree decomposition problem, as long as we offer the partial order containing only the reflexive pairs vv, where v is a vertex of the input graph. The proposed enumeration method is a modification of the CorrÃa and Szwarcfiter algorithm [9]. This modification allows only the total extensions to be enumerated. The algorithm presents two principal advantages over the Bodlander and Kloks method: it can be used in conjunction with the Branch and Bound method; and it can enumerate a subspace of solutions, what can be useful if we know some existing relations in an optimal solution, or even to investigate such subspaces in order to characterize them. We have implemented and tested the proposed algorithm, applying the branch and bound method and restricting the subspace of solutions. The partial orders used to define the explored subspaces were obtained based on the labeling heuristics for finding upper bounds. Unfortunately, we did not obtain good results because, even when we restricted the subspace of solutions to be searched, the number of nodes generated in the branch and bound tree was too large, exceeding the machineâs memory capacity. In the text, we also present the proof of the NP-hardness of the problem, an algorithm to compute an optimal decompostion of a chordal graph, and also the many existing heuristics to compute lower and upper bounds. In addition, we implemented and tested the labeling heuristics for upper bounds and a GRASP heuristic, being the first application of a GRASP meta-heuristic to the problem.

SILVA, Ana Shirley Ferreira da. Um estudo computacional sobre o problema de decomposição de grafos em árvore. 2005. 103 f. : Dissertação (mestrado) - Universidade Federal do Ceará, Centro de Ciências, Departamento de Computação, Fortaleza-CE, 2005. / Submitted by guaracy araujo (guaraa3355@gmail.com) on 2016-05-24T19:54:20Z No. of bitstreams: 1 2005_dis_asfsilva.pdf: 965121 bytes, checksum: 0620082b39fd950bff00ce625f59f846 (MD5) / Approved for entry into archive by guaracy araujo (guaraa3355@gmail.com) on 2016-05-24T19:54:44Z (GMT) No. of bitstreams: 1 2005_dis_asfsilva.pdf: 965121 bytes, checksum: 0620082b39fd950bff00ce625f59f846 (MD5) / Made available in DSpace on 2016-05-24T19:54:44Z (GMT). No. of bitstreams: 1 2005_dis_asfsilva.pdf: 965121 bytes, checksum: 0620082b39fd950bff00ce625f59f846 (MD5) Previous issue date: 2005 / The notion of Tree Decomposition was introduced by Robertson and Seymour in their seris of articles about graph minors and can be intuitively seen as an organization of the vertices and edges of the graph in a tree structure, being the treewidth equal to the size of the largest subset of vertices minus one. The minimum treewidth over all tree decompositions of a graph gives us the treewidth of the graph. Many hard problems can be polinomially solved for a graph G if a tree decomposition with bounded treewidth of G is given. For instance, hamiltonian cycle, maximum independent set isomorphism, vertex coloring, etc. The complexity of the algorithm that solves such problems are generally exponential on the width of the given tree decomposition. So, we can expect that finding a tree decomposition of minimum width is hard. In fact, Arnborg, Corneil and Proskurowski [2] showed that the problem os NP-hard. The problem of finding the treewidth of a graph is the subject of this thesis. The decision variation of the problem is, given a graph G and for a fixed integer k, deciding if the treewidth of G is at most k. We discuss a proof that the decision problem can be polynomially solved. In the last decade were proposed many heuristics for computing upper bounds [3, 10], lower bounds [6, 8, 11], enumeration methods [5] and approximative algorithms [1, 7, 4]. However, none of these results can be considered as good ones, since there is no benchmarks for with the treewidth is known, as well as the difference between the lower and upper bounds for the existing benchmarks is very large. Additionally, the enumeration method was showed to be inefficient even for the decision problem with k fixed in small values (e.g., k = 4) [12]. So, we propose another enumeration method for the problem that can be used along with branch and bound techniques. Actually, we work with the triangulation problem that is equivalent to the tree decomposition problem. We propose a new representation of a solution, wich uses the concept of total orders. Once a solution ca be represented like that, an algorithm that enumerates all the total extensions of a given partial order can be used to enumerate all solutions for the tree decomposition problem, as long as we offer the partial order containing only the reflexive pairs vv, where v is a vertex of the input graph. The proposed enumeration method is a modification of the Corrêa and Szwarcfiter algorithm [9]. This modification allows only the total extensions to be enumerated. The algorithm presents two principal advantages over the Bodlander and Kloks method: it can be used in conjunction with the Branch and Bound method; and it can enumerate a subspace of solutions, what can be useful if we know some existing relations in an optimal solution, or even to investigate such subspaces in order to characterize them. We have implemented and tested the proposed algorithm, applying the branch and bound method and restricting the subspace of solutions. The partial orders used to define the explored subspaces were obtained based on the labeling heuristics for finding upper bounds. Unfortunately, we did not obtain good results because, even when we restricted the subspace of solutions to be searched, the number of nodes generated in the branch and bound tree was too large, exceeding the machine’s memory capacity. In the text, we also present the proof of the NP-hardness of the problem, an algorithm to compute an optimal decompostion of a chordal graph, and also the many existing heuristics to compute lower and upper bounds. In addition, we implemented and tested the labeling heuristics for upper bounds and a GRASP heuristic, being the first application of a GRASP meta-heuristic to the problem. / A noção de Decomposição em árvore foi introduzida por Robertson e Seymour em sua série de artigos sobre menores de grafos e pode ser definida, intuitivamente, como uma organização dos vértices e arestas do grafo em uma estrutura de árvore, sendo a largura da decomposição igual ao tamanho do maior subconjunto de vértices relacionado a um nó desta estrutura menos um. A largura mínima de uma decomposição em árvore de um grafo G é chamada de largura em árvore de G. Vários problemas difíceis podem ser resolvidos em tempo polinomial, dada uma decomposição em árvore de largura limitada, como, por exemplo, Ciclo Hamiltoniano, Conjunto Independente Máximo, Isomorfismo, Coloração de Vértices, etc. A complexidade dos algoritmos que resolvem tais problemas são geralmente exponenciais na largura da decomposição fornecida. Logo, é esperado que encontrar uma decomposição de largura mínima seja um problema difícil. De fato, Arnborg, Corneil e Proskurowski [2] mostraram que o problema é NP - difícil. O problema de encontrar a largura em árvore de um grafo qualquer é o objeto de estudo da presente dissertação de mestrado. Uma restrição desse problema é o de decidir, para um inteiro k fixo, se a largura em árvore de G é no máximo k. Apresentamos a prova de que o problema para k fixo pode ser resolvido polinomialmente. Na última década foram propostas várias heurísticas que fornecem limites superiores para o problema [3, 10], heurísticas para o cálculo de limites inferiores [6, 8, 11], além de métodos enumerativos [5] e algoritmos aproximativos [1, 7, 4]. Porém, nenhum resultado obtido pode ser considerado bom, uma vez que não existe um benchmark para o qual se conhece a largura em árvore e os limites inferiores e superiores têm se mostrado muito distantes. Além disso, o algoritmo enumerativo existente mostrou-se ineficiente mesmo para o problema de decisão com k fixo em valores pequenos (por exemplo, k = 4) [12]. É neste quadro que propomos um método enumerativo para o problema. Na verdade, abordamos o problema de triangularização, que é equivalente ao problema de decomposição em árvore. Isso nos permitiu a proposta de uma nova representação para uma solução do problema que utiliza o conceito de ordens totais. Uma vez que as soluções podem assim ser representadas, um algoritmo que enumere as extensões totais de uma dada ordem parcial pode ser utilizado para enumerar todas as soluções do problema, bastando que fornecemos uma ordem que contenha apenas os pares reflexivos vv, onde v é um vértice do grafo de entrada. O método enumerativo proposto é uma modificação do algoritmo de Corrêa e Szwarcfiter [9]. Esta modificação faz com que apenas as extensões totais da ordem fornecida seja enumerada. O algoritmo apresenta duas principais vantagens com relação ao método enumerativo proposto por Bodlaender e Kloks: pode ser utilizado juntamente com o método “branch and bound”; e pode enumerar um sub-espaço de soluções, o que pode ser útil caso se conheça algumas relações existentes na solução ótima, ou mesmo para investigar determinados sub-espaços de soluções. Implementamos e testamos o algoritmo proposto, aplicando o método “branch and bound” e restringindo o espaço de soluções. As ordens parciais utilizadas para definir os sub-espaços explorados foram obtidas baseando-se nas heurísticas de limite superior que utilizam rotulação. Infelizmente, não obtivemos bons resultados, pois, mesmo restringindo o espaço de busca, a quantidade de nós gerados da árvore de “branch and bound” foi muito grande, excedendo a quantidade de memória disponível da máquina utilizada para os testes. No texto da dissertação apresentamos também um estudo da complexidade do problema, um algoritmo para calcular uma decomposição em árvore ótima de um grafo cordal, além das várias heurísticas para o cálculo de limites superiores e inferiores existentes. Além disso, implementamos e testamos as heurísticas de limite superior que utilizam rotulação e uma heurística GRASP, tendo sido o primeiro estudo de uma aplicação da meta-heurística GRASP para o problema de decomposição em árvore.

Nous avons étudié dans cette thèse une approche discrète de la synthèse de contrôleurs pour les systèmes hybrides permettant la manipulation de dynamiques non-linéaires : les états sont regroupés dans une partition finie au prix d'une sur-approximation non déterministe de la relation de transition. Nous avons développé des algorithmes permettant de réduire l'explosion du nombre d'états due à la discrétisation en exploitant des propriétés des systèmes ODE. Ces algorithmes sont basés sur une approche hiérarchique du problème de la synthèse en le résolvant pour des sous problèmes et en utilisant ces résultats pour réduire l'espace d'états global. Nous avons aussi combiné des objectifs de vivacité et de sécurité pour s'approcher d'une stabilisation. Des résultats implémentés sur un prototype viennent montrer l'intérêt de cette approche.Pour la vérification, nous avons étudié le problème du model checking d'automates temporisés basé sur la résolution SAT. Nous avons exploré des solutions alternatives pour le codage des réductions SAT basées sur des exécutions parallèles de transitions indépendantes. Alors qu'une telle optimisation a déjà été étudiée pour les systèmes discrets, une approche intuitive pour les automates temporisés serait de considérer que des transitions en parallèle ont lieu au même instant (synchrones). Toutefois il est possible de relâcher cette condition et nous avons montré trois sémantiques différentes pour les séquences temporisées avec des transitions parallèles. Nous montrons la correction des sémantiques et décrivons des résultats expérimentaux réalisés avec notre prototype. / We consider a discretization based approach to controller synthesis of hybrid systems that allows to handle non-linear dynamics. In such an approach, states are grouped together in a finite index partition at the price of a non-deterministic over approximation of the transition relation. The main contribution of this work is a technique to reduce the state explosion generated by the discretization: exploiting structural properties of ODE systems, we propose a hierarchical approach to the synthesis problem by solving it first for sub problems and using the results for state space reduction in the full problem. A secondary contribution concerns combined safety and liveness control objectives that approximate stabilization. Results implemented on a prototype show the benefit of this approach. For the verification, we study the model checking problem of timed automata based on SAT solving. Our work investigates alternative possibilities for coding the SAT reductions that are based on parallel executions of independent transitions. While such an optimization has been studied for discrete systems, its transposition to timed automata poses the question of what it means for timed transitions to be executed “in parallel”. The most obvious interpretation is that the transitions in parallel take place at the same time (synchronously). However, it is possible to relax this condition. On the whole, we define and analyse three different semantics of timed sequences with parallel transitions. We prove the correctness of the proposed semantics and report experimental results with a prototype implementation.

Pattern Discovery, a popular paradigm in data mining refers to a class of techniques that try and extract some unknown or interesting patterns from data. The work carried out in this thesis concerns frequent episode mining, a popular framework within pattern discovery, with applications in alarm management, fault analysis, network reconstruction etc. The data here is in the form of a single longtime-ordered stream of events. The pattern of interest here, namely episode, is basically a set of event-types with a partial order on it. The task here is to unearth all patterns( episodes here) which have a frequency above a user-defined threshold irrespective of pattern size. Most current discovery algorithms employ a level-wise a priori-based method for mining, which basically adopts a breadth-first search strategy of the space of all episodes. The episode literature has seen multiple ways of defining frequency with each definition having its own set of merits and demerits. The main reason for different frequencies definitions being proposed is that, in general, counting all occurrences of a set of episodes is computationally very expensive. The first part of the thesis gives a unified view of all the apriori-based discovery algorithms for serial episodes(associated with a total order)under these various frequencies. Specifically, the various existing counting algorithms can be viewed as minor modifications of each other. We also provide some novel proofs of correctness for some of the serial episode counting schemes, which in turn can be generalized to episodes with general partial orders. Our unified view helps us derive quantitative relationships between different frequencies. We also discuss all the anti-monotonicity properties satisfied by the various frequencies, a crucial information needed for the candidate generation step. The second part of the thesis proposes discovery algorithms for episodes with general partial orders, for which no algorithms currently exist in literature. The discovery algorithm proposed is apriori-based and generalizes the existing serial and parallel (associated with a trivial order) episode algorithms. The discovery algorithm is a level-wise procedure involving the steps of candidate generation and counting a teach level. In the context of general partial orders, a major problem in a priori-based discovery is to have an efficient candidate generation scheme. We present a novel candidate generation algorithm for mining episodes with general partial orders. The counting algorithm design for general partial order episodes draws ideas from the unified view of counting for serial episodes, presented in the first part of the work. We formally show the correctness of the proposed candidate generation and counting steps for general partial orders. The proposed candidate generation algorithm is flexible enough to be able to mine in certain specialized classes of partial orders (satisfying what we call maximal sub episode property), of which, the serial and parallel class of episodes are two specific instances. Our algorithm design initially restricts itself to the class of general partial order episodes called injective episodes wherein repeated event-types are not allowed. We then generalize this to a larger class of episodes called chain episodes, where episodes can have some repeated event types. The class of chain episodes contains all (including non-injective) serial and parallel episodes and thus our method properly generalizes the existing methods for serial and parallel episode discovery. We also discuss some problems in extending our algorithms to episodes beyond the class of chain episodes. Also, we demonstrate that frequency alone is not a sufficient enough interestingness measure for episodes with unrestricted partial orders. To address this issue, we propose an additional measure called bidirectional evidence to assess interestingness which, along with frequency is found to be extremely effective in unearthing interesting patterns. In the frequent episode framework, the choice of thresholds are most often user-defined and arbitrary. To address this issue, the last part of the work deals with assessing significance of partial order episodes in a statistical sense based on ideas from classical hypothesis testing. We declare an episode to be significant if its observed frequency in the data stream is large enough to be very unlikely, under a random i.i.d model .The key step in the significance analysis involves the mean and variance computation of the the time between successive occurrences of the pattern. This computation can be reformulated as, solving for the mean and variance of the first visit time to a particular stat e in an associated Markov chain. We use a generating function approach to solve for this mean and variance. Using this and a Gaussian approximation to the frequency random variable, we can now calculate a frequency threshold for any partial order episode, beyond which we infer it to be significant. Our significance analysis for general partial order episodes generalizes the existing significance analysis of serial episode patterns. We demonstrate on synthetic data the effectiveness of our significance thresholds.

This thesis is concerned with the modeling and the analysis of distributedreal-time systems. In distributed systems, components evolve partlyindependently: concurrent actions may be performed in any order, withoutinfluencing each other and the state reached after these actions does notdepends on the order of execution. The time constraints in distributed real-timesystems create complex dependencies between the components and the events thatoccur. So far, distributed real-time systems have not been deeply studied, andin particular the distributed aspect of these systems is often left aside. Thisthesis explores distributed real-time systems. Our work on distributed real-timesystems is based on two formalisms: time Petri nets and networks of timedautomata, and is divided into two parts.In the first part, we highlight the differences between centralized anddistributed timed systems. We compare the main formalisms and their extensions,with a novel approach that focuses on the preservation of concurrency. Inparticular, we show how to translate a time Petri net into a network of timedautomata with the same distributed behavior. We then study a concurrency relatedproblem: shared clocks in networks of timed automata can be problematic when oneconsiders the implementation of a model on a multi-core architecture. We showhow to avoid shared clocks while preserving the distributed behavior, when thisis possible.In the second part, we focus on formalizing the dependencies between events inpartial order representations of the executions of Petri nets and time Petrinets. Occurrence nets is one of these partial order representations, and theirstructure directly provides the causality, conflict and concurrency relationsbetween events. However, we show that, even in the untimed case, some logicaldependencies between event occurrences are not directly described by thesestructural relations. After having formalized these logical dependencies, wesolve the following synthesis problem: from a formula that describes a set ofruns, we build an associated occurrence net. Then we study the logicalrelations in a simplified timed setting and show that time creates complexdependencies between event occurrences. These dependencies can be used to definea canonical unfolding, for this particular timed setting.