OpenRaiser/Intern-Atlas huggingface dataset:
Polynomial Interpretations for Higher-Order Rewriting
Venue: arXiv cs.LO 2012
Year: 2012

The termination method of weakly monotonic algebras, which has been defined for higher-order rewriting in the HRS formalism, offers a lot of power, but has seen little use in recent years. We adapt and extend this method to the alternative formalism of algebraic functional systems, where the simply-typed lambda-calculus is combined with algebraic reduction. Using this theory, we define higher-order polynomial interpretations, and show how the implementation challenges of this technique can be tackled. A full implementation is provided in the termination tool WANDA.
A 100 mA Low Voltage Linear Regulators for Systems on Chip Applications Using 0.18 μm CMOS Technology
Venue: arXiv cs.OH 2012
Year: 2012

A novel design for a low dropout (LDO) voltage regulator is presented and dedicated to power many sections of a typical cellular handset. However, these baseband, RF, and audio sections have different requirements that influence which LDO is most appropriate. After discussion of the specific requirements, different LDOs are recommended. Also, some LDO design techniques are briefly discussed to demonstrate how an LDO may be optimized for a specific level of performance. Cellular phone designs require linear regulators with lowdropout, low-noise, high PSRR, low quiescent current (Iq), and low-cost. They need to deliver a stable output and use smallvalue output capacitors. Ideally, one device would have all these characteristics and one low-dropout linear regulator (LDO) could be used anywhere in the phone without worry. But in practice, the various cell phone blocks are best powered by LDOs with different performance characteristics. This paper provides a new design methodology to choosing the right LDO to power each cell phone and especially for the Voltage Phase-Locked loops (VPLLs) blocks. Fabricated in a 0.18 μm CMOS process, the measured results show the adopted topology achieves a better phase noise than the conventional saturation current source. and the spread of the current limitation (without matching) is 100mA, the VPLLs system demonstrates a phase noise of 782 nv/sqrtHz at 100-kHz, and 33 nv/sqrtHz at 1 MHz, while quiescent current 33 μA from a 2.6 V supply voltage.
Coalitions in nonatomic network congestion games
Venue: arXiv cs.GT 2012
Year: 2012

This work shows that the formation of a finite number of coalitions in a nonatomic network congestion game benefits everyone. At the equilibrium of the composite game played by coalitions and individuals, the average cost to each coalition and the individuals' common cost are all lower than in the corresponding nonatomic game (without coalitions). The individuals' cost is lower than the average cost to any coalition. Similarly, the average cost to a coalition is lower than that to any larger coalition. Whenever some members of a coalition become individuals, the individuals' payoff is increased. In the case of a unique coalition, both the average cost to the coalition and the individuals' cost are decreasing with respect to the size of the coalition. In a sequence of composite games, if a finite number of coalitions are fixed, while the size of the remaining coalitions goes to zero, the equilibria of these games converge to the equilibrium of a composite game played by the same fixed coalitions and the remaining individuals.
A Coordinated Approach to Channel Estimation in Large-scale Multiple-antenna Systems
Venue: arXiv cs.IT 2012
Year: 2012

This paper addresses the problem of channel estimation in multi-cell interference-limited cellular networks. We consider systems employing multiple antennas and are interested in both the finite and large-scale antenna number regimes (so-called "massive MIMO"). Such systems deal with the multi-cell interference by way of per-cell beamforming applied at each base station. Channel estimation in such networks, which is known to be hampered by the pilot contamination effect, constitute a major bottleneck for overall performance. We present a novel approach which tackles this problem by enabling a low-rate coordination between cells during the channel estimation phase itself. The coordination makes use of the additional second-order statistical information about the user channels, which are shown to offer a powerful way of discriminating across interfering users with even strongly correlated pilot sequences. Importantly, we demonstrate analytically that in the large-number-of-antennas regime, the pilot contamination effect is made to vanish completely under certain conditions on the channel covariance. Gains over the conventional channel estimation framework are confirmed by our simulations for even small antenna array sizes.
Adaptive group testing as channel coding with feedback
Venue: arXiv cs.IT 2012
Year: 2012

Group testing is the combinatorial problem of identifying the defective items in a population by grouping items into test pools. Recently, nonadaptive group testing - where all the test pools must be decided on at the start - has been studied from an information theory point of view. Using techniques from channel coding, upper and lower bounds have been given on the number of tests required to accurately recover the defective set, even when the test outcomes can be noisy. In this paper, we give the first information theoretic result on adaptive group testing - where the outcome of previous tests can influence the makeup of future tests. We show that adaptive testing does not help much, as the number of tests required obeys the same lower bound as nonadaptive testing. Our proof uses similar techniques to the proof that feedback does not improve channel capacity.
Probabilistic Recovery Guarantees for Sparsely Corrupted Signals
Venue: arXiv cs.IT 2012
Year: 2012

