• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 783
  • 623
  • 555
  • 15
  • 15
  • 3
  • Tagged with
  • 1979
  • 1805
  • 1800
  • 1768
  • 266
  • 255
  • 185
  • 181
  • 177
  • 175
  • 163
  • 152
  • 150
  • 141
  • 127
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
91

Automatic program analysis using Max-SMT

Larraz Hurtado, Daniel 28 July 2015 (has links)
This thesis addresses the development of techniques to build fully-automatic tools for analyzing sequential programs written in imperative languages like C or C++. In order to do the reasoning about programs, the approach taken in this thesis follows the constraint-based method used in program analysis. The idea of the constraint-based method is to consider a template for candidate invariant properties, e.g., linear conjunctions of inequalities. These templates involve both program variables as well as parameters whose values are initially unknown and have to be determined so as to ensure invariance. To this end, the conditions on inductive invariants are expressed by means of constraints (hence the name of the approach) on the unknowns. Any solution to these constraints then yields an invariant. In particular, if linear inequalities are taken as target invariants, conditions can be transformed into arithmetic constraints over the unknowns by means of Farkas' Lemma. In the general case, a Satisfiability Modulo Theories (SMT) problem over non-linear arithmetic is obtained, for which effective SMT solvers exist. One of the novelties of this thesis is the presentation of an optimization version of the SMT problems generated by the constraint-based method in such a way that, even when they turn out to be unsatisfiable, some useful information can be obtained for refining the program analysis. In particular, we show in this work how our approach can be exploited for proving termination of sequential programs, disproving termination of non-deterministic programs, and do compositional safety verification. Besides, an extension of the constraint-based method to generate universally quantified array invariants is also presented. Since the development of practical methods is a priority in this thesis, all the techniques have been implemented and tested with examples coming from academic and industrial environments. The main contributions of this thesis are summarized as follows: 1. A new constraint-based method for the generation of universally quantified invariants of array programs. We also provide extensions of the approach for sorted arrays. 2. A novel Max-SMT-based technique for proving termination. Thanks to expressing the generation of a ranking function as a Max-SMT optimization problem where constraints are assigned different weights, quasi-ranking functions -functions that almost satisfy all conditions for ensuring well-foundedness- are produced in a lack of ranking functions. Moreover, Max-SMT makes it easy to combine the process of building the termination argument with the usually necessary task of generating supporting invariants. 3. A Max-SMT constraint-based approach for proving that programs do not terminate. The key notion of the approach is that of a quasi-invariant, which is a property such that if it holds at a location during execution once, then it continues to hold at that location from then onwards. Our technique considers for analysis strongly connected subgraphs of a program's control flow graph and thus produces more generic witnesses of non-termination than existing methods. Furthermore, it can handle programs with unbounded non-determinism. 4. An automated compositional program verification technique for safety properties based on quasi-invariants. For a given program part (e.g., a single loop) and a postcondition, we show how to, using a Max-SMT solver, an inductive invariant together with a precondition can be synthesized so that the precondition ensures the validity of the invariant and that the invariant implies the postcondition. From this, we build a bottom-up program verification framework that propagates preconditions of small program parts as postconditions for preceding program parts. The method recovers from failures to prove validity of a precondition, using the obtained intermediate results to restrict the search space for further proof attempts. / Esta tesis se centra en el desarrollo de técnicas para construir herramientas altamente automatizadas que analicen programas secuenciales escritos en lenguajes imperativos como C o C++. Para realizar el razonamiento sobre los programas, la aproximación tomada en esta tesis se basa en un conocido método basado en restricciones utilizado en análisis de progamas. La idea de dicho método consiste en considerar plantillas que expresen propiedades invariantes candidatas, p.e., conjunciones de desigualdades lineales. Estas plantillas contienen tanto variables del programa como parámetros cuyos valores son inicialmente desconocidos y tienen que ser determinados para garantizar la invariancia. Para este fin, las condiciones sobre invariantes inductivos son expresadas mediante restricciones sobre los valores desconocidos. Cualquier solución a estas restricciones llevan a un invariante. En particular, si desigualdades lineales son los invariantes objetivo, las condiciones pueden ser transformadas en restricciones aritméticas sobre los valores desconocidos mediante el lema de Farkas. En el caso general, un problema de Satisfactibilidad Modulo Teorías (SMT) sobre aritmética no-lineal es obtenido, para el cual existen resolvedores eficientes. Una de las novedades de esta tesis es la presentación de una versión de optimización de los problemas SMT generados por el método tal que, incluso cuando son insatisfactibles, se puede obtener cierta información útil para refinar el análisis del programa. En particular, en este trabajo se muestra como la aproximación tomada puede usarse para probar terminación de programas, probar la no terminación de programas y realizar verificación por partes de la corrección de programas. Además, también se describe una extensión del método basado en restricciones para generar invariantes universalmente cuantificados sobre arrays. Debido a que el desarrollo de métodos prácticos es una prioridad en esta tesis, todas las técnicas han sido implementadas y probadas con ejemplos extraídos del entorno académico e industrial. Las principales contribuciones de esta tesis pueden resumirse en: 1. Un nuevo método basado en restricciones para la generación de invariantes universalmente cuantificados sobre arrays. También se explica extensiones del método para aplicarlo a arrays ordenados. 2. Un técnica novedosa basada en Max-SMT para probar terminación. Gracias a expresar la generación de funciones de ranking como problemas de optimización Max-SMT, donde a las restricciones se les asigna diferentes pesos, se generan cuasi-funciones de ranking, funciones que casi satisfacen todas las condiciones que garantizan la existencia de una relación bien fundada, en ausencia de funciones de ranking. Además, Max-SMT facilita la combinación del proceso de construcción de un argumento de terminación con la tarea habitualmente necesaria de generar invariantes de apoyo. 3. Un método basado en restricciones y Max-SMT para probar que un programa no termina. El concepto clave del método es el de cuasi-invariante, que es una propiedad tal que si se cumple una vez en un punto del programa durante la ejecución, entonces continúa cumpliendose en ese punto desde entonces en adelante. Nuestra técnica considera en su análisis subgrafos fuertemente conexos del grafo de control de flujo del programa y produce testigos de no terminación más genéricos que otros métodos existentes. Además, es capaz de tratar programas con no determinismo. 4. Una técnica automatizada de verificación por partes de propiedades de corrección de un programa basada en cuasi-invariantes. Dado una parte de un programa (p.e., un único bucle) con una postcondición, se muestra como, usando Max-SMT, puede sintetizarse un invariante inductivo junto a una precondición que garantiza la validez del invariante y que el invariante implica la postcondición. Apartir de esto, se describe una infraestructura de verificación de programas de abajo a arriba que propaga precondiciones.
92

