5 resultados para BitTorrent-like systems

em Archivo Digital para la Docencia y la Investigación - Repositorio Institucional de la Universidad del País Vasco


Relevância:

80.00% 80.00%

Publicador:

Resumo:

The aim of this technical report is to present some detailed explanations in order to help to understand and use the Message Passing Interface (MPI) parallel programming for solving several mixed integer optimization problems. We have developed a C++ experimental code that uses the IBM ILOG CPLEX optimizer within the COmputational INfrastructure for Operations Research (COIN-OR) and MPI parallel computing for solving the optimization models under UNIX-like systems. The computational experience illustrates how can we solve 44 optimization problems which are asymmetric with respect to the number of integer and continuous variables and the number of constraints. We also report a comparative with the speedup and efficiency of several strategies implemented for some available number of threads.

Relevância:

30.00% 30.00%

Publicador:

Resumo:

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.

Relevância:

30.00% 30.00%

Publicador:

Resumo:

[EN] This PhD work started in March 2010 with the support of the University of the Basque Country (UPV/EHU) under the program named “Formación de Personal Investigador” at the Chemical and Environmental Engineering Department in the Faculty of Engineering of Bilbao. The major part of the Thesis work was carried out in the mentioned department, as a member of the Sustainable Process Engineering (SuPrEn) research group. In addition, this PhD Thesis includes the research work developed during a period of 6 months at the Institut für Mikrotechnik Mainz GmbH, IMM, in Germany. During the four years of the Thesis, conventional and microreactor systems were tested for several feedstocks renewable and non-renewable, gases and liquids through several reforming processes in order to produce hydrogen. For this purpose, new catalytic formulations which showed high activity, selectivity and stability were design. As a consequence, the PhD work performed allowed the publication of seven scientific articles in peer-reviewed journals. This PhD Thesis is divided into the following six chapters described below. The opportunity of this work is established on the basis of the transition period needed for moving from a petroleum based energy system to a renewable based new one. Consequently, the present global energy scenario was detailed in Chapter 1, and the role of hydrogen as a real alternative in the future energy system was justified based on several outlooks. Therefore, renewable and non-renewable hydrogen production routes were presented, explaining the corresponding benefits and drawbacks. Then, the raw materials used in this Thesis work were described and the most important issues regarding the processes and the characteristics of the catalytic formulations were explained. The introduction chapter finishes by introducing the concepts of decentralized production and process intensification with the use of microreactors. In addition, a small description of these innovative reaction systems and the benefits that entailed their use were also mentioned. In Chapter 2 the main objectives of this Thesis work are summarized. The development of advanced reaction systems for hydrogen rich mixtures production is the main objective. In addition, the use and comparison between two different reaction systems, (fixed bed reactor (FBR) and microreactor), the processing of renewable raw materials, the development of new, active, selective and stable catalytic formulations, and the optimization of the operating conditions were also established as additional partial objectives. Methane and natural gas (NG) steam reforming experimental results obtained when operated with microreactor and FBR systems are presented in Chapter 3. For these experiments nickel-based (Ni/Al2O3 and Ni/MgO) and noble metal-based (Pd/Al2O3 and Pt/Al2O3) catalysts were prepared by wet impregnation and their catalytic activity was measured at several temperatures, from 973 to 1073 K, different S/C ratios, from 1.0 to 2.0, and atmospheric pressure. The Weight Hourly Space Velocity (WHSV) was maintained constant in order to compare the catalytic activity in both reaction systems. The results obtained showed a better performance of the catalysts operating in microreactors. The Ni/MgO catalyst reached the highest hydrogen production yield at 1073 K and steam-to-carbon ratio (S/C) of 1.5 under Steam methane Reforming (SMR) conditions. In addition, this catalyst also showed good activity and stability under NG reforming at S/C=1.0 and 2.0. The Ni/Al2O3 catalyst also showed high activity and good stability and it was the catalyst reaching the highest methane conversion (72.9 %) and H2out/CH4in ratio (2.4) under SMR conditions at 1073 K and S/C=1.0. However, this catalyst suffered from deactivation when it was tested under NG reforming conditions. Regarding the activity measurements carried out with the noble metal-based catalysts in the microreactor systems, they suffered a very quick deactivation, probably because of the effects attributed to carbon deposition, which was detected by Scanning Electron Microscope (SEM). When the FBR was used no catalytic activity was measured with the catalysts under investigation, probably because they were operated at the same WHSV than the microreactors and these WHSVs were too high for FBR system. In Chapter 4 biogas reforming processes were studied. This chapter starts with an introduction explaining the properties of the biogas and the main production routes. Then, the experimental procedure carried out is detailed giving concrete information about the experimental set-up, defining the parameters measured, specifying the characteristics of the reactors used and describing the characterization techniques utilized. Each following section describes the results obtained from activity testing with the different catalysts prepared, which is subsequently summarized: Section 4.3: Biogas reforming processes using γ-Al2O3 based catalysts The activity results obtained by several Ni-based catalysts and a bimetallic Rh-Ni catalyst supported on magnesia or alumina modified with oxides like CeO2 and ZrO2 are presented in this section. In addition, an alumina-based commercial catalyst was tested in order to compare the activity results measured. Four different biogas reforming processes were studied using a FBR: dry reforming (DR), biogas steam reforming (BSR), biogas oxidative reforming (BOR) and tri-reforming (TR). For the BSR process different steam to carbon ratios (S/C) from 1.0 to 3.0, were tested. In the case of BOR process the oxygen-to-methane (O2/CH4) ratio was varied from 0.125 to 0.50. Finally, for TR processes different S/C ratios from 1.0 to 3.0, and O2/CH4 ratios of 0.25 and 0.50 were studied. Then, the catalysts which achieved high activity and stability were impregnated in a microreactor to explore the viability of process intensification. The operation with microreactors was carried out under the best experimental conditions measured in the FBR. In addition, the physicochemical characterization of the fresh and spent catalysts was carried out by Inductively Coupled Plasma Atomic Emission Spectroscopy (ICP-AES), N2 physisorption, H2 chemisorption, Temperature Programmed Reduction (TPR), SEM, X-ray Photoelectron Spectroscopy (XPS) and X-ray powder Diffraction (XRD). Operating with the FBR, conversions close to the ones predicted by thermodynamic calculations were obtained by most of the catalysts tested. The Rh-Ni/Ce-Al2O3 catalyst obtained the highest hydrogen production yield in DR. In BSR process, the Ni/Ce-Al2O3 catalyst achieved the best activity results operating at S/C=1.0. In the case of BOR process, the Ni/Ce-Zr-Al2O3 catalyst showed the highest reactants conversion values operating at O2/CH4=0.25. Finally, in the TR process the Rh-Ni/Ce-Al2O3 catalyst obtained the best results operating at S/C=1.0 and O2/CH4=0.25. Therefore, these three catalysts were selected to be coated onto microchannels in order to test its performance under BOR and TR processes conditions. Although the operation using microreactors was carried out under considerably higher WHSV, similar conversions and yields as the ones measured in FBR were measured. Furthermore, attending to other measurements like Turnover Frequency (TOF) and Hydrogen Productivity (PROD), the values calculated for the catalysts tested in microreactors were one order of magnitude higher. Thus, due to the low dispersion degree measured by H2-chemisorption, the Ni/Ce-Al2O3 catalyst reached the highest TOF and PROD values. Section 4.4: Biogas reforming processes using Zeolites L based catalysts In this section three type of L zeolites, with different morphology and size, were synthesized and used as catalyst support. Then, for each type of L zeolite three nickel monometallic and their homologous Rh-Ni bimetallic catalysts were prepared by the wetness impregnation method. These catalysts were tested using the FBR under DR process and different conditions of BSR (S/C ratio of 1.0 and 2.0), BOR (O2/CH4 ratio of 0.25 and 0.50) and TR processes (at S/C=1.0 and O2/CH4=0.25). The characterization of these catalysts was also carried out by using the same techniques mentioned in the previous section. Very high methane and carbon dioxide conversion values were measured for almost all the catalysts under investigation. The experimental results evidenced the better catalytic behavior of the bimetallic catalysts as compared to the monometallic ones. Comparing the catalysts behavior with regards to their morphology, for the BSR process the Disc catalysts were the most active ones at the lowest S/C ratio tested. On the contrary, the Cylindrical (30–60 nm) catalysts were more active under BOR conditions at O2/CH4=0.25 and TR processes. By the contrary, the Cylindrical (1–3 µm) catalysts showed the worst activity results for both processes. Section 4.5: Biogas reforming processes using Na+ and Cs+ doped Zeolites LTL based catalysts A method for the synthesis of Linde Type L (LTL) zeolite under microwave-assisted hydrothermal conditions and its behavior as a support for heterogeneously catalyzed hydrogen production is described in this section. Then, rhodium and nickel-based bimetallic catalysts were prepared in order to be tested by DR process and BOR process at O2/CH4=0.25. Moreover, the characterization of the catalysts under investigation was also carried out. Higher activities were achieved by the catalysts prepared from the non-doped zeolites, Rh-Ni/D and Rh-Ni/N, as compared to the ones supported on Na+ and Cs+ exchanged supports. However, the differences between them were not very significant. In addition, the Na+ and Cs+ incorporation affected mainly to the Disc catalysts. Comparing the results obtained by these catalysts with the ones studied in the section 4.4, in general worst results were achieved under DR conditions and almost the same results when operated under BOR conditions. In Chapter 5 the ethylene glycol (EG) as feed for syngas production by steam reforming (SR) and oxidative steam reforming (OSR) was studied by using microchannel reactors. The product composition was determined at a S/C of 4.0, reaction temperatures between 625°C and 725°C, atmospheric pressure and Volume Hourly Space Velocities (VHSV) between 100 and 300 NL/(gcath). This work was divided in two sections. The first one corresponds to the introduction of the main and most promising EG production routes. Then, the new experimental procedure is detailed and the information about the experimental set-up and the measured parameters is described. The characterization was carried out using the same techniques as for the previous chapter. Then, the next sections correspond to the catalytic activity and catalysts characterization results. Section 5.3: xRh-cm and xRh-np catalysts for ethylene glycol reforming Initially, catalysts with different rhodium loading, from 1.0 to 5.0 wt. %, and supported on α-Al2O3 were prepared by two different preparation methods (conventional impregnation and separate nanoparticle synthesis). Then, the catalysts were compared regarding their measured activity and selectivity, as well as the characterization results obtained before and after the activity tests carried out. The samples prepared by a conventional impregnation method showed generally higher activity compared to catalysts prepared from Rh nanoparticles. By-product formation of species such as acetaldehyde, ethane and ethylene was detected, regardless if oxygen was added to the feed or not. Among the catalysts tested, the 2.5Rh-cm catalyst was considered the best one. Section 5.4: 2.5Rh-cm catalyst support modification with CeO2 and La2O3 In this part of the Chapter 5, the catalyst showing the best performance in the previous section, the 2.5Rh-Al2O3 catalyst, was selected in order to be improved. Therefore, new Rh based catalysts were designed using α-Al2O3 and being modified this support with different contents of CeO2 or La2O3 oxides. All the catalysts containing additives showed complete conversion and selectivities close to the equilibrium in both SR and OSR processes. In addition, for these catalysts the concentrations measured for the C2H4, CH4, CH3CHO and C2H6 by-products were very low. Finally, the 2.5Rh-20Ce catalyst was selected according to its catalytic activity and characterization results in order to run a stability test, which lasted more than 115 hours under stable operation. The last chapter, Chapter 6, summarizes the main conclusions achieved throughout this Thesis work. Although very high reactant conversions and rich hydrogen mixtures were obtained using a fixed bed reaction system, the use of microreactors improves the key issues, heat and mass transfer limitations, through which the reforming reactions are intensified. Therefore, they seem to be a very interesting and promising alternative for process intensification and decentralized production for remote application.

