Cotutela Universitat Politècnica de Catalunya i Queen Mary University of London / The increasing availability of smartphones is facilitating people to capture videos of their experience when attending events such as concerts, sports competitions and public rallies. Smartphones are equipped with inertial sensors which could be beneficial for event understanding. The captured User-Generated Videos (UGVs) are made available on media sharing websites. Searching and mining of UGVs of the same event are challenging due to inconsistent tags or incorrect timestamps. A UGV recorded from a fixed location contains monotonic content and unintentional camera motions, which may make it less interesting to playback. In this thesis, we propose the following identification, synchronisation and video composition frameworks for UGVs. We propose a framework for the automatic identification and synchronisation of unedited multi-camera UGVs within a database. The proposed framework analyses the sound to match and cluster UGVs that capture the same spatio-temporal event, and estimate their relative time-shift to temporally align them. We design a novel descriptor derived from the pairwise matching of audio chroma features of UGVs. The descriptor facilitates the definition of a classification threshold for automatic query-by-example event identification. We contribute a database of 263 multi-camera UGVs of 48 real-world events. We evaluate the proposed framework on this database and compare it with state-of-the-art methods. Experimental results show the effectiveness of the proposed approach in the presence of audio degradations (channel noise, ambient noise, reverberations). Moreover, we present an automatic audio and visual-based camera selection framework for composing uninterrupted recording from synchronised multi-camera UGVs of the same event. We design an automatic audio-based cut-point selection method that provides a common reference for audio and video segmentation. To filter low quality video segments, spatial and spatio-temporal assessments are computed. The framework combines segments of UGVs using a rank-based camera selection strategy by considering visual quality scores and view diversity. The proposed framework is validated on a dataset of 13 events (93~UGVs) through subjective tests and compared with state-of-the-art methods. Suitable cut-point selection, specific visual quality assessments and rank-based camera selection contribute to the superiority of the proposed framework over the existing methods. Finally, we contribute a method for Camera Motion Detection using Gyroscope for UGVs captured from smartphones and design a gyro-based quality score for video composition. The gyroscope measures the angular velocity of the smartphone that can be use for camera motion analysis. We evaluate the proposed camera motion detection method on a dataset of 24 multi-modal UGVs captured by us, and compare it with existing visual and inertial sensor-based methods. By designing a gyro-based score to quantify the goodness of the multi-camera UGVs, we develop a gyro-based video composition framework. A gyro-based score substitutes the spatial and spatio-temporal scores and reduces the computational complexity. We contribute a multi-modal dataset of 3 events (12~UGVs), which is used to validate the proposed gyro-based video composition framework. / El incremento de la disponibilidad de teléfonos inteligentes o smartphones posibilita a la gente capturar videos de sus experiencias cuando asisten a eventos así como como conciertos, competiciones deportivas o mítines públicos. Los Videos Generados por Usuarios (UGVs) pueden estar disponibles en sitios web públicos especializados en compartir archivos. La búsqueda y la minería de datos de los UGVs del mismo evento son un reto debido a que los etiquetajes son incoherentes o las marcas de tiempo erróneas. Por otra parte, un UGV grabado desde una ubicación fija, contiene información monótona y movimientos de cámara no intencionados haciendo menos interesante su reproducción. En esta tesis, se propone una identificación, sincronización y composición de tramas de vídeo para UGVs. Se ha propuesto un sistema para la identificación y sincronización automática de UGVs no editados provenientes de diferentes cámaras dentro de una base de datos. El sistema propuesto analiza el sonido con el fin de hacerlo coincidir e integrar UGVs que capturan el mismo evento en el espacio y en el tiempo, estimando sus respectivos desfases temporales y alinearlos en el tiempo. Se ha diseñado un nuevo descriptor a partir de la coincidencia por parejas de características de la croma del audio de los UGVs. Este descriptor facilita la determinación de una clasificación por umbral para una identificación de eventos automática basada en búsqueda mediante ejemplo (en inglés, query by example). Se ha contribuido con una base de datos de 263 multi-cámaras UGVs de un total de 48 eventos reales. Se ha evaluado la trama propuesta en esta base de datos y se ha comparado con los métodos elaborados en el estado del arte. Los resultados experimentales muestran la efectividad del enfoque propuesto con la presencia alteraciones en el audio. Además, se ha presentado una selección automática de tramas en base a la reproducción de video y audio componiendo una grabación ininterrumpida de multi-cámaras UGVs sincronizadas en el mismo evento. También se ha diseñado un método de selección de puntos de corte automático basado en audio que proporciona una referencia común para la segmentación de audio y video. Con el fin de filtrar segmentos de videos de baja calidad, se han calculado algunas medidas espaciales y espacio-temporales. El sistema combina segmentos de UGVs empleando una estrategia de selección de cámaras basadas en la evaluación a través de un ranking considerando puntuaciones de calidad visuales y diversidad de visión. El sistema propuesto se ha validado con un conjunto de datos de 13 eventos (93 UGVs) a través de pruebas subjetivas y se han comparado con los métodos elaborados en el estado del arte. La selección de puntos de corte adecuados, evaluaciones de calidad visual específicas y la selección de cámara basada en ranking contribuyen en la mejoría de calidad del sistema propuesto respecto a otros métodos existentes. Finalmente, se ha realizado un método para la Detección de Movimiento de Cámara usando giróscopos para las UGVs capturadas desde smartphones y se ha diseñado un método de puntuación de calidad basada en el giro. El método de detección de movimiento de la cámara con una base de datos de 24 UGVs multi-modales y se ha comparado con los métodos actuales basados en visión y sistemas inerciales. A través del diseño de puntuación para cuantificar con el giróscopo cuán bien funcionan los sistemas de UGVs con multi-cámara, se ha desarrollado un sistema de composición de video basada en el movimiento del giroscopio. Este sistema basado en la puntuación a través del giróscopo sustituye a los sistemas de puntuaciones basados en parámetros espacio-temporales reduciendo la complejidad computacional. Además, se ha contribuido con un conjunto de datos de 3 eventos (12 UGVs), que se han empleado para validar los sistemas de composición de video basados en giróscopo.

