OpenRaiser/Intern-Atlas huggingface dataset:
A provably efficient online collaborative caching algorithm for multicell-coordinated systems
Venue: arXiv cs.NI 2015
Year: 2015

Caching at the base stations brings the contents closer to the users, reduces the traffic through the backhaul links, and reduces the delay experienced by the cellular users. The cellular network operator may charge the content providers for caching their contents. Moreover, content providers may lose their users if the users are not getting their desired quality of service, such as maximum tolerable delay in Video on Demand services. In this paper, we study the collaborative caching problem for a multicell-coordinated system from the point of view of minimizing the total cost paid by the content providers. We formulate the problem as an Integer Linear Program and prove its NP-completeness. We also provide an online caching algorithm that does not require any knowledge about the contents popularities. We prove that the online algorithm achieves a competitive ratio of $\mathcal{O}(\log(n))$, and we show that the best competitive ratio that any online algorithm can achieve is $Ω(\frac{\log(n)}{\log\log(n)})$. Therefore, our proposed caching algorithm is provably efficient. Through simulations, we show that our online algorithm performs very close to the optimal offline collaborative scheme, and can outperform it when contents popularities are not properly estimated.
Coarse-to-Fine Sequential Monte Carlo for Probabilistic Programs
Venue: arXiv cs.AI 2015
Year: 2015

Many practical techniques for probabilistic inference require a sequence of distributions that interpolate between a tractable distribution and an intractable distribution of interest. Usually, the sequences used are simple, e.g., based on geometric averages between distributions. When models are expressed as probabilistic programs, the models themselves are highly structured objects that can be used to derive annealing sequences that are more sensitive to domain structure. We propose an algorithm for transforming probabilistic programs to coarse-to-fine programs which have the same marginal distribution as the original programs, but generate the data at increasing levels of detail, from coarse to fine. We apply this algorithm to an Ising model, its depth-from-disparity variation, and a factorial hidden Markov model. We show preliminary evidence that the use of coarse-to-fine models can make existing generic inference algorithms more efficient.
Dictionary Learning and Sparse Coding for Third-order Super-symmetric Tensors
Venue: arXiv cs.CV 2015
Year: 2015

Super-symmetric tensors - a higher-order extension of scatter matrices - are becoming increasingly popular in machine learning and computer vision for modelling data statistics, co-occurrences, or even as visual descriptors. However, the size of these tensors are exponential in the data dimensionality, which is a significant concern. In this paper, we study third-order super-symmetric tensor descriptors in the context of dictionary learning and sparse coding. Our goal is to approximate these tensors as sparse conic combinations of atoms from a learned dictionary, where each atom is a symmetric positive semi-definite matrix. Apart from the significant benefits to tensor compression that this framework provides, our experiments demonstrate that the sparse coefficients produced by the scheme lead to better aggregation of high-dimensional data, and showcases superior performance on two common computer vision tasks compared to the state-of-the-art.
On the Multidimensional Stable Marriage Problem
Venue: arXiv cs.GT 2015
Year: 2015

We provide a problem definition of the stable marriage problem for a general number of parties $p$ under a natural preference scheme in which each person has simple lists for the other parties. We extend the notion of stability in a natural way and present so called elemental and compound algorithms to generate matchings for a problem instance. We demonstrate the stability of matchings generated by both algorithms, as well as show that the former runs in $O(pn^2)$ time.
Social Learning with Coordination Motives
Venue: arXiv cs.SI 2015
Year: 2015