Action Selection in Cooperative Robot Soccer using Case-Based Reasoning

Ros Espinoza, Raquel 31 March 2008 (has links)
La tasca de dissenyar el mecanisme de presa de decisions d'un equip de robots és un gran repte, no només per la complexitat de l'entorn en el qual els robots realitzen les seves tasques, que comporta incertesa, dinamicitat i imprecisió, sinó també perquè la coordinació entre els robots s'ha de tenir en compte a l'hora de dissenyar el mecanisme. Els robots han de ser conscients de les accions dels altres robots per tal de cooperar i assolir satisfactòriament els objectius de l'equip. Aquesta tesi doctoral presenta una novedosa aproximació basada en casos per la selecció d'accions i la coordinació de tasques cooperatives en equips de robots. Aquesta aproximació s'ha aplicat i avaluat en un domini molt representatiu, com és el del futbol robòtic, tot i que les idees presentades són aplicables a altres dominis com les operacions de rescat, l'exploració d'entorns desconeguts i la vigilància submarina, entre d'altres. El procés de selecció proposa un cas per reutilitzar, avaluant els casos candidats amb una sèrie de criteris per tal de tenir en compte les característiques d'un entorn real, incloent-hi la presència d'adversaris, que és un factor clau en el domini del futbol robòtic. A diferència dels sistemes de raonament basats en casos clàssics, la reutilització del cas consisteix en l'execució d'un conjunt d'accions per part d'un equip de robots. Per tant, des de la perspectiva multi- robot, el sistema ha d'incloure un mecanisme per tal de decidir qui fa què i com. En aquesta tesi, es presenta una arquitectura multi-robot juntament amb un mecanisme de coordinació per tal d'atacar aquests reptes. Hem validat experimentalment l'aproximació tant en simulació com amb robots reals. L'experimentació ha permès comprovar que l'aproximació presentada assoleix els objectius de la tesi, és a dir, el disseny de comportaments d'un equip de robots cooperatius. Així mateix, els resultats obtinguts també mostren els avantatges d'utilitzar una estratègia col·laborativa en entorns en els quals el component adversari juga un paper important, en contrast amb comportaments individualistes. / Designing the decision-making engine of a team of robots is a challenging task, not only due to the complexity of the environment where the robots usually perform their task, which include uncertainty, dynamism and imprecision, but also because the coordination of the team must be included in this design. The robots must be aware of other robots' actions to cooperate and to successfully achieve their common goal. Besides, decisions must be made in real-time and with limited computational resources.This thesis contributes a novel case-based approach for action selection and coordination in joint multi-robot tasks in real environments. This approach has been applied and evaluated in the representative domain of robot soccer, although the ideas presented are applicable to domains such as disaster rescue operations, exploration of unknown environments and underwater surveillance, among others. The retrieval process proposes a case to reuse, evaluating the candidate cases through different measures to overcome the real world characteristics, including the adversarial component which is a key ingredient in the robot soccer domain. Unlike classical case- based reasoning engines, the case reuse consists in the execution of a set of actions through a team of robots. Therefore, from the multi- robot perspective, the system has to include a mechanism for deciding who does what and how. In this thesis, we propose a multi- robot architecture along with a coordination mechanism to address these issues. We have validated the approach experimentally both in a simulated environment and with real robots. The results showed that our approach achieves the expected goals of the thesis, i.e. designing the behavior of a cooperative team of robots. Moreover, the experimentation also showed the advantages of using collaborative strategies in contrast to individualistic ones, where the adversarial component plays an important role.
93