This thesis is about the stabilization of the numerical solution of the Euler and Navier- Stokes equations of compressible flow. When simulating numerically the flow equations, if no stabilization is added, the solution presents non-physical (but numerical) oscillations. For this reason the stabilization of partial differential equations and of the fluid dynamics equations is of great importance. In the framework of the so-called variational multiscale stabilization, we present here a stabilization method for compressible flow. The method assessment is done first of all on a batch of academical examples for different Mach numbers, for viscous and inviscid, steady and transient flow. Afterwards the method is applied to atmospheric flow simulations. To this end we solve the Euler equations for dry and moist atmospheric flow. In the presence of moisture a set of transport equations for water species should be solved as well. This domain of application is a real challenge from the stabilization point of view because the correct amount of stabilization must be added in order to preserve the physical properties of the atmospheric flow. At this point, in order to even improve our method, we turn towards local preconditioning. Local preconditiong permits to reduce the stiffness problems that present the flow equations and cause a bad and slow convergence to the solution. With this purpose in mind we combine our stabilization method with local preconditioning and present a stabilization method for the preconditioned Navier-Stokes equations of compressible flow, that we call P-VMS. This method is tested over several examples at different Mach numbers and proves a significant improvement not only in the convergence to the solution but also in the accuracy and robustness of the method. Finally, the benefits of P-VMS are theoretically assessed using Fourier stability analysis. As a result of this analysis a modification on the computation of the time step is done even improving the convergence of the method. / Aquesta tesi tracta sobre l'estabilització de la solució numèrica de les equacions d'Euler i Navier-Stokes de flux compressible. Quan es simulen numèricament les equacions que governen els fluids, si no s'afegeix cap estabilització, la solució presenta oscil·lacions no físiques sinó numèriques. Per aquest motiu l'estabilització de les equacions en derivades parcials i de les equacions de la mecànica de fluids és de gran importància. Dins del marc de l'anomenada estabilització de multiescales variacionals, presentem aquí un mètode d'estabilització per flux compressible. L'evaluació del mètode es realitza primer en varis exemples acadèmics per diferents nombres de Mach, per flux viscós, inviscid, estacionari i transitori. Després el mètode s'aplica a simulacions de flux atmosfèric. Per això, resolem les equacions d'Euler per flux atmosfèric sec i humit. En presència d'humitat, també s'ha de resoldre un grup d'equacions de transport d'espècies d'aigua. Aquest domini d'aplicació representa un desafiament des del punt de vista de l'estabilització, donat que s'ha d'afegir la quantitat adequada d'estabilització per tal de preservar les propietats físiques del flux atmosfèric. Arribat aquest punt, per tal de millorar el nostre mètode, ens interessem pels precondicionadors locals. Els precondicionadors locals permeten reduir els problemes de rigidesa que presenten les equacions dels fluids i que són causa d'una pitjor i més lenta convergència cap a la solució. Amb aquest propòsit en ment, combinem el nostre mètode d'estabilització amb els precondicionadors locals i presentem un mètode d'estabilització per les equacions de Navier-Stokes de flux compressible, anomenem aquest màtode P-VMS. Aquest mètode es evaluat per mitjà de varis exemples per diferents nombres de Mach i demostra una millora sustancial no només pel que fa la convergència cap a la solució, sinó també en la precisió i robusteza del mètode. Finalment els beneficis del P-VMS es demostren teòricament a través de l'anàlisi d'estabilitat de Fourier. Com a resultat d'aquest anàlisi, sorgeix una modificació en el càlcul del pas de temps que millora un cop més la convergència del mètode