The theoretical study of social learning typically assumes that each agent's action affects only her own payoff. In this paper, I present a model in which agents' actions directly affect the payoffs of other agents. On a discrete time line, there is a community containing a random number of agents in each period. Before each agent needs to take an action, the community receives a private signal about the underlying state of the world and may observe some past actions in previous communities. An agent's payoff is higher if her action matches the state or if more agents take the same action as hers. I analyze two observation structures: exogenous observation and costly strategic observation. In both cases, coordination motives enhance social learning in the sense that agents take the correct action with significantly higher probability when the community size is greater than a threshold. In particular, this probability reaches one (asymptotic learning) with unbounded private beliefs and can be arbitrarily close to one with bounded private beliefs. I then discuss the issue of multiple equilibria and use risk dominance as a criterion for equilibrium selection. I find that in the selected equilibria, the community size has no effect on learning under exogenous observation, facilitates learning under endogenous observation and unbounded private beliefs, and either helps or hinders learning under endogenous observation and bounded private beliefs.
Reasoning about modular datatypes with Mendler induction
Venue: arXiv cs.LO 2015
Year: 2015

In functional programming, datatypes a la carte provide a convenient modular representation of recursive datatypes, based on their initial algebra semantics. Unfortunately it is highly challenging to implement this technique in proof assistants that are based on type theory, like Coq. The reason is that it involves type definitions, such as those of type-level fixpoint operators, that are not strictly positive. The known work-around of impredicative encodings is problematic, insofar as it impedes conventional inductive reasoning. Weak induction principles can be used instead, but they considerably complicate proofs. This paper proposes a novel and simpler technique to reason inductively about impredicative encodings, based on Mendler-style induction. This technique involves dispensing with dependent induction, ensuring that datatypes can be lifted to predicates and relying on relational formulations. A case study on proving subject reduction for structural operational semantics illustrates that the approach enables modular proofs, and that these proofs are essentially similar to conventional ones.
The World of Combinatorial Fuzzy Problems and the Efficiency of Fuzzy Approximation Algorithms
Venue: arXiv cs.AI 2015
Year: 2015

We re-examine a practical aspect of combinatorial fuzzy problems of various types, including search, counting, optimization, and decision problems. We are focused only on those fuzzy problems that take series of fuzzy input objects and produce fuzzy values. To solve such problems efficiently, we design fast fuzzy algorithms, which are modeled by polynomial-time deterministic fuzzy Turing machines equipped with read-only auxiliary tapes and write-only output tapes and also modeled by polynomial-size fuzzy circuits composed of fuzzy gates. We also introduce fuzzy proof verification systems to model the fuzzification of nondeterminism. Those models help us identify four complexity classes: Fuzzy-FPA of fuzzy functions, Fuzzy-PA and Fuzzy-NPA of fuzzy decision problems, and Fuzzy-NPAO of fuzzy optimization problems. Based on a relative approximation scheme targeting fuzzy membership degree, we formulate two notions of "reducibility" in order to compare the computational complexity of two fuzzy problems. These reducibility notions make it possible to locate the most difficult fuzzy problems in Fuzzy-NPA and in Fuzzy-NPAO.
Realistic, Extensible DNS and mDNS Models for INET/OMNeT++
Venue: arXiv cs.NI 2015
Year: 2015

The domain name system (DNS) is one of the core services in today's network structures. In local and ad-hoc networks DNS is often enhanced or replaced by mDNS. As of yet, no simulation models for DNS and mDNS have been developed for INET/OMNeT++. We introduce DNS and mDNS simulation models for OMNeT++, which allow researchers to easily prototype and evaluate extensions for these protocols. In addition, we present models for our own experimental extensions, namely Stateless DNS and Privacy-Enhanced mDNS, that are based on the aforementioned models. Using our models we were able to further improve the efficiency of our protocol extensions.
The paradox of controlling complex networks: control inputs versus energy requirement
Venue: arXiv cs.SY 2015
Year: 2015