Coding and Decoding Design of ECOCs for Multi-class Pattern and Object Recognition

Escalera Guerrero, Sergio 07 September 2008 (has links)
Molts problemes de la vida quotidiana estan plens de decisions multi-classe. En l'àmbit del Reconeixement de Patrons, s'han proposat moltes tècniques d'aprenentatge que treballen sobre problemes de dos classes. No obstant, la extensió de classificadors binaris al cas multi-classe és una tasca complexa. En aquest sentit, Error-Correcting Output Codes (ECOC) han demostrat ser una eina potent per combinar qualsevol nombre de classificadors binaris i així modelar problemes multi-classe. No obstant, encara hi ha molts punts oberts sobre les capacitats del framework d'ECOC. En aquesta tesis, els dos estats principals d'un disseny ECOC són analitzats: la codificació i la decodificació. Es presenten diferents alternatives de dissenys dependents del domini del problema. Aquests dissenys fan ús del coneixement del domini del problema per minimitzar el nombre de classificadors que permeten obtenir un alt rendiment de classificació. Per altra banda, l'anàlisi de la codificació de dissenys d'ECOC es emprada per definir noves regles de decodificació que prenen total avantatja de la informació provinent del pas de la codificació. A més a més, com que classificacions exitoses requereixen rics conjunts de característiques, noves tècniques de detecció/extracció de característiques es presenten i s'avaluen en els nous dissenys d'ECOC. L'avaluació de la nova metodologia es fa sobre diferents bases de dades reals i sintètiques: UCI Machine Learning Repositori, símbols manuscrits, senyals de trànsit provinents de sistemes Mobile Mapping, imatges coronàries d'ultrasò, imatges de la Caltech Repositori i bases de dades de malats de Chagas. Els resultats que es mostren en aquesta tesis mostren que s'obtenen millores de rendiment rellevants tant a la codificació com a la decodificació dels dissenys d'ECOC quan les noves regles són aplicades. / Many real problems require multi-class decisions. In the Pattern Recognition field, many techniques have been proposed to deal with the binary problem. However, the extension of many 2-class classifiers to the multi-class case is a hard task. In this sense, Error-Correcting Output Codes (ECOC) demonstrated to be a powerful tool to combine any number of binary classifiers to model multi-class problems. But there are still many open issues about the capabilities of the ECOC framework. In this thesis, the two main stages of an ECOC design are analyzed: the coding and the decoding steps. We present different problem-dependent designs. These designs take advantage of the knowledge of the problem domain to minimize the number of classifiers, obtaining a high classification performance. On the other hand, we analyze the ECOC codification in order to define new decoding rules that take full benefit from the information provided at the coding step. Moreover, as a successful classification requires a rich feature set, new feature detection/extraction techniques are presented and evaluated on the new ECOC designs. The evaluation of the new methodology is performed on different real and synthetic data sets: UCI Machine Learning Repository, handwriting symbols, traffic signs from a Mobile Mapping System, Intravascular Ultrasound images, Caltech Repository data set or Chaga's disease data set. The results of this thesis show that significant performance improvements are obtained on both traditional coding and decoding ECOC designs when the new coding and decoding rules are taken into account.
94

Contributions to mobile agent protection from malicious hosts