Capítols 1 i 7 escrits també en anglés / The spatial decision-making process for the purpose of planning, policies, plans, or territorial programs, is intimately tied to the concept of location in the respective geographical space, mainly because many aspects such as natural resources; raw materials, infrastructure, proximity to markets, weather, culture, safety and strategic areas, among others, can be determined, and directly or indirectly related, based on spatial locations. Because of this and assuming that the geographical space constitutes a complex system, it is necessary that the spatial decision-making process intended for achieving aspects of location of goods and services, and/or events for the aforementioned purposes, is carried out in an interdisciplinary way, preferably through participation and consensus from the involved stakeholders involved.In this thesis, an applied research is presented that had as main purpose to provide an archetype that supports the process of spatial decision-making through the spatial consensus by diverse social actors, specially in regard to the location of goods, services and/or events. The archetype, based on the spatial version of the Delphi method modified, has as main characteristic the use of the opinions from a group of experts to solve a problem in the context of the decision-making process and / or in the framework for foresight while also considering the geographical aspect, all of this in order to reach a consensus in regard to the identification of an optimal location in a limited part of a territory.By following the Design Science Research methodology (DSR) and by adopting as auxiliary methods, Documentary Research and Reuse-Based Software Development, an artifact called Geospatial System of Collective Intelligence (SIGIC) was devised through which a collective intelligence behavior could be induced into multidisciplinary groups not experienced in the use of geotechnologies, and for the purpose of locating goods, services, and / or events through the spatial consensus from the participants. After having evaluated the artifact in five different spatial decision situations, two of them in Italy for the location of an air quality monitoring station, and for the zoning of the street prostitution process; two of them in Ecuador to determine the location for the installation of a booth for the screening of HIV and to state the location of booths for the annual initiative for blood collection, and finally, one more in Antarctica, Greenwich Island to determine the location of goods and services to plan the activities of the Scientific Station Pedro Vicente Maldonado.The main results exhibit that even multidisciplinary groups without previous experience in the use of geotechnologies can interact with these tools to study and determine through consensus of their spatial opinions, the potential location of goods, services and / or events in a given territory, thus achieving in this way a process of Collective Spatial Analysis as support for spatial decisions, mainly in aspects related to planning, organization, and use of resources in the territory, and even for the evaluation, preparation, or adoption of policies, plans, and corresponding programs. / El proceso de toma de decisiones espaciales con fines de planificación, políticas, planes o programas territoriales, está estrechamente vinculado con el concepto de la localización en el espacio geográfico respectivo, principalmente porque en base a las ubicaciones espaciales se pueden determinar y relacionar directa e indirectamente, muchos otros aspectos como son los recursos naturales, las materias primas, la infraestructura, la proximidad al mercado, el clima, la cultura, las áreas estratégicas y de seguridad, entre otros. Por esta razón, y asumiendo que el espacio geográfico constituye un sistema complejo, es necesario que la toma de decisiones espaciales destinada a lograr aspectos de localización de bienes servicios y/o eventos para lo fines antes mencionados, se efectúe interdisciplinarmente, preferentemente a través de la participación y consenso de los actores involucrados.En esta tesis se presenta una investigación aplicada que tuvo como propósito aportar un arquetipo para coadyuvar en el proceso de toma de decisiones espaciales por medio del consenso espacial entre diversos actores sociales, primordialmente con respecto a la localización de bienes, servicios y/o eventos. El arquetipo, basado en la versión espacial del Método Delphi modificado, tiene como característica principal el uso de las opiniones de un grupo de expertos para resolver un problema en el contexto de toma de decisiones y/o marco de previsión considerando el aspecto geográfico, con el objetivo de llegar a un consenso respecto a la identificación de una ubicación óptima en una parte limitada del territorio.Siguiendo la metodología de Investigación en Ciencia del Diseño (DSR por su acrónimo en Inglés) y adoptando como métodos auxiliares la Investigación Documental y el Desarrollo de Software Basado en la Reutilización, se ideó el artefacto llamado Sistema Geoespacial de Inteligencia Colectiva (SIGIC), con el cual se logró inducir y coordinar un comportamiento de inteligencia colectiva en grupos multidisciplinares no experimentados en el uso de geotecnologías, con el propósito de localizar bienes, servicios y/o eventos mediante el consenso espacial de los participantes. Este artefacto se evaluó en cinco situaciones diferentes de decisión espacial: dos en Italia, para la ubicación de una estación de monitoreo de calidad del aire y para la zonificación del proceso de prostitución de calle; dos en Ecuador, para determinar el lugar de instalación de un puesto para pruebas de tamizaje de VIH y para establecer las ubicaciones de puestos para la campaña anual de colecta de sangre; y una en la Antártida, Isla de Greenwich, para determinar la ubicación de bienes y servicios con fines de planificación de actividades de la Estación Científica Pedro Vicente Maldonado.Los principales resultados exhiben que grupos multidisciplinares sin práctica en el uso de geotecnologías pueden interactuar con estas herramientas para estudiar y determinar a través del consenso de sus opiniones espaciales, la probable localización de bienes, servicios y/o eventos en un territorio determinado, conformando de esta manera un proceso de Análisis Espacial Colectivo como soporte a las decisiones espaciales principalmente, para aspectos de planificación, organización y empleo de recursos en el territorio o bien para la evaluación, preparación o adopción de políticas, planes y programas correspondientes. / El procés de presa de decisions espacials amb fins de planificació, polítiques, plans o programes territorials, esta íntimament vinculat amb el concepte de la localització en l’espai geogràfic respectiu, principalment perquè en base a las ubicacions espacials es pot determinar i relacionar directament i indirecta, molts altres aspectes com són els recursos naturals, les matèries primeres, la infraestructura, la proximitat al mercat, el clima, la cultura, les àrees estratègiques i de seguretat, entre d´altres. Per aquesta raó, i assolint que el espai geogràfic constitueix un sistema complex, és necessari que la presa de decisions espacials destinada a aconseguir aspectes de localització de béns serveis i/o esdeveniments per els fins anteriorment esmentats, s’efectui interdisciplinariament, de manera preferent mitjançant la participació i consens dels actors involucrats.A aquesta tesi es presenta una investigació aplicada que va tenir com a propòsit aportar un arquetip per coadjuvar en el procés de presa de decisions espacials mitjançant el consens espacial entre diversos actors socials, primordialment respecte de la localització de béns, serveis i/o esdeveniments. L'arquetip, basat en la versió espacial del Mètode Delphi modificat, té com a característica principal l'ús de les opinions d'un grup d'experts per resoldre un problema en el context de presa de decisions i/o marc de previsió considerant l'aspecte geogràfic, amb el objectiu d'arribar a un consens respecte a la identificació d'una ubicació òptima en una part limitada del territori.Tot seguint la metodologia d´Investigació en Ciència del Disseny (DSR per el seu acrònim en anglès) i adoptant com a mètodes auxiliars la Investigació Documental i el Desenvolupament de Software Fonamentat en la Reutilització, es va idear l’artefacte anomenat Sistema Geoespacial d’Intel·ligència Col·lectiva (SIGIC), mitjançant del qual es va aconseguir induir i coordinar un comportament d’intel·ligència col·lectiva en grups multidisciplinaris no experimentats en l’ús de geotecnologíes, amb el propòsit de localitzar béns, serveis i/o esdeveniments mitjançant el consens espacial dels participants. Aquest artefacte es va avaluar en cinc situacions diferents de decisió espacial: dos a Itàlia, per a la ubicació d'una estació de monitorització de qualitat de l'aire i per a la zonificació del procés de prostitució del carrer; dos a Equador, per determinar el lloc d'instal·lació d'un posat per a proves de tamisatge de VIH i per establir les ubicacions de llocs per a la campanya anual de col·lecta de sang; i una a l'Antàrtida, Illa de Greenwich, per determinar la ubicació de béns i serveis amb fins de planificació d'activitats de l'Estació Científica Pedro Vicente Maldonado.Els principals resultats exhibeixen que grups multidisciplinaris sense practica en l’ús de les geotecnologíes poden interactuar amb aquestes eines per estudiar i determinar mitjançant el consens de les seves opinions espacials, la probable localització de béns, serveis i/o esdeveniments en un territori determinat, conformant d´aquesta manera un procés d’Anàlisi Espacial Col·lectiu com a suport a les decisions espacials principalment, per aspectes de planificació, organització i ocupació de recursos en el territori o bé per l´avaluació, preparació o adopció de polítiques, plans i programes corresponents. / Il processo decisionale spaziale ai fini della pianificazione, delle politiche, dei piani o dei programmi territoriali, è strettamente legato al concetto di localizzazione dello spazio geografico di riferimento, principalmente perché in base alle ubicazioni spaziali possono essere determinati e si relazionano direttamente e indirettamente, molti altri aspetti tra i quali le risorse naturali, le materie prime, le infrastrutture, la vicinanza al mercato, il clima, la cultura, le aree strategiche e di sicurezza. Quindi, assumendo che lo spazio geografico costituisce un sistema complesso, è necessario che le decisioni spaziali volte ad ottenere aspetti per la localizzazione di beni e servizi e/o eventi per i fini prima menzionati, siano effettuate in maniera interdisciplinare, preferibilmente attraverso la partecipazione e il consenso tra le parti interessate. In questa tesi viene presentata una ricerca applicata che ha avuto come proposito fornire un archetipo per aiutare nel processo decisionale spaziale per mezzo del consenso speciale tra diversi attori sociali, soprattutto per quanto riguarda la localizzazione dei beni, servizi e/o eventi. L'archetipo, in base alla versione spaziale del Metodo Delphi modificato, ha come caratteristica principale l'uso delle opinioni di un gruppo di esperti per risolvere un problema nel contesto del processo decisionale e/o di un quadro di previsione considerando l'aspetto geografico, con l'obiettivo di giungere ad un consenso riguardo l'identificazione di una posizione ottimale in una parte limitata del territorio. Seguendo la metodologia della Ricerca Scientifica di Progettazione (DSR con il suo acronimo in inglese) e adottando come metodi ausiliari la Ricerca Documentaria e lo Sviluppo del Software Basato sulla Riutilizzazione, è stato messo a punto l’artefatto chiamato Sistema Geo-Spaziale di Intelligenza Collettiva (SIGIC), con il quale è stato possibile indurre e coordinare un comportamento di intelligenza collettiva in gruppi multidisciplinari non sperimentati nell'uso di geo-tecniche, al fine di localizzare beni, servizi e/o eventi attraverso il consenso spaziale dei partecipanti. Questo artefatto è stato valutato in cinque situazioni diverse di decisione spaziale: due in Italia, per l'ubicazione di una stazione di monitoraggio della qualità dell'aria e per la zonizzazione del processo di prostituzione di strada; due in Ecuador, per determinare il luogo di installazione di un centro per i test per l'HIV e per stabilire le ubicazioni di centri per la campagna annuale di donazione del sangue; e una in Antartide, nell'isola Greenwich, per determinare l'ubicazione di beni e servizi al fine di pianificare le attività della Stazione Scientifica Pedro Vicente Maldonado. Dopo aver valutato l'artefatto in cinque differenti situazioni di decisione spaziale, i principali risultati mostrano che i gruppi multidisciplinari senza pratica nell'uso di geo-tecniche possono interagire con questi strumenti per studiare e determinare attraverso il consenso delle loro opinioni spaziali, la probabile localizzazione dei beni, servizi e/o eventi in un determinato territorio, formando così un processo di Analisi Spaziale Collettiva principalmente come supporto alle decisioni spaziali, per gli aspetti di pianificazione, organizzazione e l'uso delle risorse in il territorio o anche per la valutazione, la preparazione o l'adozione di politiche, piani e programmi corrispondenti.