In this paper, we investigate the linear controllability framework for complex networks from a physical point of view. There are three main results. (1) If one applies control signals as determined from the structural controllability theory, there is a high probability that the control energy will diverge. Especially, if a network is deemed controllable using a single driving signal, then most likely the energy will diverge. (2) The energy required for control exhibits a power-law scaling behavior. (3) Applying additional control signals at proper nodes in the network can reduce and optimize the energy cost. We identify the fundamental structures embedded in the network, the longest control chains, which determine the control energy and give rise to the power-scaling behavior. (To our knowledge, this was not reported in any previous work on control of complex networks.) In addition, the issue of control precision is addressed. These results are supported by extensive simulations from model and real networks, physical reasoning, and mathematical analyses. Notes on the submission history of this work: This work started in late 2012. The phenomena of power-law energy scaling and energy divergence with a single controller were discovered in 2013. Strategies to reduce and optimize control energy was articulated and tested in 2013. The senior co-author (YCL) gave talks about these results at several conferences, including the NETSCI 2014 Satellite entitled "Controlling Complex Networks" on June 2, 2014. The paper was submitted to PNAS in September 2014 and was turned down. It was revised and submitted to PRX in early 2015 and was rejected. After that it was revised and submitted to Nature Communications in May 2015 and again was turned down.
A new Initial Centroid finding Method based on Dissimilarity Tree for K-means Algorithm
Venue: arXiv cs.LG 2015
Year: 2015

Cluster analysis is one of the primary data analysis technique in data mining and K-means is one of the commonly used partitioning clustering algorithm. In K-means algorithm, resulting set of clusters depend on the choice of initial centroids. If we can find initial centroids which are coherent with the arrangement of data, the better set of clusters can be obtained. This paper proposes a method based on the Dissimilarity Tree to find, the better initial centroid as well as every bit more accurate cluster with less computational time. Theory analysis and experimental results indicate that the proposed method can effectively improve the accuracy of clusters and reduce the computational complexity of the K-means algorithm.
Binary Continuous Phase Modulations Robust to a Modulation Index Mismatch
Venue: arXiv cs.IT 2015
Year: 2015

We consider binary continuous phase modulation (CPM) signals used in some recent low-cost and low-power consumption telecommunications standard. When these signals are generated through a low-cost transmitter, the real modulation index can end up being quite different from the nominal value employed at the receiver and a significant performance degradation is observed, unless proper techniques for the estimation and compensation are employed. For this reason, we design new binary schemes with a much higher robustness. They are based on the concatenation of a suitable precoder with binary input and a ternary CPM format. The result is a family of CPM formats whose phase state is constrained to follow a specific evolution. Two of these precoders are considered. We will discuss many aspects related to these schemes, such as the power spectral density, the spectral efficiency, simplified detection, the minimum distance, and the uncoded performance. The adopted precoders do not change the recursive nature of CPM schemes. So these schemes are still suited for serial concatenation, through a pseudo-random interleaver, with an outer channel encoder.
Measuring an Artificial Intelligence System's Performance on a Verbal IQ Test For Young Children
Venue: arXiv cs.AI 2015
Year: 2015

We administered the Verbal IQ (VIQ) part of the Wechsler Preschool and Primary Scale of Intelligence (WPPSI-III) to the ConceptNet 4 AI system. The test questions (e.g., "Why do we shake hands?") were translated into ConceptNet 4 inputs using a combination of the simple natural language processing tools that come with ConceptNet together with short Python programs that we wrote. The question answering used a version of ConceptNet based on spectral methods. The ConceptNet system scored a WPPSI-III VIQ that is average for a four-year-old child, but below average for 5 to 7 year-olds. Large variations among subtests indicate potential areas of improvement. In particular, results were strongest for the Vocabulary and Similarities subtests, intermediate for the Information subtest, and lowest for the Comprehension and Word Reasoning subtests. Comprehension is the subtest most strongly associated with common sense. The large variations among subtests and ordinary common sense strongly suggest that the WPPSI-III VIQ results do not show that "ConceptNet has the verbal abilities a four-year-old." Rather, children's IQ tests offer one objective metric for the evaluation and comparison of AI systems. Also, this work continues previous research on Psychometric AI.
Modal Characterisations of Behavioural Pseudometrics
Venue: arXiv cs.LO 2015
Year: 2015

