The Metabolic Core and Catalytic Switches Are Fundamental Elements in the Self-Regulation of the Systemic Metabolic Structure of Cells

19 p.

Invariant-free deduction systems for temporal logic

In this thesis we propose a new approach to deduction methods for temporal logic. Our proposal is based on an inductive definition of eventualities that is different from the usual one. On the basis of this non-customary inductive definition for eventualities, we first provide dual systems of tableaux and sequents for Propositional Linear-time Temporal Logic (PLTL). Then, we adapt the deductive approach introduced by means of these dual tableau and sequent systems to the resolution framework and we present a clausal temporal resolution method for PLTL. Finally, we make use of this new clausal temporal resolution method for establishing logical foundations for declarative temporal logic programming languages. The key element in the deduction systems for temporal logic is to deal with eventualities and hidden invariants that may prevent the fulfillment of eventualities. Different ways of addressing this issue can be found in the works on deduction systems for temporal logic. Traditional tableau systems for temporal logic generate an auxiliary graph in a first pass.Then, in a second pass, unsatisfiable nodes are pruned. In particular, the second pass must check whether the eventualities are fulfilled. The one-pass tableau calculus introduced by S. Schwendimann requires an additional handling of information in order to detect cyclic branches that contain unfulfilled eventualities. Regarding traditional sequent calculi for temporal logic, the issue of eventualities and hidden invariants is tackled by making use of a kind of inference rules (mainly, invariant-based rules or infinitary rules) that complicates their automation. A remarkable consequence of using either a two-pass approach based on auxiliary graphs or aone-pass approach that requires an additional handling of information in the tableau framework, and either invariant-based rules or infinitary rules in the sequent framework, is that temporal logic fails to carry out the classical correspondence between tableaux and sequents. In this thesis, we first provide a one-pass tableau method TTM that instead of a graph obtains a cyclic tree to decide whether a set of PLTL-formulas is satisfiable. In TTM tableaux are classical-like. For unsatisfiable sets of formulas, TTM produces tableaux whose leaves contain a formula and its negation. In the case of satisfiable sets of formulas, TTM builds tableaux where each fully expanded open branch characterizes a collection of models for the set of formulas in the root. The tableau method TTM is complete and yields a decision procedure for PLTL. This tableau method is directly associated to a one-sided sequent calculus called TTC. Since TTM is free from all the structural rules that hinder the mechanization of deduction, e.g. weakening and contraction, then the resulting sequent calculus TTC is also free from this kind of structural rules. In particular, TTC is free of any kind of cut, including invariant-based cut. From the deduction system TTC, we obtain a two-sided sequent calculus GTC that preserves all these good freeness properties and is finitary, sound and complete for PLTL. Therefore, we show that the classical correspondence between tableaux and sequent calculi can be extended to temporal logic. The most fruitful approach in the literature on resolution methods for temporal logic, which was started with the seminal paper of M. Fisher, deals with PLTL and requires to generate invariants for performing resolution on eventualities. In this thesis, we present a new approach to resolution for PLTL. The main novelty of our approach is that we do not generate invariants for performing resolution on eventualities. Our method is based on the dual methods of tableaux and sequents for PLTL mentioned above. Our resolution method involves translation into a clausal normal form that is a direct extension of classical CNF. We first show that any PLTL-formula can be transformed into this clausal normal form. Then, we present our temporal resolution method, called TRS-resolution, that extends classical propositional resolution. Finally, we prove that TRS-resolution is sound and complete. In fact, it finishes for any input formula deciding its satisfiability, hence it gives rise to a new decision procedure for PLTL. In the field of temporal logic programming, the declarative proposals that provide a completeness result do not allow eventualities, whereas the proposals that follow the imperative future approach either restrict the use of eventualities or deal with them by calculating an upper bound based on the small model property for PLTL. In the latter, when the length of a derivation reaches the upper bound, the derivation is given up and backtracking is used to try another possible derivation. In this thesis we present a declarative propositional temporal logic programming language, called TeDiLog, that is a combination of the temporal and disjunctive paradigms in Logic Programming. We establish the logical foundations of our proposal by formally defining operational and logical semantics for TeDiLog and by proving their equivalence. Since TeDiLog is, syntactically, a sublanguage of PLTL, the logical semantics of TeDiLog is supported by PLTL logical consequence. The operational semantics of TeDiLog is based on TRS-resolution. TeDiLog allows both eventualities and always-formulas to occur in clause heads and also in clause bodies. To the best of our knowledge, TeDiLog is the first declarative temporal logic programming language that achieves this high degree of expressiveness. Since the tableau method presented in this thesis is able to detect that the fulfillment of an eventuality is prevented by a hidden invariant without checking for it by means of an extra process, since our finitary sequent calculi do not include invariant-based rules and since our resolution method dispenses with invariant generation, we say that our deduction methods are invariant-free.