This thesis focuses on the control of a singing voice synthesizer to achieve natural expression similar to a real singer. There are many features that should be controlled to achieve natural expression related to melody, dynamics, rhythm, and timbre. In this thesis we focus on the control of pitch and dynamics with a unit selection-based system, two statistically-based systems, and a hybrid system. These systems are trained with two possible expression databases that we have designed, recorded, and labeled. We define the basic units from which the databases are built of, which are basically sequences of three notes or rests. Our perceptual evaluation compares the proposed systems with other systems to see how these relate to each other. The objective evaluation focuses on the algorithms efficiency. / Aquesta tesi es centra en el control dels sintetitzadors de veu cantada per aconseguir una expressivitat natural semblant a la d'un cantant real. Hi ha moltes característiques que s'haurien de controlar per aconseguir una expressivitat natural relacionades amb la melodia, la dinàmica, el ritme i el timbre. En aquesta tesi ens centrem en el control de la freqüència fonamental i de la dinàmica amb un sistema basat en selecció d'unitats, dos sistemes estadístics, i un sistema híbrid. Aquests sistemes són entrenats amb dues possibles bases de dades expressives que hem dissenyat, enregistrat i etiquetat. Hem definit les unitats bàsiques a partir de les quals les bases de dades s'han construit i que són seqüències de tres notes o silencis. La nostra avaluació perceptual compara els sistemes proposats amb altres sistemes per tal de veure com els podem relacionar. L'avaluació objectiva es centra en l'eficiència dels sistemes.

En aquest treball s'estudien aproximacions de llenguatges regulars per membres d'una varietat de llenguatges regulars donada. Es tracta d'aproximacions superiors o inferiors en el sentit de la teoria dels conjunts aproximats (Rough set theory) de Pawlak. Les relacions utilitzades per a les aproximacions són les congruències corresponents a la varietat de llenguatges regulars considerada. En particular, s'estudia l'existència de les aproximacions superior mínima i inferior màxima. En les anomenades varietats principals, aquestes sempre existeixen, i presentem algorismes per trobar-les. Per a varietats no principals, la situació és molt més complexa. En aquest cas estudiem les condicions per a la seva existència. Concretament, considerem varietats que són unió d'una família dirigida de varietats principals, i també varietats pseudo-principals, que es defineixen en aquest treball. A continuació estudiem la precisió de les aproximacions, utilitzant la densitat relativa entre el llenguatge objecte i la seva aproximació, observant després el seu comportament asimptòtic. Aquesta mesura de la precisió és aplicada a les aproximacions en les famílies de llenguatges k-definits, k-definits inversos, i,j-definits, k-testables i commutatius. Finalment examinem aproximacions sota relacions de indiscernibilitat, l'índex de les quals és infinit, seguint el treball de Paun, Polkowsky i Skowron (1997), i analitzem fins a quin punt poden ser estudiades dins del nostre marc teòric. Descrivim algunes de les seves característiques generals, comparant-les amb algunes de les famílies ja presentades, i en alguns casos, introduïm modificacions en les seves definicions per obtenir relacions de congruència. Encara que en aquesta tesi considerem sobretot varietats d’Eilenberg, les idees poden ser aplicades a altres tipus de varietats de llenguatges. El nostre treball també pot ser considerat com un abordatge al problema / En este trabajo se estudian aproximaciones de lenguajes regulares por miembros de una variedad de lenguajes regulares dada. Se trata de aproximaciones superiores o inferiores en el sentido de la teoría de los conjuntos approximados (Rough set theory) de Pawlak. Las relaciones utilizadas para las aproximaciones son las congruencias correspondientes a la variedad de lenguages regulares considerada. En particular, se estudia la existencia de las aproximaciones superior mínima e inferior máxima. En las llamadas variedades principales, éstas siempre existen, y presentamos algoritmos para hallarlas. Para variedades no principales, la situación es mucho más compleja. En este caso estudiamos las condiciones para su existencia. Concretamente, consideramos variedades que son unión de una familia dirigida de variedades principales, y también variedades pseudo-principales, que se definen en este trabajo. A continuación estudiamos la precisión de las aproximaciones, utilizando la densidad relativa entre el lenguaje objeto y su aproximación, observando luego su comportamiento asintótico. Esta medida de la precisión es aplicada a las aproximaciones en las familias de lenguajes k-definidos, k-definidos inversos, i,j-definidos, k-testables y conmutativos. Finalmente examinamos aproximaciones bajo relaciones de indiscernibilidad, cuyo índice es infinito, siguiendo el trabajo de Paun, Polkowsky y Skowron (1997), y analizamos hasta qué punto pueden ser estudiadas dentro de nuestro marco teórico. Describimos algunas de sus características generales, comparándolas con algunas de las familias ya presentadas, y en algunos casos, introducimos modificaciones en sus definiciones para obtener relaciones de congruencia. Aunque en esta tesis consideramos sobre todo variedades de Eilenberg, las ideas pueden ser aplicadas a otros tipos de variedades de lenguajes. Nuestro trabajo también puede ser considerado como un abordaje al problema de la inferencia caracterizable, en la cual a partir de una muestra, se infiere un lenguaje de un tipo determinado. / We study approximations of regular languages by members of a given variety of regular languages. These are upper or lower approximations in the sense of Pawlak’s rough set theory with respect to congruences belonging to the variety of congruences corresponding to the given variety of regular languages. In particular, we consider the closest upper and lower approximations in the later. In the so-called principal varieties these always exist, and we present algorithms for finding them, but for other varieties the situation is more complex. For non-principal +-varieties we study conditions for the existence of the closest upper and lower approximations. In particular, we consider varieties that are the union of a directed family of principal +-varieties, and pseudo-principal +-varieties, that are defined in this work. Next, we consider the accuracy of the considered approximations, measured by the relative density of the object language in the approximation language and the asymptotic behavior of this quotient. In particular, we apply our measures of accuracy to k-definite, reverse k-definite, i,j-definite, k-testable and commutative approximations. Finally, we examine rough approximations under some infinite index indiscernibility relations as they were presented by Paun, Polkowski and Skowron (1997), looking at how they fit in our framework. We study their general features, comparing them with some of the families already studied, and in some cases introducing modifications in their definitions to make them congruences. Although we consider mostly Eilenberg’s +-varieties, the general ideas apply also to other types of varieties of languages. Our work may also be viewed as an approach to the characterizable inference problem in which a language of a certain kind is to be inferred from a given sample.

