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.

Floquet generation of Majorana end modes and topological invariants

We show how Majorana end modes can be generated in a one-dimensional system by varying some of the parameters in the Hamiltonian periodically in time. The specific model we consider is a chain containing spinless electrons with a nearest-neighbor hopping amplitude, a p-wave superconducting term, and a chemical potential; this is equivalent to a spin-1/2 chain with anisotropic XY couplings between nearest neighbors and a magnetic field applied in the (z) over cap direction. We show that varying the chemical potential (or magnetic field) periodically in time can produce Majorana modes at the ends of a long chain. We discuss two kinds of periodic driving, periodic delta-function kicks, and a simple harmonic variation with time. We discuss some distinctive features of the end modes such as the inverse participation ratio of their wave functions and their Floquet eigenvalues which are always equal to +/- 1 for time-reversal-symmetric systems. For the case of periodic delta-function kicks, we use the effective Hamiltonian of a system with periodic boundary conditions to define two topological invariants. The first invariant is a well-known winding number, while the second invariant has not appeared in the literature before. The second invariant is more powerful in that it always correctly predicts the numbers of end modes with Floquet eigenvalues equal to + 1 and -1, while the first invariant does not. We find that the number of end modes can become very large as the driving frequency decreases. We show that periodic delta-function kicks in the hopping and superconducting terms can also produce end modes. Finally, we study the effect of electron-phonon interactions (which are relevant at finite temperatures) and a random noise in the chemical potential on the Majorana modes.

Automatic visual dictionary generation through Optimum-Path Forest clustering

Image categorization by means of bag of visual words has received increasing attention by the image processing and vision communities in the last years. In these approaches, each image is represented by invariant points of interest which are mapped to a Hilbert Space representing a visual dictionary which aims at comprising the most discriminative features in a set of images. Notwithstanding, the main problem of such approaches is to find a compact and representative dictionary. Finding such representative dictionary automatically with no user intervention is an even more difficult task. In this paper, we propose a method to automatically find such dictionary by employing a recent developed graph-based clustering algorithm called Optimum-Path Forest, which does not make any assumption about the visual dictionary's size and is more efficient and effective than the state-of-the-art techniques used for dictionary generation. © 2012 IEEE.

Automatic visual dictionary generation through optimum-path forest clusteringautomatic visual dictionary generation through optimum-path forest clustering

Image categorization by means of bag of visual words has received increasing attention by the image processing and vision communities in the last years. In these approaches, each image is represented by invariant points of interest which are mapped to a Hilbert Space representing a visual dictionary which aims at comprising the most discriminative features in a set of images. Notwithstanding, the main problem of such approaches is to find a compact and representative dictionary. Finding such representative dictionary automatically with no user intervention is an even more difficult task. In this paper, we propose a method to automatically find such dictionary by employing a recent developed graph-based clustering algorithm called Optimum-Path Forest, which does not make any assumption about the visual dictionary's size and is more efficient and effective than the state-of-the-art techniques used for dictionary generation.

Advanced signal and receiver design for next generation OFDM systems