Relevância:

30.00% 30.00%

Publicador:

Resumo:

Nowadays, Power grids are critical infrastructures on which everything else relies, and their correct behavior is of the highest priority. New smart devices are being deployed to be able to manage and control power grids more efficiently and avoid instability. However, the deployment of such smart devices like Phasor Measurement Units (PMU) and Phasor Data Concentrators (PDC), open new opportunities for cyber attackers to exploit network vulnerabilities. If a PDC is compromised, all data coming from PMUs to that PDC is lost, reducing network observability. Our approach to solve this problem is to develop an Intrusion detection System (IDS) in a Software-defined network (SDN). allowing the IDS system to detect compromised devices and use that information as an input for a self-healing SDN controller, which redirects the data of the PMUs to a new, uncompromised PDC, maintaining the maximum possible network observability at every moment. During this research, we have successfully implemented Self-healing in an example network with an SDN controller based on Ryu controller. We have also assessed intrinsic vulnerabilities of Wide Area Management Systems (WAMS) and SCADA networks, and developed some rules for the Intrusion Detection system which specifically protect vulnerabilities of these networks. The integration of the IDS and the SDN controller was also successful. \\To achieve this goal, the first steps will be to implement an existing Self-healing SDN controller and assess intrinsic vulnerabilities of Wide Area Measurement Systems (WAMS) and SCADA networks. After that, we will integrate the Ryu controller with Snort, and create the Snort rules that are specific for SCADA or WAMS systems and protocols.