Esta tesi tracta sobre la participació de les persones en la creació de dades espacials de forma més o menys voluntària i en l'anàlisi d'aquestes dades utilitzant patrons de processos puntuals i geoestadística. Les dades geogràfiques creades per voluntaris suposen un canvi radical en la forma com aquestes han segut creades tradicionalment. Fins fa uns anys, les dades geogràfiques han estat creades tan sols per experts i grans institucions, una aproximació des de dalt cap a baix. La revolució 2.0 a internet ha permés que la tecnologia estiga a l'abast de tothom. Per a les dades geogràfiques ha suposat que qualsevol puga contribuir a projectes voluntaris com OspenStreetMap aportant el seu coneixemnet de l'entorn. Una aportació des de baix cap a dalt. Aquest canvi deixa preguntes sobre si es poden emprar les dades, quina qualitat tenen, són creïbles els usuaris quan fan aportacions, hi ha errors... Aquesta tesi tracta de donar resposta a com fer mesures de la qualitat, la credibilitat i l'anàlisi de les dades així com facilitar la recol·lecció de dades geogràfiques provinents de les xarxes socials.

Tesi per compendi de publicacions. / The growth of the Internet impacts multiple areas of the world economy, and it has become a permanent part of the economic landscape both at the macro- and at microeconomic level. On-line traffic and information are currently assets with large business value. Even though commercial Internet has been a part of our lives for more than two decades, its impact on global, and everyday, economy still holds many unknowns. In this work we analyse important macro- and microeconomic aspects of the Internet. First we investigate the characteristics of the interdomain traffic, which is an important part of the macroscopic economy of the Internet. Finally, we investigate the microeconomic phenomena of price discrimination in the Internet. At the macroscopic level, we describe quantitatively the interdomain traffic matrix (ITM), as seen from the perspective of a large research network. The ITM describes the traffic flowing between autonomous systems (AS) in the Internet. It depicts the traffic between the largest Internet business entities, therefore it has an important impact on the Internet economy. In particular, we analyse the sparsity and statistical distribution of the traffic, and observe that the shape of the statistical distribution of the traffic sourced from an AS might be related to congestion within the network. We also investigate the correlations between rows in the ITM. Finally, we propose a novel method to model the interdomain traffic, that stems from first-principles and recognizes the fact that the traffic is a mixture of different Internet applications, and can have regional artifacts. We present and evaluate a tool to generate such matrices from open and available data. Our results show that our first-principles approach is a promising alternative to the existing solutions in this area, which enables the investigation of what-if scenarios and their impact on the Internet economy. At the microscopic level, we investigate the rising phenomena of price discrimination (PD). We find empirical evidences that Internet users can be subject to price and search discrimination. In particular, we present examples of PD on several ecommerce websites and uncover the information vectors facilitating PD. Later we show that crowd-sourcing is a feasible method to help users to infer if they are subject to PD. We also build and evaluate a system that allows any Internet user to examine if she is subject to PD. The system has been deployed and used by multiple users worldwide, and uncovered more examples of PD. The methods presented in the following papers are backed with thorough data analysis and experiments. / Internet es hoy en día un elemento crucial en la economía mundial, su constante crecimiento afecta directamente múltiples aspectos tanto a nivel macro- como a nivel microeconómico. Entre otros aspectos, el tráfico de red y la información que transporta se han convertido en un producto de gran valor comercial para cualquier empresa. Sin embargo, más de dos decadas después de su introducción en nuestras vidas y siendo un elemento de vital importancia, el impacto de Internet en la economía global y diaria es un tema que alberga todavía muchas incógnitas que resolver. En esta disertación analizamos importantes aspectos micro y macroeconómicos de Internet. Primero, investigamos las características del tráfico entre Sistemas Autónomos (AS), que es un parte decisiva de la macroeconomía de Internet. A continuacin, estudiamos el controvertido fenómeno microeconómico de la discriminación de precios en Internet. A nivel macroeconómico, mostramos cuantitatívamente la matriz del tráfico entre AS ("Interdomain Traffic Matrix - ITM"), visto desde la perspectiva de una gran red científica. La ITM obtenida empíricamente muestra la cantidad de tráfico compartido entre diferentes AS, las entidades más grandes en Internet, siendo esto uno de los principales aspectos a evaluar en la economiá de Internet. Esto nos permite por ejemplo, analizar diferentes propiedades estadísticas del tráfico para descubrir si la distribución del tráfico producido por un AS está directamente relacionado con la congestión dentro de la red. Además, este estudio también nos permite investigar las correlaciones entre filas de la ITM, es decir, entre diferentes AS. Por último, basándonos en el estudio empírico, proponemos una innovadora solución para modelar el tráfico en una ITM, teniendo en cuenta que el tráfico modelado es dependiente de las particularidades de cada escenario (e.g., distribución de apliaciones, artefactos). Para obtener resultados representativos, la herramienta propuesta para crear estas matrices es evaluada a partir de conjuntos de datos abiertos, disponibles para toda la comunidad científica. Los resultados obtenidos muestran que el método propuesto es una prometedora alternativa a las soluciones de la literatura. Permitiendo así, la nueva investigación de escenarios desconocidos y su impacto en la economía de Internet. A nivel microeconómico, en esta tesis investigamos el fenómeno de la discriminación de precios en Internet ("price discrimination" - PD). Nuestros estudios permiten mostrar pruebas empíricas de que los usuarios de Internet están expuestos a discriminación de precios y resultados de búsquedas. En particular, presentamos ejemplos de PD en varias páginas de comercio electrónico y descubrimos que informacin usan para llevarlo a cabo. Posteriormente, mostramos como una herramienta crowdsourcing puede ayudar a la comunidad de usuarios a inferir que páginas aplican prácticas de PD. Con el objetivo de mitigar esta cada vez más común práctica, publicamos y evaluamos una herramienta que permite al usuario deducir si está siendo víctima de PD. Esta herramienta, con gran repercusión mediática, ha sido usada por multitud de usuarios alrededor del mundo, descubriendo así más ejemplos de discriminación. Por último remarcar que todos los metodos presentados en esta disertación están respaldados por rigurosos análisis y experimentos.