For the model of probabilistic labelled transition systems that allow for the co-existence of nondeterminism and probabilities, we present two notions of bisimulation metrics: one is state-based and the other is distribution-based. We provide a sound and complete modal characterisation for each of them, using real-valued modal logics based on the Hennessy-Milner logic. The logic for characterising the state-based metric is much simpler than an earlier logic by Desharnais et al. as it uses only two non-expansive operators rather than the general class of non-expansive operators.
Observer-based correct-by-design controller synthesis
Venue: arXiv cs.SY 2015
Year: 2015

Current state-of-the-art correct-by-design controllers are designed for full-state measurable systems. This work first extends the applicability of correct-by-design controllers to partially observable LTI systems. Leveraging 2nd order bounds we give a design method that has a quantifiable robustness to probabilistic disturbances on state transitions and on output measurements. In a case study from smart buildings we evaluate the new output-based correct-by-design controller on a physical system with limited sensor information.
Fast community structure local uncovering by independent vertex-centred process
Venue: arXiv cs.SI 2015
Year: 2015

This paper addresses the task of community detection and proposes a local approach based on a distributed list building, where each vertex broadcasts basic information that only depends on its degree and that of its neighbours. A decentralised external process then unveils the community structure. The relevance of the proposed method is experimentally shown on both artificial and real data.
Premise Selection and External Provers for HOL4
Venue: arXiv cs.AI 2015
Year: 2015

Learning-assisted automated reasoning has recently gained popularity among the users of Isabelle/HOL, HOL Light, and Mizar. In this paper, we present an add-on to the HOL4 proof assistant and an adaptation of the HOLyHammer system that provides machine learning-based premise selection and automated reasoning also for HOL4. We efficiently record the HOL4 dependencies and extract features from the theorem statements, which form a basis for premise selection. HOLyHammer transforms the HOL4 statements in the various TPTP-ATP proof formats, which are then processed by the ATPs. We discuss the different evaluation settings: ATPs, accessible lemmas, and premise numbers. We measure the performance of HOLyHammer on the HOL4 standard library. The results are combined accordingly and compared with the HOL Light experiments, showing a comparably high quality of predictions. The system directly benefits HOL4 users by automatically finding proofs dependencies that can be reconstructed by Metis.
Skip This Paper - RINASim: Your Recursive InterNetwork Architecture Simulator
Venue: arXiv cs.NI 2015
Year: 2015

Recursive InterNetwork Architecture is a clean-slate approach to how to deal with the current issues of the Internet based on the traditional TCP/IP networking stack. Instead of using a fixed number of layers with dedicated functionality, RINA proposes a single generic layer with programmable functionality that may be recursively stacked. We introduce a brand new framework for modeling and simulation of RINA that is intended for OMNeT++.
Invited Abstract: A Simulation Package for Energy Consumption of Content Delivery Networks (CDNs)
Venue: arXiv cs.PF 2015
Year: 2015

Content Delivery Networks (CDNs) are becoming an integral part of the future generation Internet. Traditionally, these networks have been designed with the goals of traffic offload and the improvement of users' quality of experience (QoE), but the energy consumption is also becoming an indispensable design factor for CDNs to be a sustainable solution. To study and improve the CDN architectures using this new design metric, we are planning to develop a generic and flexible simulation package in OMNet++. This package is aimed to render a holistic view about the CDN energy consumption behaviour by incorporating the state-of-the-art energy consumption models proposed for the individual elements of CDNs (e.g. servers, routers, wired and wireless links, wireless devices, etc.) and for the various Internet contents (web pages, files, streaming video, etc.).
Mechatronics Architecture of Smartphone-Based Spacecraft ADCS using VSCMG Actuators
Venue: arXiv cs.SY 2015
Year: 2015