We consider the recovery of sparse signals subject to sparse interference, as introduced in Studer et al., IEEE Trans. IT, 2012. We present novel probabilistic recovery guarantees for this framework, covering varying degrees of knowledge of the signal and interference support, which are relevant for a large number of practical applications. Our results assume that the sparsifying dictionaries are characterized by coherence parameters and we require randomness only in the signal and/or interference. The obtained recovery guarantees show that one can recover sparsely corrupted signals with overwhelming probability, even if the sparsity of both the signal and interference scale (near) linearly with the number of measurements.
Revisiting the D-iteration method: from theoretical to practical computation cost
Venue: arXiv cs.NA 2012
Year: 2012

In this paper, we revisit the D-iteration algorithm in order to better explain its connection to the Gauss-Seidel method and different performance results that were observed. In particular, we study here the practical computation cost based on the execution runtime compared to the theoretical number of iterations. We also propose an exact formula of the error for PageRank class of equations.
A Programmer-Centric Approach to Program Verification in ATS
Venue: arXiv cs.PL 2012
Year: 2012

Formal specification is widely employed in the construction of high-quality software. However, there is often a huge gap between formal specification and actual implementation. While there is already a vast body of work on software testing and verification, the task to ensure that an implementation indeed meets its specification is still undeniably of great difficulty. ATS is a programming language equipped with a highly expressive type system that allows the programmer to specify and implement and then verify within the language itself that an implementation meets its specification. In this paper, we present largely through examples a programmer-centric style of program verification that puts emphasis on requesting the programmer to explain in a literate fashion why his or her code works. This is a solid step in the pursuit of software construction that is verifiably correct according to specification.
Power Control in Multi-Layer Cellular Networks
Venue: arXiv cs.NI 2012
Year: 2012

We investigate the possible performance gains of power control in multi-layer cellular systems where microcells and picocells are distributed within macrocells. Although multilayers in cellular networks help increase system capacity and coverage, and can reduce total energy consumption; they cause interference, reducing the performance of the network. Therefore, downlink transmit power levels of multi-layer hierarchical cellular networks need to be controlled in order to fully exploit their benefits. In this work, we present an analytical derivation to determine optimum power levels for two-layer cellular networks and generalize our solution to multi-layer cellular networks. We also simulate our results in a typical multi-layer network setup and observe significant power savings compared to single-layer cellular networks.
Tree Transducers, Machine Translation, and Cross-Language Divergences
Venue: arXiv cs.CL 2012
Year: 2012

Tree transducers are formal automata that transform trees into other trees. Many varieties of tree transducers have been explored in the automata theory literature, and more recently, in the machine translation literature. In this paper I review T and xT transducers, situate them among related formalisms, and show how they can be used to implement rules for machine translation systems that cover all of the cross-language structural divergences described in Bonnie Dorr's influential article on the topic. I also present an implementation of xT transduction, suitable and convenient for experimenting with translation rules.
On Graph Refutation for Relational Inclusions
Venue: arXiv cs.LO 2012
Year: 2012

We introduce a graphical refutation calculus for relational inclusions: it reduces establishing a relational inclusion to establishing that a graph constructed from it has empty extension. This sound and complete calculus is conceptually simpler and easier to use than the usual ones.
Integrated Solution Modeling Software: A New Paradigm on Information Security Review and Assessment
Venue: arXiv cs.CR 2012
Year: 2012

Actually Information security becomes a very important part for the organization's intangible assets, so level of confidence and stakeholder trusted are performance indicator as successes organization. Since information security has a very important role in supporting the activities of the organization, we need a standard or benchmark which regulates governance over information security. The main objective of this paper is to implement a novel practical approach framework to the development of information security management system (ISMS) assessment and monitoring software, called by I-SolFramework. System / software is expected to assist stakeholders in assessing the level of their ISO27001 compliance readiness, the software could help stakeholders understood security control or called by compliance parameters, being shorter and more structured. The case study illustrated provided to the reader with a set of guidelines, that aims easy understood and applicable as measuring tools for ISMS standards (ISO27001) compliance.
Optimal Pruning for Multi-Step Sensor Scheduling
Venue: arXiv cs.SY 2012
Year: 2012

In the considered linear Gaussian sensor scheduling problem, only one sensor out of a set of sensors performs a measurement. To minimize the estimation error over multiple time steps in a computationally tractable fashion, the so-called information-based pruning algorithm is proposed. It utilizes the information matrices of the sensors and the monotonicity of the Riccati equation. This allows ordering sensors according to their information contribution and excluding many of them from scheduling. Additionally, a tight lower is calculated for branch-and-bound search, which further improves the pruning performance.
A study of the universal threshold in the L1 recovery by statistical mechanics
Venue: arXiv cs.IT 2012
Year: 2012