The energy efficiency assessment of high-pressure pneumatic circuits is the aim of this dissertation. From a historical perspective the past and cur- rent activities with regards to the energy saving conservation in pneumatic technology were examined, and it could be concluded that high pressure pneumatic circuits have been repeatedly used for years in several industrial applications but to date no studies on that specific field are known. After a systematic review of studies concerning energy saving in pneumatic applications, a complete dynamic model for a high-pressure air blowing machine, employed in the production of plastic bottles, was developed. A synthetic version of the real pneumatic system was considered and consisted of a valve manifold, two tanks, one that simulated the mould cavity where the plastic preform is commonly blown and the other, was intended to recycle air. The one-dimensional models were derived for the pneumatic valve, pipes and vessels. The dynamic modelling of the valve took into account the flow non-linearities through the various geometrical restrictions as well as the pressure and temperature evolution at the inner chambers. Because of the existence of flow discontinuities in the pipes, different solving methods were applied, taking as starting point the Method of Characteristics and continued delving into finite volume methods such as Riemann-solver-based schemes. On the experimental phase a single blowing station unit was designed and built up. The pressure and temperature characteristics at different positions of the pneumatic circuit were measured in detail. In addition, the fluid flow through the valve manifold could be characterised by the sonic conductance and critical pressure ratio, which were determined by the isothermal discharge method. Effort was also expended to study the behaviour of the pressure waves generated along the tubes. The pressure wave propagation was computationally charted, with the intention of assessing how this parameter affected the recycling process. The examination of the experimental results proved the efficiency of the re- cycling process and demonstrated to be in close agreement with the mathematical model. The parameters governing the maximum amount of air to be recycled at each working cycle were identified, and the influence of the pipe geometry was discussed. Finally the author provides recommendations for future research and makes suggestions regarding the valve design to enhance the efficiency of the system. / El objetivo de esta investigación es evaluar la eficiencia energética de los circuitos neumáticos que trabajan con presiones muy superiores a las que habitualmente se emplean en la mayoría de aplicaciones industriales. Un análisis exhaustivo de como el ahorro energético se ha tratado a lo largo de las últimas décadas permite concluir que a pesar de que existen numerosos estudios que revisan las diferentes metodologías empleadas tanto en el reciclaje como en la reducción del consumo de aire comprimido, ninguno presta atención a las aplicaciones que representan el objeto de este estudio. La revisión de las patentes publicadas en las últimas décadas pone de manifiesto la actividad creciente en el desarrollo de máquinas de soplado para botellas de plástico (PET). Las diferentes técnicas empleadas con la intención de reciclar el aire empleado en una de las fases de soplado indican la necesidad de un ahorro de energía. En base a este escenario, se desarrolló un modelo matemático que permite determinar la variación transitoria de los principales parámetros físicos que gobiernan el flujo de aire a través del circuito neumático utilizado en una máquina de soplado de aire a alta presión. El modelo reducido de dicho circuito consiste de un bloque de válvulas, dos tanques, uno que simula la cavidad del molde, donde la preforma de plástico se moldea mediante inyección por soplado y el otro, en el que se recicla el aire empleado en el soplado. Debido a la existencia de discontinuidades de flujo en las tuberías, se aplicaron diferentes métodos de resolución para las ecuaciones de Euler, tomando como punto de partida el Método de las Características y finalizando con métodos numéricos basados en esquemas del tipo Riemann-solver. Por otro lado el modelado matemático de la válvula tiene en cuenta las no linealidades del flujo a través de las diversas restricciones geométricas, así como la evolución de presión y temperatura en los volúmenes interiores de la misma. En la fase experimental, se diseñó y construyó una estación de soplado que permitía determinar las características de presión y temperatura en diferentes posiciones del circuito neumático. Esto permitió determinar el comportamiento de las ondas de presión generadas a lo largo de los tubos y su influencia el proceso de reciclaje. A sí mismo, se emplearon métodos alternativos (simple discharge method and isothermal discharge method) para caracterizar el flujo a través del bloque de válvulas. El examen de los resultados experimentales demostró la eficiencia del proceso de reciclaje y demostró estar en estrecho acuerdo con el modelo matemático. Se identificaron los parámetros que rigen la máxima cantidad de aire que puede reciclarse en cada ciclo de trabajo, y se examinó la influencia de la geometría de la tubería. Por último, el autor aporta recomendaciones para futuras investigaciones y hace sugerencias sobre el diseño de la válvula neumática para mejorar la eficiencia del sistema.