Garrigues Olivella, Carles 21 July 2008 (has links)
La utilització d'agents mòbils en sistemes distribuïts comporta diverses avantatges. Les avantatges més freqüentment citades inclouen: reducció de la càrrega de la xarxa, decrement de la latència de les comunicacions, adaptació dinàmica, i millor suport per dispositius mòbils amb connexions intermitents, entre d'altres. No obstant, els beneficis oferts pels agents mòbils no han estat suficients per estimular el seu ús generalitzat. La raó principal per la qual els agents mòbils no han estat àmpliament adoptats encara, a pesar dels seus avantatges tecnològics, és que aquesta tecnologia comporta certs riscos de seguretat. S'han dut a terme molts avenços en la seguretat, la fiabilitat i la eficiència dels agents mòbils, però hi ha problemes de seguretat que encara romanen sense solució.El treball principal d'aquesta tesi gira en torn a la protecció dels agents mòbils contra els hostes maliciosos. Per tal de proporcionar una solució a alguns dels problemes de seguretat actuals, en primer lloc, s'ha presentat un protocol de protecció d'itineraris que suporta agents que viatgen lliurament. Els protocols de protecció d'itineraris proposats fins ara limiten la capacitat de l'agent de migrar a voluntat. Per tant, aquesta tesi presenta un protocol que permet als agents descobrir noves plataformes en temps d'execució, de tal manera que les aplicacions poden aprofitar tots els avantatges proporcionats per la tecnologia dels agents mòbils.En segon lloc, s'ha presentat un protocol que protegeix els agents mòbils d'atacs de re-execució externs. Els atacs de re-execució externs estan basats en tornar a enviar l'agent a la seva plataforma destí, per tal de forçar-lo a re-executar part del seu itinerari. El protocol proposat evita aquest tipus d'atacs sense limitar la capacitat de l'agent de visitar certes plataformes repetidament.Les solucions de seguretat presentades en aquesta tesi es basen en el fet que en molts, si no en la majoria, dels escenaris basats en agents mòbils podem trobar plataformes de confiança. Mitjançant la incorporació de plataformes de confiança en l'itinerari de l'agent, les solucions proposades proporcionen un compromís equilibrat entre seguretat i flexibilitat.Per tal de promoure el desenvolupament d'aplicacions basades en agents mòbils segurs, aquesta tesi també presenta un entorn de desenvolupament que facilita la implementació dels protocols de protecció d'agents proposats, així com altres solucions de seguretat. / Several advantages have been identified in using mobile agents in distributed systems. The most frequently cited advantages include: reduction of network load, decrease in communication latency, dynamic adaptation, and better support for mobile devices with intermittent connections, among others. However, the benefits offered by mobile agents have not been sufficient to stimulate their widespread deployment. The main reason why mobile agents have not been widely adopted yet, despite their technological benefits, is their inherent security risks. Many breakthroughs have been achieved in the security, reliability and efficiency of mobile agents, but there are security issues still remaining unsolved.The core work of this thesis revolves around the protection of mobile agents against malicious hosts. In order to provide a solution to some of the current security issues, first of all, an itinerary protection protocol is presented that supports free-roaming agents. Itinerary protection protocols proposed to date limit the agent's ability to migrate at will. Therefore, this thesis presents a protocol that allows agents to discover new platforms at runtime, so that applications can take full advantage of the benefits provided by mobile agent itineraries.Second, a protocol is presented that protects mobile agents against external replay attacks. External replay attacks are based on resending the agent to another platform, so as to force the reexecution of part of its itinerary. The proposed protocol counters this kind of attacks without limiting the agent's ability to visit certain platforms repeatedly.The security solutions presented in this thesis are based on the fact that trusted platforms can be found in many, if not most, mobile agent-based scenarios. By incorporating trusted platforms in the agent's itinerary, the proposed solutions provide a balanced trade-off between security and flexibility.In order to promote the development of secure mobile agent-based applications, this thesis also presents a development environment that facilitates the implementation of the proposed agent protection protocols as well as other security solutions.
95

Contribution to the study of alliances in graphs

González Yero, Ismael 13 December 2010 (has links)
Contribution to the study of alliances in graphs.ResumenEn este trabajo se estudian propiedades matemáticas de las alianzas (defensivas, ofensivas y duales) en grafos. Entre los temas tratados se destacan los siguientes:· Se estudian las alianzas en grafos producto. Específicamente, se obtienen relaciones entre las alianzas en grafos producto Cartesiano y las alianzas en los factores. · Se estudia las particiones de un grafo en alianzas. En particular, se hacen estimaciones del número máximo de conjuntos pertenecientes a una partición del grafo en k-alianzas. Además, se estudian las relaciones existentes entre dicho número y otros invariantes del grafo, tales como el orden, la medida, el número cromático, el número isoperimétrico y la medida de bipartición. · Se estudian las propiedades matemáticas de los conjuntos libres de alianzas y los cubrimientos de alianzas. En particular, se obtienen cotas tensas para la cardinalidad máxima de un conjunto libre de alianzas y la cardinalidad mínima de un cubrimiento de alianzas. Además, se caracterizan grafos que son libres de k-alianzas defensivas.· Se introduce el concepto de alianza frontera y se estudian algunas de sus propiedades. Entre los resultados obtenidos se destaca una condición necesaria para la existencia de una partición de un grafo regular en dos alianzas fronteras. · Se estudian las alianzas ofensivas globales y sus relaciones con algunos conjuntos característicos en grafos, tales como conjuntos dominantes, t-dominantes y r-dependientes.· Se estudian las alianzas de cardinal mínimo. En particular, se hacen estimaciones de dicho cardinal en función de diversos invariantes del grafo.
96

Document Image Representation, Classification and Retrieval in Large-Scale Domains