FTT-MA: A Flexible Time-Triggered Middleware Architecture for Time Sensitive, Resource-Aware AmI Systems

There is an increasing number of Ambient Intelligence (AmI) systems that are time-sensitive and resource-aware. From healthcare to building and even home/office automation, it is now common to find systems combining interactive and sensing multimedia traffic with relatively simple sensors and actuators (door locks, presence detectors, RFIDs, HVAC, information panels, etc.). Many of these are today known as Cyber-Physical Systems (CPS). Quite frequently, these systems must be capable of (1) prioritizing different traffic flows (process data, alarms, non-critical data, etc.), (2) synchronizing actions in several distributed devices and, to certain degree, (3) easing resource management (e.g., detecting faulty nodes, managing battery levels, handling overloads, etc.). This work presents FTT-MA, a high-level middleware architecture aimed at easing the design, deployment and operation of such AmI systems. FTT-MA ensures that both functional and non-functional aspects of the applications are met even during reconfiguration stages. The paper also proposes a methodology, together with a design tool, to create this kind of systems. Finally, a sample case study is presented that illustrates the use of the middleware and the methodology proposed in the paper.

Analytical efficiency evaluation of a network mobility management protocol for Intelligent Transportation Systems

One of the major concerns in an Intelligent Transportation System (ITS) scenario, such as that which may be found on a long-distance train service, is the provision of efficient communication services, satisfying users' expectations, and fulfilling even highly demanding application requirements, such as safety-oriented services. In an ITS scenario, it is common to have a significant amount of onboard devices that comprise a cluster of nodes (a mobile network) that demand connectivity to the outside networks. This demand has to be satisfied without service disruption. Consequently, the mobility of the mobile network has to be managed. Due to the nature of mobile networks, efficient and lightweight protocols are desired in the ITS context to ensure adequate service performance. However, the security is also a key factor in this scenario. Since the management of the mobility is essential for providing communications, the protocol for managing this mobility has to be protected. Furthermore, there are safety-oriented services in this scenario, so user application data should also be protected. Nevertheless, providing security is expensive in terms of efficiency. Based on this considerations, we have developed a solution for managing the network mobility for ITS scenarios: the NeMHIP protocol. This approach provides a secure management of network mobility in an efficient manner. In this article, we present this protocol and the strategy developed to maintain its security and efficiency in satisfactory levels. We also present the developed analytical models to analyze quantitatively the efficiency of the protocol. More specifically, we have developed models for assessing it in terms of signaling cost, which demonstrates that NeMHIP generates up to 73.47% less signaling compared to other relevant approaches. Therefore, the results obtained demonstrate that NeMHIP is the most efficient and secure solution for providing communications in mobile network scenarios such as in an ITS context.

Agent based modeling of energy networks

Attempts to model any present or future power grid face a huge challenge because a power grid is a complex system, with feedback and multi-agent behaviors, integrated by generation, distribution, storage and consumption systems, using various control and automation computing systems to manage electricity flows. Our approach to modeling is to build upon an established model of the low voltage electricity network which is tested and proven, by extending it to a generalized energy model. But, in order to address the crucial issues of energy efficiency, additional processes like energy conversion and storage, and further energy carriers, such as gas, heat, etc., besides the traditional electrical one, must be considered. Therefore a more powerful model, provided with enhanced nodes or conversion points, able to deal with multidimensional flows, is being required. This article addresses the issue of modeling a local multi-carrier energy network. This problem can be considered as an extension of modeling a low voltage distribution network located at some urban or rural geographic area. But instead of using an external power flow analysis package to do the power flow calculations, as used in electric networks, in this work we integrate a multiagent algorithm to perform the task, in a concurrent way to the other simulation tasks, and not only for the electric fluid but also for a number of additional energy carriers. As the model is mainly focused in system operation, generation and load models are not developed.

Energy Supply and the Sustainability of Endogenous Growth

29 p.

Valuation of wind energy projects: A real options approach

27 p.

Design and evaluation of an optical switching node

[EN]For a good development of elastic optical networks, the design of flexible optical switching nodes is required. This work analyses the previously proposed flexible architectures and, based on the most appropriate, which is the Architecture on Demand (AoD), proposes a specific configuration of the node that includes spatial and spectral switching and the wavelength conversion functionality with a low blocking probability and the minimum amount of modules; the characteristics of the traffic that the designed node is able to cope with are specified in the last chapter. An evaluation of the designed node is also done, and, compared to the other architectures, it is shown that the Architecture on Demand gives better results than others and that it has a higher potential for future developments.