We discuss the universality of the L1 recovery threshold in compressed sensing. Previous studies in the fields of statistical mechanics and random matrix integration have shown that L1 recovery under a random matrix with orthogonal symmetry has a universal threshold. This indicates that the threshold of L1 recovery under a non-orthogonal random matrix differs from the universal one. Taking this into account, we use a simple random matrix without orthogonal symmetry, where the random entries are not independent, and show analytically that the threshold of L1 recovery for such a matrix does not coincide with the universal one. The results of an extensive numerical experiment are in good agreement with the analytical results, which validates our methodology. Though our analysis is based on replica heuristics in statistical mechanics and is not rigorous, the findings nevertheless support the fact that the universality of the threshold is strongly related to the symmetry of the random matrix.
Joint Base Station Clustering and Beamformer Design for Partial Coordinated Transmission in Heterogenous Networks
Venue: arXiv cs.IT 2012
Year: 2012

We consider the interference management problem in a multicell MIMO heterogenous network. Within each cell there are a large number of distributed micro/pico base stations (BSs) that can be potentially coordinated for joint transmission. To reduce coordination overhead, we consider user-centric BS clustering so that each user is served by only a small number of (potentially overlapping) BSs. Thus, given the channel state information, our objective is to jointly design the BS clustering and the linear beamformers for all BSs in the network. In this paper, we formulate this problem from a {sparse optimization} perspective, and propose an efficient algorithm that is based on iteratively solving a sequence of group LASSO problems. A novel feature of the proposed algorithm is that it performs BS clustering and beamformer design jointly rather than separately as is done in the existing approaches for partial coordinated transmission. Moreover, the cluster size can be controlled by adjusting a single penalty parameter in the nonsmooth regularized utility function. The convergence of the proposed algorithm (to a local optimal solution) is guaranteed, and its effectiveness is demonstrated via extensive simulation.
Formal Abstraction of Linear Systems via Polyhedral Lyapunov Functions
Venue: arXiv cs.SY 2012
Year: 2012

In this paper we present an abstraction algorithm that produces a finite bisimulation quotient for an autonomous discrete-time linear system. We assume that the bisimulation quotient is required to preserve the observations over an arbitrary, finite number of polytopic subsets of the system state space. We generate the bisimulation quotient with the aid of a sequence of contractive polytopic sublevel sets obtained via a polyhedral Lyapunov function. The proposed algorithm guarantees that at iteration $i$, the bisimulation of the system within the $i$-th sublevel set of the Lyapunov function is completed. We then show how to use the obtained bisimulation quotient to verify the system with respect to arbitrary Linear Temporal Logic formulas over the observed regions.
Towards a Tool-based Development Methodology for Pervasive Computing Applications
Venue: arXiv cs.PL 2012
Year: 2012

Despite much progress, developing a pervasive computing application remains a challenge because of a lack of conceptual frameworks and supporting tools. This challenge involves coping with heterogeneous devices, overcoming the intricacies of distributed systems technologies, working out an architecture for the application, encoding it in a program, writing specific code to test the application, and finally deploying it. This paper presents a design language and a tool suite covering the development life-cycle of a pervasive computing application. The design language allows to define a taxonomy of area-specific building-blocks, abstracting over their heterogeneity. This language also includes a layer to define the architecture of an application, following an architectural pattern commonly used in the pervasive computing domain. Our underlying methodology assigns roles to the stakeholders, providing separation of concerns. Our tool suite includes a compiler that takes design artifacts written in our language as input and generates a programming framework that supports the subsequent development stages, namely implementation, testing, and deployment. Our methodology has been applied on a wide spectrum of areas. Based on these experiments, we assess our approach through three criteria: expressiveness, usability, and productivity.
Solving Mahjong Solitaire boards with peeking
Venue: arXiv cs.CC 2012
Year: 2012

We first prove that solving Mahjong Solitaire boards with peeking is NP-complete, even if one only allows isolated stacks of the forms /aab/ and /abb/. We subsequently show that layouts of isolated stacks of heights one and two can always be solved with peeking, and that doing so is in P, as well as finding an optimal algorithm for such layouts without peeking. Next, we describe a practical algorithm for solving Mahjong Solitaire boards with peeking, which is simple and fast. The algorithm uses an effective pruning criterion and a heuristic to find and prioritize critical groups. The ideas of the algorithm can also be applied to solving Shisen-Sho with peeking.
Fast Matrix Rank Algorithms and Applications
Venue: arXiv cs.DS 2012
Year: 2012