Gordo, Albert 18 January 2013 (has links)
A pesar del ideal de “oficina sin papeles” nacida en la década de los setenta, la mayoría de empresas siguen todavía luchando contra una ingente cantidad de documentación en papel. Aunque muchas empresas están haciendo un esfuerzo en la transformación de parte de su documentación interna a un formato digital sin necesidad de pasar por el papel, la comunicación con otras empresas y clientes en un formato puramente digital es un problema mucho más complejo debido a la escasa adopción de estándares. Las empresas reciben una gran cantidad de documentación en papel que necesita ser analizada y procesada, en su mayoría de forma manual. Una solución para esta tarea consiste en, en primer lugar, el escaneo automático de los documentos entrantes. A continuación, las imágenes de los documentos puede ser analizadas y la información puede ser extraida a partir de los datos. Los documentos también pueden ser automáticamente enviados a los flujos de trabajo adecuados, usados para buscar documentos similares en bases de datos para transferir información, etc. Debido a la naturaleza de esta “sala de correo” digital, es necesario que los métodos de representación de documentos sean generales, es decir, adecuados para representar correctamente tipos muy diferentes de documentos. Es necesario que los métodos sean robustos, es decir, capaces de representar nuevos tipos de documentos, imágenes con ruido, etc. Y, por último, es necesario que los métodos sean escalables, es decir, capaces de funcionar cuando miles o millones de documentos necesitan ser tratados, almacenados y consultados. Desafortunadamente, las técnicas actuales de representación, clasificación y búsqueda de documentos no son aptos para esta sala de correo digital, ya que no cumplen con algunos o ninguno de estos requisitos. En esta tesis nos centramos en el problema de la representación de documentos enfocada a la clasificación y búsqueda en el marco de la sala de correo digital. En particular, en la primera parte de esta tesis primero presentamos un descriptor de documentos basado en un histograma de “runlengths” a múltiples escalas. Este descriptor supera en resultados a otros métodos del estado-del-arte en bases de datos públicas y propias de diferente naturaleza y condición en tareas de clasificación y búsqueda de documentos. Más tarde modificamos esta representación para hacer frente a documentos más complejos, tales como documentos de varias páginas o documentos que contienen más fuentes de información como texto extraído por OCR. En la segunda parte de esta tesis nos centramos en el requisito de escalabilidad, sobre todo para las tareas de búsqueda, en el que todos los documentos deben estar disponibles en la memoria RAM para que la búsqueda pueda ser eficiente. Proponemos un nuevo método de binarización que llamamos PCAE, así como dos distancias asimétricas generales para descriptores binarios que pueden mejorar significativamente los resultados de la búsqueda con un mínimo coste computacional adicional. Por último, señalamos la importancia del aprendizaje supervisado cuando se realizan búsquedas en grandes bases de datos y estudiamos varios enfoques que pueden aumentar significativamente la precisión de los resultados sin coste adicional en tiempo de consulta. / Despite the “paperless office” ideal that started in the decade of the seventies, businesses still strive against an increasing amount of paper documentation. Although many businesses are making an effort in transforming some of the internal documentation into a digital form with no intrinsic need for paper, the communication with other businesses and clients in a pure digital form is a much more complex problem due to the lack of adopted standards. Companies receive huge amounts of paper documentation that need to be analyzed and processed, mostly in a manual way. A solution for this task consists in, first, automatically scanning the incoming documents. Then, document images can be analyzed and information can be extracted from the data. Documents can also be automatically dispatched to the appropriate workflows, used to retrieve similar documents in the dataset to transfer information, etc. Due to the nature of this “digital mailroom”, we need document representation methods to be general, i.e., able to cope with very different types of documents. We need the methods to be sound, i.e., able to cope with unexpected types of documents, noise, etc. And, we need to methods to be scalable, i.e., able to cope with thousands or millions of documents that need to be processed, stored, and consulted. Unfortunately, current techniques of document representation, classification and retrieval are not apt for this digital mailroom framework, since they do not fulfill some or all of these requirements. Through this thesis we focus on the problem of document representation aimed at classification and retrieval tasks under this digital mailroom framework. Specifically, on the first part of this thesis, we first present a novel document representation based on runlength histograms that achieves state-of-the-art results on public and in-house datasets of different nature and quality on classification and retrieval tasks. This representation is later modified to cope with more complex documents such as multiple-page documents, or documents that contain more sources of information such as extracted OCR text. Then, on the second part of this thesis, we focus on the scalability requirements, particularly for retrieval tasks, where all the documents need to be available in RAM memory for the retrieval to be efficient. We propose a novel binarization method which we dubbed PCAE, as well as two general asymmetric distances between binary embeddings that can significantly improve the retrieval results at a minimal extra computational cost. Finally, we note the importance of supervised learning when performing large-scale retrieval, and study several approaches that can significantly boost the results at no extra cost at query time.
97

Predicting Saliency and Aesthetics in Images: A Bottom-up Perspective