Stability analysis of RF amplifiers based on MIMO pole-zero identification

Spurious oscillations are one of the principal issues faced by microwave and RF circuit designers. The rigorous detection of instabilities or the characterization of measured spurious oscillations is still an ongoing challenge. This project aims to create a new stability analysis CAD program that tackles this chal- lenge. Multiple Input Multiple Output (MIMO) pole-zero identification analysis is introduced on the program as a way to create new methods to automate the stability analysis process and to help designers comprehend the obtained results and prevent incorrect interpretations. The MIMO nature of the analysis contributes to eliminate possible controllability and observability losses and helps differentiate mathematical and physical quasi-cancellations, products of overmodeling. The created program reads Single Input Single Output (SISO) or MIMO frequency response data, and determines the corresponding continuous transfer functions with Vector Fitting. Once the transfer function is calculated, the corresponding pole/zero diagram is mapped enabling the designers to analyze the stability of an amplifier. Three data processing methods are introduced, two of which consist of pole/zero elimina- tions and the latter one on determining the critical nodes of an amplifier. The first pole/zero elimination method is based on eliminating non resonant poles, whilst the second method eliminates the poles with small residue by assuming that their effect on the dynamics of a system is small or non-existent. The critical node detection is also based on the residues; the node at which the effect of a pole on the dynamics is highest is defined as the critical node. In order to evaluate and check the efficiency of the created program, it is compared via examples with another existing commercial stability analysis tool (STAN tool). In this report, the newly created tool is proved to be as rigorous as STAN for detecting instabilities. Additionally, it is determined that the MIMO analysis is a very profitable addition to stability analysis, since it helps to eliminate possible problems of loss of controllability, observability and overmodeling.

Contributions to the efficient use of general purpose coprocessors: kernel density estimation as case study

142 p.

Contributions to High-Throughput Computing Based on the Peer-to-Peer Paradigm

XII, 116 p.

Bideratze arazoen ebazpenerako aplikatutako algoritmo metaheuristikoen diseinu, inplementazio eta konparaketa.

[EU]Proiektu honen helburua sare ezberdinetan algoritmo metaheuristikoen erabileraren bitartez bideratze arazoak ebaztea eta aztertzea da. Helburu honetarako erabiliko diren algoritmoak Coral Reefs Optimization eta Firefly Algorithm dira. Bi algoritmoak Python erabiliz inplementatuko dira, baita sareak simulatzen dituen programa ere. Modu honetan, algoritmo bakoitzaren gaitasuna aztertuko da sareko bi punturen arteko bide bideragarri bat, zeinek ezarritako murrizketak betetzen dituen, aurkitzeko; prozesu hau ausaz sortutako simulatutako sare batean oinarrituz garatuko da. Honen bitartez, arazo honen ebazpenerako algoritmo bakoitza egokia den eta bietariko zein den egokiena ondorioztatu ahalko da.

Caracterización del retardo en redes definidas por software para monitorizar el nivel de utilización de recursos.

[ES]Este proyecto busca caracterizar el retardo sufrido por los mensajes de estadísticas en las redes definidas por software cuando la red se encuentra en estado de saturación. Para ello, se utilizarán los paquetes OpenFlow que utiliza el controlador OpenDaylight para comunicarse con los nodos presentes en la red, a través de ellos se podrán monitorizar los recursos consumidos por los servicios instalados. Toda la monitorización se llevará a cabo desde el controlador, el módulo de monitorización optimizado en este proyecto permitirá al controlador conocer el valor promedio del ancho de banda consumido en instantes de tiempo de hasta un segundo en todos los nodos de la red donde se hayan instalado los servicios. Estos valores podrán ser utilizados para controlar el ancho de banda consumido por los distintos servicios dentro de una red, realizando acciones desde el propio controlador sobre aquellos servicios que superen el límite establecido.

Higher order vortex gyrotropic modes in circular ferromagnetic nanodots

Magnetic vortex that consists of an in-plane curling magnetization configuration and a needle-like core region with out-of-plane magnetization is known to be the ground state of geometrically confined submicron soft magnetic elements. Here magnetodynamics of relatively thick (50-100 nm) circular Ni80Fe20 dots were probed by broadband ferromagnetic resonance in the absence of external magnetic field. Spin excitation modes related to the thickness dependent vortex core gyrotropic dynamics were detected experimentally in the gigahertz frequency range. Both analytical theory and micromagnetic simulations revealed that these exchange dominated modes are flexure oscillations of the vortex core string with n = 0,1,2 nodes along the dot thickness. The intensity of the mode with n = 1 depends significantly on both dot thickness and diameter and in some cases is higher than the one of the uniform mode with n = 0. This opens promising perspectives in the area of spin transfer torque oscillators.