We consider the problem of computing the rank of an m x n matrix A over a field. We present a randomized algorithm to find a set of r = rank(A) linearly independent columns in Õ(|A| + r^ω) field operations, where |A| denotes the number of nonzero entries in A and ω< 2.38 is the matrix multiplication exponent. Previously the best known algorithm to find a set of r linearly independent columns is by Gaussian elimination, with running time O(mnr^{ω-2}). Our algorithm is faster when r < max(m,n), for instance when the matrix is rectangular. We also consider the problem of computing the rank of a matrix dynamically, supporting the operations of rank one updates and additions and deletions of rows and columns. We present an algorithm that updates the rank in Õ(mn) field operations. We show that these algorithms can be used to obtain faster algorithms for various problems in numerical linear algebra, combinatorial optimization and dynamic data structure.
Creating Intelligent Linking for Information Threading in Knowledge Networks
Venue: arXiv cs.AI 2012
Year: 2012

Informledge System (ILS) is a knowledge network with autonomous nodes and intelligent links that integrate and structure the pieces of knowledge. In this paper, we aim to put forward the link dynamics involved in intelligent processing of information in ILS. There has been advancement in knowledge management field which involve managing information in databases from a single domain. ILS works with information from multiple domains stored in distributed way in the autonomous nodes termed as Knowledge Network Node (KNN). Along with the concept under consideration, KNNs store the processed information linking concepts and processors leading to the appropriate processing of information.
Critical Task Re-assignment under Hybrid Scheduling Approach in Multiprocessor Real-Time Systems
Venue: arXiv cs.OH 2012
Year: 2012

Embedded hard real time systems require substantial amount of emergency processing power for the management of large scale systems like a nuclear power plant under the threat of an earth quake or a future transport systems under a peril. In order to meet a fully coordinated supervisory control of multiple domains of a large scale system, it requires the scenario of engaging multiprocessor real time design. There are various types of scheduling schemes existing for meeting the critical task assignment in multiple processor environments and it requires the tracking of faulty conditions of the subsystem to avoid system underperformance from failure patterns. Hybrid scheduling usually engages a combined scheduling philosophy comprising of a static scheduling of a set of tasks and a highly pre-emptive scheduling for another set of tasks in different situations of process control. There are instances where highly critical tasks need to be introduced at a least expected catastrophe and it cannot be ensured to meet all deadline in selected processors because of the arrival pattern of such tasks and they bear low tolerance of time to meet the required target. In such circumstances an effective switching of processors for this set of task is feasible and we describe a method to achieve this effectively.
Face Expression Recognition and Analysis: The State of the Art
Venue: arXiv cs.CV 2012
Year: 2012

The automatic recognition of facial expressions has been an active research topic since the early nineties. There have been several advances in the past few years in terms of face detection and tracking, feature extraction mechanisms and the techniques used for expression classification. This paper surveys some of the published work since 2001 till date. The paper presents a time-line view of the advances made in this field, the applications of automatic face expression recognizers, the characteristics of an ideal system, the databases that have been used and the advances made in terms of their standardization and a detailed summary of the state of the art. The paper also discusses facial parameterization using FACS Action Units (AUs) and MPEG-4 Facial Animation Parameters (FAPs) and the recent advances in face detection, tracking and feature extraction methods. Notes have also been presented on emotions, expressions and facial features, discussion on the six prototypic expressions and the recent studies on expression classifiers. The paper ends with a note on the challenges and the future work. This paper has been written in a tutorial style with the intention of helping students and researchers who are new to this field.
Adaptive Gaussian Mixture Filter Based on Statistical Linearization
Venue: arXiv cs.SY 2012
Year: 2012

Gaussian mixtures are a common density representation in nonlinear, non-Gaussian Bayesian state estimation. Selecting an appropriate number of Gaussian components, however, is difficult as one has to trade of computational complexity against estimation accuracy. In this paper, an adaptive Gaussian mixture filter based on statistical linearization is proposed. Depending on the nonlinearity of the considered estimation problem, this filter dynamically increases the number of components via splitting. For this purpose, a measure is introduced that allows for quantifying the locally induced linearization error at each Gaussian mixture component. The deviation between the nonlinear and the linearized state space model is evaluated for determining the splitting direction. The proposed approach is not restricted to a specific statistical linearization method. Simulations show the superior estimation performance compared to related approaches and common filtering algorithms.
Complexity Information Flow in a Multi-threaded Imperative Language
Venue: arXiv cs.CC 2012
Year: 2012

We propose a type system to analyze the time consumed by multi-threaded imperative programs with a shared global memory, which delineates a class of safe multi-threaded programs. We demonstrate that a safe multi-threaded program runs in polynomial time if (i) it is strongly terminating wrt a non-deterministic scheduling policy or (ii) it terminates wrt a deterministic and quiet scheduling policy. As a consequence, we also characterize the set of polynomial time functions. The type system presented is based on the fundamental notion of data tiering, which is central in implicit computational complexity. It regulates the information flow in a computation. This aspect is interesting in that the type system bears a resemblance to typed based information flow analysis and notions of non-interference. As far as we know, this is the first characterization by a type system of polynomial time multi-threaded programs.