Murray, Naila 18 December 2012 (has links)
Esta tesis investiga dos aspectos diferentes sobre cómo un observador percibe una imagen natural: (i) dónde miramos o, concretamente, qué nos atrae la atención, y (ii) qué nos gusta, e.g., si una imagen es estéticamente agradable, o no. Estas dos experiencias son objeto de crecientes esfuerzos de la investigación en visión por computador. Tanto la atención visual como la estética visual pueden ser modeladas como consecuencia de múltiples mecanismos en interacción, algunos bottom-up o involuntarios, y otros top-down o guiados por tareas. En este trabajo nos concentramos en una perspectiva bottom-up, usando mecanismos visuales y características de bajo nivel, ya que es aquí donde los vínculos entre estética y atención son más evidentes, o fácilmente analizables. En la Parte 1 de la tesis presentamos la hipótesis de que las regiones en una imagen que atraen o no la atención pueden ser estimadas usando representaciones estándar de bajo nivel de imágenes en color. Demostramos esta hipótesis usando un modelo de percepción de color de bajo nivel y adaptándolo a un modelo de estimación de la atención. Nuestro modelo de atención hereda una selección de parámetros y un mecanismo de spatial pooling de los modelos de percepción en los que está basado. Éste mecanismo de pooling ha sido ajustado usando datos psicofísicos adquiridos a través de experimentos sobre color y luminancia. El modelo propuesto mejora el estado-del-arte en la tarea de predecir los puntos de atención en dos bases de datos. Tras demostrar la efectividad de nuestro modelo básico de atención, introducimos una representación de la imagen mejorada, basada en conjuntos geométricos. Con esta mejorada representación de imágenes, el rendimiento de nuestro modelo de atención mejora en las dos bases de datos. En la Parte 2 de la tesis, investigamos el problema del análisis estético visual. Debido a que la estética de imágenes es algo complejo y subjetivo, las bases de datos existentes, que proveen unas pocas imágenes y anotaciones, tienen importantes limitaciones. Para tratar estas limitaciones, hemos presentado una base de datos a gran escala para llevar a cabo actividades de análisis estético visual, que llamamos AVA. AVA contiene más de 250,000 imágenes, junto con una rica variedad de anotaciones. Hemos demostrado que aprovechando los datos en AVA, y usando características genéricas de bajo nivel, como SIFT e histogramas de color, podemos superar el estado-del-arte en tareas de predicción de la calidad estética. Finalmente, consideramos la hipótesis de que la información visual de bajo nivel en nuestro modelo de atención puede también ser usada para predecir la estética visual. Para ello, capturamos las características locales de la imagen como contraste, agrupaciones y aislamiento de características, que se suponen relacionadas con reglas universales de la estética. Usamos las respuestas del centre-surround que forman la base de nuestro modelo de atención, para crear un vector de características que describe la estética. También introducimos un nuevo espacio de color, para representaciones de grano fino. Para terminar, demostramos que las características resultantes alcanzan la precisión del estado-del-arte en el problema de clasificación de la calidad estética. Una contribución prometedora de esta tesis es demostrar que diversas experiencias de la visión - percepción de color a bajo nivel, atención visual, y estimación de la estética visual - pueden ser satisfactoriamente modeladas usando un marco de trabajo unificado. Esto sugiere una arquitectura similar en el área V1 del cerebro para la percepción del color y la atención, y añade evidencias a la hipótesis que la apreciación estética está influenciada, en parte, por información de bajo nivel. / This thesis investigates two different aspects of how an observer experiences a natural image: (i) where we look, namely, where attention is guided, and (ii) what we like, i.e., whether or not the image is aesthetically pleasing. These two experiences are the subjects of increasing research efforts in computer vision. Both visual attention and visual aesthetics can be modeled as a consequence of multiple interacting mechanisms, some bottom-up or involuntary, and others top-down or task-driven. In this work we focus on a bottom-up perspective, using low-level visual mechanisms and features, as it is here that the links between aesthetics and attention may be more obvious and/or easily studied. In Part 1 of the thesis, we hypothesize that salient and non-salient image regions can be estimated to be the regions which are enhanced or assimilated in standard low-level color image representations. We prove this hypothesis by adapting a low-level model of color perception into a saliency estimation model. This model shares the three main steps found in many successful models for predicting attention in a scene: convolution with a set of filters, a center-surround mechanism and spatial pooling to construct a saliency map. For such models, integrating spatial information and justifying the choice of various parameter values remain open problems. Our saliency model inherits a principled selection of parameters as well as an innate spatial pooling mechanism from the perception model on which it is based. This pooling mechanism has been fitted using psychophysical data acquired in color-luminance setting experiments. The proposed model outperforms the state-of-the-art at the task of predicting eye-fixations from two datasets. After demonstrating the effectiveness of our basic saliency model, we introduce an improved image representation. With this improved image representation, the performance of our saliency model in predicting eye-fixations increases for both datasets. In Part 2 of the thesis, we investigate the problem of aesthetic visual analysis. Because image aesthetics is complex and subjective, existing datasets, which have few images and few annotations, have significant limitations. To address these limitations, we introduced a new large-scale database for conducting Aesthetic Visual Analysis, which we call AVA. AVA contains more than 250,000 images, along with a rich variety of annotations. We investigate how the wealth of data in AVA can be used to tackle the challenge of understanding and assessing visual aesthetics by looking into several problems relevant for aesthetic analysis. We demonstrate that by leveraging the data in AVA, and using generic low-level features such as SIFT and color histograms, we can exceed state-of-the-art performance in aesthetic quality prediction tasks. Finally, we entertain the hypothesis that low-level visual information in our saliency model can also be used to predict visual aesthetics by capturing local image characteristics such as feature contrast, grouping and isolation, characteristics thought to be related to universal aesthetic laws. We use the weighted center-surround responses that form the basis of our saliency model to create a feature vector that describes aesthetics. We also introduce a novel color space for fine-grained color representation. We then demonstrate that the resultant features achieve state-of-the-art performance on aesthetic quality classification. As such, a promising contribution of this thesis is to show that several vision experiences - low-level color perception, visual saliency and visual aesthetics estimation - may be successfully modeled using a unified framework. This suggests a similar architecture in area V1 for both color perception and saliency and adds evidence to the hypothesis that visual aesthetics appreciation is driven in part by low-level cues.
98