Hardware and software architecture of a novel spacecraft Attitude Determination and Control System (ADCS) based on smartphones using Variable Speed Control Moment Gyroscope (VSCMG) as actuator is proposed here. A spacecraft ground simulator testbed for Hardware-in-the-loop (HIL) attitude estimation and control with VSCMG is also described. The sensor breakouts with independent micro-controller units are used in the conventional ADCS units, which are replaced by a single integrated off-the-shelf smartphone. On-board sensing, data acquisition, data uplink/downlink, state estimation and real-time feedback control objectives can be performed using this novel spacecraft ADCS. The attitude control and attitude determination (estimation) schemes have appeared in prior publications, but are presented in brief here. Experimental results from running the attitude estimation (filtering) scheme with the "onboard" sensors of the smartphone in the HIL simulator are given. These results, obtained in the Spacecraft Guidance, Navigation and Control Laboratory at NMSU, demonstrate the excellent performance of this estimation scheme with the noisy raw data from the smartphone sensors.
Integrated Science, Technology, Engineering and Mathematics (STEM) Education through Active Experience of Designing Technical Toys in Vietnamese Schools
Venue: arXiv cs.CY 2015
Year: 2015

STEM has attracted great consideration. The purpose of research is: (1) study STEM education, (2) explore STEM education with the creative and experiential activity, (3) suggest applying STEM education by designing technical toys for the middle school student. This study used a qualitative approach to carry out teaching integration for STEM education. The study applied to teaching the technological field in Vietnamese middle schools. The design performed at the Faculty of Technology Education, Hanoi National University of Education, Vietnam in April 2015. This study used the integrated approach to design subjects for STEM education. Two procedures for integration undertook with analysis. A sample of producing technical toy was consistent with developing students competencies. Integrated approach to STEM education through designing technical toys is possible. Recently, there has been a booming interest in Integrated Science, Technology, Engineering and Mathematics (STEM) education, but the approaches to STEM still remains controversial in diverse educational contexts. This study addressed this issue by exploring STEM education with the use of creative and experiential activities in a Vietnamese educational context. It also proposed a practical model for integrating STEM into teaching technology in secondary schools by designing technical toys. The implementation of the practical model suggests the possibility in using the integrated approach to STEM education through designing technical toys for middle school students in Vietnam. By applying the subject knowledge domains to solve real world problems and settings, the students can experience the benefits of a concrete and active learning in a meaningful and practical context. The multidisciplinary and interdisciplinary integration approaches are consistent with the development of the students competencies.
Minimum parametric flow over time
Venue: arXiv cs.DM 2015
Year: 2015

The paper presents a dynamic solution method for dynamic minimum parametric networks flow. The solution method solves the problem for a special parametric dynamic network with linear lower bound functions of a single parameter. Instead directly work on the original network, the method implements a labelling algorithm in the parametric dynamic residual network and uses quickest paths from the source node to the sink node in the time-space network along which repeatedly decreases the dynamic flow for a sequence of parameter values, in their increasing order. In each iteration, the algorithm computes both the minimum flow for a certain subinterval of the parameter values, and the new breakpoint for the maximum parametric dynamic flow value function.
Adaptation and Disturbance Rejection for Output Synchronization of Incrementally Output-feedback Passive Systems
Venue: arXiv cs.SY 2015
Year: 2015

This note addresses the output synchronization problem of incrementally output-feedback passive nonlinear systems in the presence of exogenous disturbances. Two kinds of distributed controllers are proposed; one placed at the nodes and the other placed at the edges. Each of them is synthesized based on the adaptive control method to cope with the shortage of passivity, and on the internal model principle to deal with the disturbances. The proposed controllers synchronize the outputs of the nonlinear systems when the solution of the closed-loop system is bounded. Based on this, we present a class of systems for which boundedness of the solutions is guaranteed. The analysis used in this note is also applicable to a case where systems are coupled via links modeled by dynamical systems. Simulation results of a network of Van der Pol oscillators show the effectiveness of the proposed methods.