L'objectiu d'aquesta tesi és proposar noves tècniques per al disseny de microarquitectures clúster superescalars eficients. Les microarquitectures clúster particionen el disseny de diversos components crítics del hardware com a mitjà per mantenir-ne el paral·lelisme i millorar-ne l'escalabilitat. El nucli d'un processador clúster, format per blocs de baixa complexitat o clústers, pot executar cadenes d'instruccions dependents sense pagar el sobrecost d'una llarga emissió, curtcircuïts, o lectura de registres, encara que si dues instruccions dependents s'executen en clústers diferents, es paga la penalització d'una comunicació. Per altra banda, les estructures distribuïdes impliquen generalment menors requisits de potència dinàmica, i simplifiquen la gestió de l'energia per mitjà de tècniques com la desactivació selectiva del rellotge o l'energia, o com la reducció a escalade la tensió.El primer objecte d'aquesta recerca és l'assignació d'instruccions a clústers, ja que aquesta juga un paper clau en el rendiment, amb l'objectiu de mantenir equilibrada la càrrega i reduir la penalització de les comunicacions crítiques. Es proposen dos diferents enfocs: primer, una família de nous esquemes que identifiquen dinàmicament certs grups d'instruccions dependents anomenats "slices", i fan l'assignació de clústers slice per slice. Es diferencien d'altres enfocs previs, ja sigui perquè són dinàmics i/o bé perquè inclouen nous mecanismes explícits de mesura i gestió de l'equilibri de càrrega. Segon, una família de nous esquemes que assignen clústers instrucció per instrucció, basats en les assignacions prèvies dels productors dels registres fonts, en la ubicació dels registres físics, i en la càrrega de treball.La segona contribució proposa la predicció de valors com a mitjà per mitigar les penalitzacions dels retards dels connectors i, en particular, per amagar les comunicacions entre clústers. Es demostra que el benefici obtingut amb l'eliminació de dependències creix amb el nombre de clústers i la latència de les comunicacions i, doncs, és major que per a una arquitectura centralitzada. Es proposa un nou esquema d'assignació de clústers que aprofita la menor densitat del graf de dependències per tal de millorar l'equilibri de càrrega.El tercer aspecte considerat es la xarxa d'interconnexió entre clústers, ja que determina la latència de les comunicacions, amb l'objectiu de trobar el millor compromís entre cost i rendiment. Es proposen diverses xarxes punt-a-punt, tant síncrones com parcialment asíncrones, que assoleixen un IPC pròxim al d'un model ideal amb ample de banda il·limitat, tot i tenir molt baixa complexitat. Llur impacte sobre els curtcircuïts, cues d'emissió o bancs de registres es molt menor que el d'altres enfocs. Es proposen també possibles implementacions dels enrutadors, que il·lustren llur factibilitat amb solucions hardware molt simples i de baixa latència. Es proposa un nou esquema d'assignació de clústers conscient de la topologia, que redueix la latència de les comunicacions.L'última contribució proposa tècniques per distribuir els components principals de les etapes inicials del processador, amb l'objectiu de reduir-ne la complexitat i evitar-ne la replicació. Es proposen tècniques eficaces per a la partició del predictor de salts i la lògica de distribució d'instruccions, a fi de minimitzar la penalització pels retards dels connectors causada per les dependències recursives en dos llaços crítics del hardware: la generació de l'adreça de búsqueda d'instruccions i la lògica d'assignació d'instruccions, respectivament. En el primer cas, es converteixen els retards dels connectors intra-estructurals d'un predictor centralitzat en retards de comunicació entre clústers, els quals se segmenten sense problemes. En el segon cas, el particionat de la lògica d'assignació d'instruccions basada en dependències implica paral·lelitzar aquesta tasca, la qual es inherentment seqüencial. / El objetivo de esta tesis es proponer técnicas para el diseño de microarquitecturas clúster superescalares eficientes. Las microarquitecturas clúster particionan el diseño de diversos componentes críticos del hardware como medio para mantener el paralelismo y mejorar la escalabilidad. El núcleo de un procesador clúster, formado por bloques de baja complejidad o clústers, puede ejectutar cadenas de instrucciones dependientes sin pagar el sobrecoste de una larga emisión, cortocircuitos, o lectura de registros; pero si dos instrucciones dependientes se ejecutan en clústers distintos, se paga la penalización de una comunicación. Por otro lado, las estructuras distribuidas implican generalmente menores requisitos de potencia dinámica, y simplifican la gestión de la energía por medio de técnicas como la desactivación selectiva del reloj o de la alimentación, o la reducción a escala del voltaje.El primer objetivo de esta investigación es la asignación dinámica de instrucciones a clústers, ya que ésta juega un papel clave en el rendimiento, a fin de mantener equilibrada la carga y reducir la penalización de las comunicaciones críticas. Se proponen dos enfoques distintos: primero, una familia de nuevos esquemas que identifican dinámicamente ciertos grupos de instrucciones denominados "slices", y realizan la asignación slice por slice. Éstos se diferencian de otros enfoques previos, ya sea porque son dinámicos y/o porque incluyen nuevos mecanismos explícitos de medida y gestión del equilibrio de carga. Segundo, una familia de nuevos esquemas que asignan clústers instrucción a instrucción, basándose en las asignaciones previas de los productores de sus registros fuente, en la ubicación de los registros físicos, y en la carga de trabajo.La segunda contribución propone la predicción de valores como medio para mitigar las penalizaciones de los retardos de los conectores, y en particular, para esconder las comunicaciones entre clústers. Se demuestra que el beneficio obtenido con la eliminación de dependencias aumenta con el número de clústers y con la latencia de las comunicaciones, y es asimismo mayor que para una arquitectura centralizada. Se propone un nuevo esquema de asignación de clústers que aprovecha la menor densidad del grafo de dependencias con el fin de mejorar el equilibrio de la carga.El tercer aspecto considerado es la red de interconexión entre clústers, pues determina la latencia de las comunicaciones, a fin de hallar el mejor compromiso entre coste y rendimiento. Se proponen diversas redes punto a punto, tanto síncronas como parcialmente asíncronas, que aun teniendo muy baja complejidad consiguen un IPC próximo al de un modelo con ancho de banda ilimitado. Su impacto sobre la complejidad de los cortocircuitos, colas de emisión o bancos de registros es mucho menor que el de otros enfoques. Se proponen también posibles implementaciones de los enrutadores, ilustrando su factibilidad como soluciones simples y de baja latencia. Se propone un esquema de asignación de clústers consciente de la topología, que reduce la latencia de las comunicaciones.La última contribución propone técnicas para distribuir los componentes principales de las etapas iniciales del procesador, con el objetivo de reducir su complejidad y evitar su replicación. Se proponen técnicas eficaces para particionar el predictor de saltos y la lógica de distribución de instrucciones, a fin de minimizar la penalización por retardos de conectores causada por las dependencias recursivas en dos bucles críticos del hardware: la generación de la dirección de búsqueda de instrucciones y la lógica de asignación de clústers. En el primer caso, los retardos de los conectores intra-estructurales de un predictor centralizado se convierten en retardos de comunicación entre clústers, que se pueden segmentar fácilmente. En el segundo caso, el particionado de la lógica de asignación de clústers basada en dependencias implica paralelizar esta tarea, intrínsecamente secuencial. / The objective of this thesis is to propose new techniques to design efficient clustered superscalar microarchitectures. Clustered microarchitectures partition the layout of several critical hardware components as a means to keep most of the parallelism while improving the scalability. A clustered processor core, made up of several low complex blocks or clusters, can efficiently execute chains of dependent instructions without paying the overheads of a long issue, register read or bypass latencies. Of course, when two dependent instructions execute in different clusters, an inter-cluster communication penalty is incurred. Moreover, distributed structures usually imply lower dynamic power requirements, and simplify power management via techniques such a selective clock/power gating and voltage scaling.The first target of this research is the assignment of instructions to clusters, since it plays a major role on performance, with the goals of keeping the workload of clusters balanced and reducing the penalty of critical communications. Two different approaches are proposed: first, a family of new schemes that dynamically identify groups of data-dependent instructions called slices, and make cluster assignments on a per-slice basis. The proposed schemes differ from previous approaches either because they are dynamic and/or because they include new mechanisms to deal explicitly with workload balance information gathered at runtime. Second, it proposes a family of new dynamic schemes that assign instructions to clusters in a per-instruction basis, based on prior assignment of the source register producers, on the cluster location of the source physical registers, and on the workload of clusters.The second contribution proposes value prediction as a means to mitigate the penalties of wire delays and, in particular, to hide inter-cluster communications while also improving workload balance. First, it is proven that the benefit of breaking dependences with value prediction grows with the number of clusters and the communication latency, thus it is higher than for a centralized architecture. Second, it is proposed a cluster assignment scheme that exploits the less dense data dependence graph that results from predicting values to achieve a better workload balance.The third aspect considered is the cluster interconnect, which mainly determines communication latency, seeking for the best trade-off between cost and performance. First, several cost-effective point-to-point interconnects are proposed, both synchronous and partially asynchronous, that approach the IPC of an ideal model with unlimited bandwidth while keeping the complexity low. The proposed interconnects have much lower impact than other approaches on the complexity of bypasses, issue queues and register files. Second, possible router implementations are proposed, which illustrate their feasibility with very simple and low-latency hardware solutions. Third, a new topology-aware improvement to the cluster assignment scheme is proposed to reduce the distance (and latency) of inter-cluster communications.The last contribution proposes techniques for distributing the main components of the processor front-end with the goals of reducing their complexity and avoiding replication. In particular, effective techniques are proposed to cluster the branch predictor and the steering logic, that minimize the wire delay penalties caused by broadcasting recursive dependences in two critical hardware loops: the fetch address generation, and the cluster assignment logic, respectively. In the former case, the proposed technique converts the cross-structure wire delays of a centralized predictor into cross-cluster communication delays, which are smoothly pipelined. In the latter case, the partitioning of the instruction steering logic involves the parallelization of an inherently sequential task such as the dependence based cluster assignment of instructions.