Generalizaciones de la teoría de integrabilidad de Darboux para campos de vectores polinomiales

Bolaños Rivera, Yudy Marcela 17 May 2013 (has links)
En matemáticas, la integrabilidad de los campos de vectores polinomiales ha sido objeto de estudio desde hace más de cien años. En 1878, Darboux dio unas condiciones que permiten establecer la existencia de una integral prime- ra para estos campos. La existencia de integrales primeras simplifica mucho el estudio de la dinámica de un sistema diferencial, pero dado un sistema diferencial no es fácil, en general, saber si posee o no integrales primeras. A pesar de los notables progresos que en los últimos años se han obtenido sobre este tema dentro de la teoría de integrabilidad de Darboux, todavía no se ha encontrado una respuesta plenamente satisfactoria. En esta memoria estudiamos aspectos relacionados con la teoría de integrabilidad de Darboux y generalizamos algunos resultados. En particular nos interesan los campos de vectores polinomiales en Rn+1 definidos sobre hipersuperficies regulares algebraicas. En 1979 Jouanolou mostró que si el número de hipersuperficies algebraicas invariantes de un campo vectorial en Rn+1 de grado m es por lo menos (n+m n+1 ) +n+1, entonces el campo vectorial tiene una integral primera racional que se puede calcular utilizando hipersuperficies algebraicas inva- riantes. En el capítulo 2 extendemos este resultado mostrando que el número de hipersuperficies algebraicas invariantes necesarias para garantizar la exis- tencia de una integral primera racional de un campo de vectorial polinomial definido sobre una hipersuperficie de grado d es (n+m n+1 ) ��� (n+m ���d n+1 ) + n. Otro aspecto relacionado con la teoría de integrabilidad de Darboux es el estudio del número máximo de clases de hipersuperficies invariantes que un campo vectorial polinomial puede tener. Para encontrar hipersuperficies algebraicas invariantes utilizamos el concepto de hipersuperficie algebraica extáctica. En el capítulo 3 obtenemos cotas superiores para el número máxi- mo de esferas n-dimensionales invariantes de campos vectoriales polinomiales de Rn+1 en función del grado del campo y teniendo en cuenta la multiplicidad de las esferas invariantes. En el capítulo 4 estudiamos los campos vectoriales polinomiales de R3 definidos sobre una cuádrica y obtenemos las cotas supe- riores para el número máximo de cónicas invariantes que uno de estos campos puede tener en función de su grado y que vivan sobre planos invariantes. Pa- ra esto extendemos la noción de multiplicidad de una superficie algebraica invariante. Además, probamos si estas cotas pueden ser alcanzadas o no. En los capítulos 5 y 6 estudiamos sistemas cuadráticos. El estudio de esta clase de sistemas diferenciales no es trivial y se han publicado más de mil artículos sobre ellos. En el capítulo 5 estudiamos sistemas cuadráticos con una silla integrable. Recientemente este tipo de sillas han sido estudiadas por varios autores. Artés, Llibre y Vulpe caracterizaron los retratos de fase de todos los sistemas cuadráticos con una silla integrable pero no encontra- ron sus integrales primeras. Nosotros obtenemos las expresiones explícitas para las integrales primeras Liouvillianas de estos sistemas cuadráticos. En el capítulo 6 estudiamos los sistemas cuadráticos Lotka-Volterra que poseen un invariante Darboux. Cuando no podemos calcular una integral primera de un sistema diferencial es útil determinar si el sistema tiene un invariante Darboux. Nosotros caracterizamos los retratos de fase globales en el disco de Poincaré de todos los sistemas cuadráticos Lotka-Volterra que poseen un invariante Darboux. / In mathematics, the integrability of polynomial vector fields has been studied for more than one hundred years. In 1878, Darboux provided conditions to establish the existence of first integrals for these fields. The existence of first integrals simplifies the study of the dynamics of a differential system, but given a differential system it is not easy, in general, to know whether or not it has first integrals. Despite the remarkable progress that in recent years have been obtained in the Darboux theory of integrability, this question has not yet a satisfactory answer. We study aspects related to the Darboux theory of integrability and we generalize some results. In particular we are interested in polynomial vector fields in Rn+1 defined on regular algebraic hypersurfaces. In 1979 Jouanolou showed that if the number of invariant algebraic hypersurfaces of a vector field in Rn+1 of degree m is at least (n+m n+1 ) + n + 1, then the vector field has a rational first integral that can be calculated using invariant algebraic hypersurfaces. In chapter 2 we extend this result by showing that the number of invariant algebraic hypersurfaces to ensure the existence of a rational first integral of a polynomial vector field defined on a regular algebraic hypersurface of degree d is (n+m n+1 ) �� (n+m ��d n+1 ) + n. Other aspect related to the Darboux integrability theory is the study of the maximum number of classes of invariant hypersurfaces that a polynomial vector field can have. In order to find invariant algebraic hypersurfaces we use the concept of extactic algebraic hypersurface. In chapter 3 we obtain upper bounds for the maximum number of invariant n-dimensional spheres of polynomial vector fields in Rn+1 in function of the degree of the field and taking into account the multiplicity of the invariant spheres. In chapter 4 we study the polynomial vector fields of R3 defined on a quadric and we obtain upper bounds for the maximum number of invariant conics that one of these fields can have in terms of their degree and living on invariant planes. To do this we extend the notion of multiplicity of an invariant algebraic surface. Moreover, we show whether these bounds can be reached or not. In chapters 5 and 6 we study quadratic differential systems. The study of this class of differential systems is not trivial and have been published more than one thousand papers about them. In chapter 5 we study quadratic systems with an integrable saddle. Recently these saddles have been studied by several authors. Artes, Llibre and Vulpe characterized the phase portraits of all quadratic systems having an integrable saddle, but they did not provide their first integrals. We obtain explicit expressions for the Liouvillian first integrals of these systems. In chapter 6 we study the Lotka-Volterra quadratic systems having a Darboux invariant. When we cannot calculate a first integral of a differential system is useful to determine if the system has a Darboux invariant. We characterize the global phase portraits in the Poincaré disc of all quadratic Lotka-Volterra systems possessing a Darboux invariant.
99