This thesis deal with the design of advanced OFDM systems. Both waveform and receiver design have been treated. The main scope of the Thesis is to study, create, and propose, ideas and novel design solutions able to cope with the weaknesses and crucial aspects of modern OFDM systems. Starting from the the transmitter side, the problem represented by low resilience to non-linear distortion has been assessed. A novel technique that considerably reduces the Peak-to-Average Power Ratio (PAPR) yielding a quasi constant signal envelope in the time domain (PAPR close to 1 dB) has been proposed.The proposed technique, named Rotation Invariant Subcarrier Mapping (RISM),is a novel scheme for subcarriers data mapping,where the symbols belonging to the modulation alphabet are not anchored, but maintain some degrees of freedom. In other words, a bit tuple is not mapped on a single point, rather it is mapped onto a geometrical locus, which is totally or partially rotation invariant. The final positions of the transmitted complex symbols are chosen by an iterative optimization process in order to minimize the PAPR of the resulting OFDM symbol. Numerical results confirm that RISM makes OFDM usable even in severe non-linear channels. Another well known problem which has been tackled is the vulnerability to synchronization errors. Indeed in OFDM system an accurate recovery of carrier frequency and symbol timing is crucial for the proper demodulation of the received packets. In general, timing and frequency synchronization is performed in two separate phases called PRE-FFT and POST-FFT synchronization. Regarding the PRE-FFT phase, a novel joint symbol timing and carrier frequency synchronization algorithm has been presented. The proposed algorithm is characterized by a very low hardware complexity, and, at the same time, it guarantees very good performance in in both AWGN and multipath channels. Regarding the POST-FFT phase, a novel approach for both pilot structure and receiver design has been presented. In particular, a novel pilot pattern has been introduced in order to minimize the occurrence of overlaps between two pattern shifted replicas. This allows to replace conventional pilots with nulls in the frequency domain, introducing the so called Silent Pilots. As a result, the optimal receiver turns out to be very robust against severe Rayleigh fading multipath and characterized by low complexity. Performance of this approach has been analytically and numerically evaluated. Comparing the proposed approach with state of the art alternatives, in both AWGN and multipath fading channels, considerable performance improvements have been obtained. The crucial problem of channel estimation has been thoroughly investigated, with particular emphasis on the decimation of the Channel Impulse Response (CIR) through the selection of the Most Significant Samples (MSSs). In this contest our contribution is twofold, from the theoretical side, we derived lower bounds on the estimation mean-square error (MSE) performance for any MSS selection strategy,from the receiver design we proposed novel MSS selection strategies which have been shown to approach these MSE lower bounds, and outperformed the state-of-the-art alternatives. Finally, the possibility of using of Single Carrier Frequency Division Multiple Access (SC-FDMA) in the Broadband Satellite Return Channel has been assessed. Notably, SC-FDMA is able to improve the physical layer spectral efficiency with respect to single carrier systems, which have been used so far in the Return Channel Satellite (RCS) standards. However, it requires a strict synchronization and it is also sensitive to phase noise of local radio frequency oscillators. For this reason, an effective pilot tone arrangement within the SC-FDMA frame, and a novel Joint Multi-User (JMU) estimation method for the SC-FDMA, has been proposed. As shown by numerical results, the proposed scheme manages to satisfy strict synchronization requirements and to guarantee a proper demodulation of the received signal.

Defining the role of IL-15 trans-presentation by distinct cell-types during the development and homeostasis of Natural Killer and invariant Natural Killer T cells

The immuno-regulatory functions displayed by NK and iNKT cells have highlighted their importance as key lymphocytes involved in innate and adaptive immunity. Therefore, understanding the dynamics influencing the generation of NK and iNKT cells is extremely important. IL-15 has been shown to provide a critical signal throughout the development and homeostasis of NK and iNKT cells; however, the cellular source of IL-15 has remained unclear. In this investigation, I provide evidence that the cell-type providing IL-15 to NK and iNKT cells via trans-presentation is determined by the tissue site and the maturation status of NK and iNKT cells. For NK cells, I revealed the non-hematopoietic compartment provides IL-15 to NK cells in the early stages of development while hematopoietic cells were crucial for the generation and maintenance of mature NK cells. Regarding iNKT cells in the thymus, IL-15 trans-presentation by non-hematopoietic cells was crucial for the survival of mature iNKT cells. In the liver, both hematopoietic and non-hematopoietic compartments provided IL-15 to both immature and mature iNKT cells. This IL-15 signal helped mediate the survival and proliferation of both NK and iNKT cells as well as induce the functional maturation of mature iNKT cells via enhanced T-bet expression. In conclusion, my work illustrates an important notion that the immunological niche of NK and iNKT cells is tightly regulated and that this regulation is meticulously influenced by the tissue microenvironment.

Isotone Recursive Methods for Overlapping Generation Models with Stochastic Nonclassical Production

Based on an order-theoretic approach, we derive sufficient conditions for the existence, characterization, and computation of Markovian equilibrium decision processes and stationary Markov equilibrium on minimal state spaces for a large class of stochastic overlapping generations models. In contrast to all previous work, we consider reduced-form stochastic production technologies that allow for a broad set of equilibrium distortions such as public policy distortions, social security, monetary equilibrium, and production nonconvexities. Our order-based methods are constructive, and we provide monotone iterative algorithms for computing extremal stationary Markov equilibrium decision processes and equilibrium invariant distributions, while avoiding many of the problems associated with the existence of indeterminacies that have been well-documented in previous work. We provide important results for existence of Markov equilibria for the case where capital income is not increasing in the aggregate stock. Finally, we conclude with examples common in macroeconomics such as models with fiat money and social security. We also show how some of our results extend to settings with unbounded state spaces.

Biosynthesis of major histocompatibility complex molecules and generation of T cells in Ii TAP1 double-mutant mice.