Complex hardware systems become more and more ubiquitous in mission critical applications such as military, satellite, and medical to name but a few. In such applications, reliability remains a primary concern because a failure that occurs during their normal operations might produce important catastrophes like loss of life or loss of money. All these failures are often caused by minuscule bug that exists inside the software which controls the systems, or within the hardware itself. In addition, most of these systems cannot be interrupted while working, even for a few seconds a year, making it difficult to repair bugs found during their normal operations. The main purpose of this work is to build efficient verification techniques for asynchronous concurrent systems. Because of the pivotal roles these systems assume in a given application, designers of such systems must keep development and maintenance costs under control and meet nonfunctional constraints on the design of the system, such as cost, power, weight, or the system architecture by itself. But most importantly, they must assure their customer as well as the certification authorities that both the design and its implementation are correct. Otherwise, they may end up shipping unsafe systems to the market, and the consequences of this action would be catastrophic. To achieve this goal, designers need efficient methods and tools to assist them in verifying the correctness of the design. In this thesis we focus on a symbolic model checking technique called bounded model checking (BMC). BMC is a method targeted mainly at finding bugs in a system. It answers the questions whether there exists a counterexample, shorter than a given length, that violates a given property. During a BMC operation each execution path is encoded into Boolean formula, and the problem is reduced to satisfiability checking of the formula. Therefore, the operation consists mainly in constructing a Boolean formula that is satisfiable if and only if such a counterexample exists. We model our systems with transition systems (TSs). In particular, we are mainly interested in synchronized product of TSs. Since concurrent systems are formed by a combination of several components communicating between each other, synchronized product of TSs is well-suited to capture the behavior of such systems. The executions of concurrent systems are commonly modeled using the so-called interleaving execution, which allows only one single event to fire at each step. However, due to the complexity of such systems inteleaving method will not only require many steps but also generate long formulas. In this work, we adopt another approach based on breadth-first search (BFS). In a BMC operation, the translation of the model into a Boolean formula is polynomial in the size of the model, but the solving time of the Boolean formula can be exponential in the size of the formula. Therefore, our research hypothesis is that we can improve the efficiency of BMC by generating succinct formula, and by minimizing the number of necessary steps during an execution. We introduce several BMC techniques aimed at improving the efficiency of BMC for asynchronous concurrent systems. The techniques are grouped in two main parts (i) techniques for checking reachability properties and (ii) techniques for checking properties written in linear temporal logic (LTL). In addition, we also propose some methods for minimizing the number of execution steps or bound. We implemented all these methods in a BMC toolset. At the end of the dissertation, we will discuss the experimental results we obtained.