Algorithms and complex phenomena in networks: Neural ensembles, statistical, interference and online communities

Gómez Cerdà, Vicenç 23 June 2008 (has links)
Aquesta tesi tracta d'algoritmes i fenòmens complexos en xarxes.En la primera part s'estudia un model de neurones estocàstiques inter-comunicades mitjançant potencials d'acció. Proposem una tècnica de modelització a escala mesoscòpica i estudiem una transició de fase en un acoblament crític entre les neurones. Derivem una regla de plasticitat sinàptica local que fa que la xarxa s'auto-organitzi en el punt crític.Seguidament tractem el problema d'inferència aproximada en xarxes probabilístiques mitjançant un algorisme que corregeix la solució obtinguda via belief propagation en grafs cíclics basada en una expansió en sèries. Afegint termes de correcció que corresponen a cicles generals en la xarxa, s'obté el resultat exacte. Introduïm i analitzem numèricament una manera de truncar aquesta sèrie.Finalment analizem la interacció social en una comunitat d'Internet caracteritzant l'estructura de la xarxa d'usuaris, els fluxes de discussió en forma de comentaris i els patrons de temps de reacció davant una nova notícia. / This thesis is about algorithms and complex phenomena in networks.In the first part we study a network model of stochastic spiking neurons. We propose a modelling technique based on a mesoscopic description level and show the presence of a phase transition around a critical coupling strength. We derive a local plasticity which drives the network towards the critical point.We then deal with approximate inference in probabilistic networks. We develop an algorithm which corrects the belief propagation solution for loopy graphs based on a loop series expansion. By adding correction terms, one for each "generalized loop" in the network, the exact result is recovered. We introduce and analyze numerically a particular way of truncating the series.Finally, we analyze the social interaction of an Internet community by characterizing the structure of the network of users, their discussion threads and the temporal patterns of reaction times to a new post.
100

Estudis matemàtics de Pietro Mengoli (1625-1686): taules triangulars i quasi proporcions com a desenvolupament de l'àlgebra de Viète

Massa Esteve, M. Rosa 26 June 1998 (has links)
No description available.

Page generated in 0.0622 seconds