Major histocompatibility complex (MHC) class I and II molecules are loaded with peptides in distinct subcellular compartments. The transporter associated with antigen processing (TAP) is responsible for delivering peptides derived from cytosolic proteins to the endoplasmic reticulum, where they bind to class I molecules, while the invariant chain (Ii) directs class II molecules to endosomal compartments, where they bind peptides originating mostly from exogenous sources. Mice carrying null mutations of the TAP1 or Ii genes (TAP10) or Ii0, respectively) have been useful tools for elucidating the two MHC/peptide loading pathways. To evaluate to what extent these pathways functionally intersect, we have studied the biosynthesis of MHC molecules and the generation of T cells in Ii0TAP10 double-mutant mice. We find that the assembly and expression of class II molecules in Ii0 and Ii0TAP10 animals are indistinguishable and that formation and display of class I molecules is the same in TAP10 and Ii0TAP10 animals. Thymic selection in the double mutants is as expected, with reduced numbers of both CD4+ CD8- and CD4- CD8+ thymocyte compartments. Surprisingly, lymph node T-cell populations look almost normal; we propose that population expansion of peripheral T cells normalizes the numbers of CD4+ and CD8+ cells in Ii0TAP10 mice.

Proteolysis of major histocompatibility complex class II-associated invariant chain is regulated by the alternatively spliced gene product, p41.

Invariant chain (Ii) is an intracellular type II transmembrane glycoprotein that is associated with major histocompatibility complex class II molecules during biosynthesis. Ii exists in two alternatively spliced forms, p31 and p41. Both p31 and p41 facilitate folding of class II molecules, promote egress from the endoplasmic reticulum, prevent premature peptide binding, and enhance localization to proteolytic endosomal compartments that are thought to be the sites for Ii degradation, antigen processing, and class II-peptide association. In spite of the dramatic and apparently equivalent effects that p31 and p41 have on class II biosynthesis, the ability of invariant chain to enhance antigen presentation to T cells is mostly restricted to p41. Here we show that degradation of Ii leads to the generation of a 12-kDa amino-terminal fragment that in p41-positive, but not in p31-positive, cells remains associated with class II molecules for an extended time. Interestingly, we find that coexpression of the two isoforms results in a change in the pattern of p31 degradation such that endosomal processing of p31 also leads to extended association of a similar 12-kDa fragment with class II molecules. These data raise the possibility that p41 may have the ability to impart its pattern of proteolytic processing on p31 molecules expressed in the same cells. This would enable a small number of p41 molecules to modify the post-translational transport and/or processing of an entire cohort of class II-Ii complexes in a manner that could account for the unique ability of p41 to enhance antigen presentation.

Principal component and second generation wavelet analysis of Treasury yield curve evolution

Prices of U.S. Treasury securities vary over time and across maturities. When the market in Treasurys is sufficiently complete and frictionless, these prices may be modeled by a function time and maturity. A cross-section of this function for time held fixed is called the yield curve; the aggregate of these sections is the evolution of the yield curve. This dissertation studies aspects of this evolution. ^ There are two complementary approaches to the study of yield curve evolution here. The first is principal components analysis; the second is wavelet analysis. In both approaches both the time and maturity variables are discretized. In principal components analysis the vectors of yield curve shifts are viewed as observations of a multivariate normal distribution. The resulting covariance matrix is diagonalized; the resulting eigenvalues and eigenvectors (the principal components) are used to draw inferences about the yield curve evolution. ^ In wavelet analysis, the vectors of shifts are resolved into hierarchies of localized fundamental shifts (wavelets) that leave specified global properties invariant (average change and duration change). The hierarchies relate to the degree of localization with movements restricted to a single maturity at the base and general movements at the apex. Second generation wavelet techniques allow better adaptation of the model to economic observables. Statistically, the wavelet approach is inherently nonparametric while the wavelets themselves are better adapted to describing a complete market. ^ Principal components analysis provides information on the dimension of the yield curve process. While there is no clear demarkation between operative factors and noise, the top six principal components pick up 99% of total interest rate variation 95% of the time. An economically justified basis of this process is hard to find; for example a simple linear model will not suffice for the first principal component and the shape of this component is nonstationary. ^ Wavelet analysis works more directly with yield curve observations than principal components analysis. In fact the complete process from bond data to multiresolution is presented, including the dedicated Perl programs and the details of the portfolio metrics and specially adapted wavelet construction. The result is more robust statistics which provide balance to the more fragile principal components analysis. ^

Dynamical generation of a gauge symmetry in the double-exchange model

It is shown that a bosonic formulation of the double-exchange model, one of the classical models for magnetism, generates dynamically a gauge-invariant phase in a finite region of the phase diagram. We use analytical methods, Monte Carlo simulations and finite-size scaling analysis. We study the transition line between that region and the paramagnetic phase. The numerical results show that this transition line belongs to the universality class of the antiferromagnetic RP^(2) model. The fact that one can define a universality class for the antiferromagnetic RP^(2) model, different from the one of the O(N) models, is puzzling and somehow contradicts naive expectations about universality.