OpenRaiser/Intern-Atlas huggingface dataset:
Designing a Routing Protocol for Ubiquitous Networks Using ECA Scheme
Venue: arXiv cs.NI 2015
Year: 2015

We have designed a novel Event-Condition-Action(ECA) scheme based Ad hoc On-demand Distance Vector(ECA-AODV) routing protocol for a Ubiquitous Network(UbiNet). ECA-AODV is designed to make routing decision dynamically and quicker response to dynamic network conditions as and when event occur. ECA scheme essentially consists of three modules to make runtime routing decision quicker. First, event module receive event that occur in a UbiNet and split up event into event type and event attributes. Second, condition module obtain event details from event module split up each condition into condition attributes that matches event and fire the rule as soon as condition hold. Third, action module make runtime decisions based on event obtained and condition applied. We have simulated and tested the designed ECA scheme by considering ubiquitous museum environment as a case study with nodes range from 10 to 100. The simulation results show the time efficient with minimal operations
Prime Factorization of the Kirchhoff Polynomial: Compact Enumeration of Arborescences
Venue: arXiv cs.DS 2015
Year: 2015

We study the problem of enumerating all rooted directed spanning trees (arborescences) of a directed graph (digraph) $G=(V,E)$ of $n$ vertices. An arborescence $A$ consisting of edges $e_1,\ldots,e_{n-1}$ can be represented as a monomial $e_1\cdot e_2 \cdots e_{n-1}$ in variables $e \in E$. All arborescences $\mathsf{arb}(G)$ of a digraph then define the Kirchhoff polynomial $\sum_{A \in \mathsf{arb}(G)} \prod_{e\in A} e$. We show how to compute a compact representation of the Kirchhoff polynomial -- its prime factorization, and how it relates to combinatorial properties of digraphs such as strong connectivity and vertex domination. In particular, we provide digraph decomposition rules that correspond to factorization steps of the polynomial, and also give necessary and sufficient primality conditions of the resulting factors expressed by connectivity properties of the corresponding decomposed components. Thereby, we obtain a linear time algorithm for decomposing a digraph into components corresponding to factors of the initial polynomial, and a guarantee that no finer factorization is possible. The decomposition serves as a starting point for a recursive deletion-contraction algorithm, and also as a preprocessing phase for iterative enumeration algorithms. Both approaches produce a compressed output and retain some structural properties in the resulting polynomial. This proves advantageous in practical applications such as calculating steady states on digraphs governed by Laplacian dynamics, or computing the greatest common divisor of Kirchhoff polynomials. Finally, we initiate the study of a class of digraphs which allow for a practical enumeration of arborescences. Using our decomposition rules we observe that various digraphs from real-world applications fall into this class or are structurally similar to it.
Randomization beats Second Price as a Prior-Independent Auction
Venue: arXiv cs.GT 2015
Year: 2015

Designing revenue optimal auctions for selling an item to $n$ symmetric bidders is a fundamental problem in mechanism design. Myerson (1981) shows that the second price auction with an appropriate reserve price is optimal when bidders' values are drawn i.i.d. from a known regular distribution. A cornerstone in the prior-independent revenue maximization literature is a result by Bulow and Klemperer (1996) showing that the second price auction without a reserve achieves $(n-1)/n$ of the optimal revenue in the worst case. We construct a randomized mechanism that strictly outperforms the second price auction in this setting. Our mechanism inflates the second highest bid with a probability that varies with $n$. For two bidders we improve the performance guarantee from $0.5$ to $0.512$ of the optimal revenue. We also resolve a question in the design of revenue optimal mechanisms that have access to a single sample from an unknown distribution. We show that a randomized mechanism strictly outperforms all deterministic mechanisms in terms of worst case guarantee.
An Open Challenge Problem Repository for Systems Supporting Binders
Venue: arXiv cs.LO 2015
Year: 2015

A variety of logical frameworks support the use of higher-order abstract syntax in representing formal systems; however, each system has its own set of benchmarks. Even worse, general proof assistants that provide special libraries for dealing with binders offer a very limited evaluation of such libraries, and the examples given often do not exercise and stress-test key aspects that arise in the presence of binders. In this paper we design an open repository ORBI (Open challenge problem Repository for systems supporting reasoning with BInders). We believe the field of reasoning about languages with binders has matured, and a common set of benchmarks provides an important basis for evaluation and qualitative comparison of different systems and libraries that support binders, and it will help to advance the field.
Proof-relevant pi-calculus
Venue: arXiv cs.LO 2015
Year: 2015

Formalising the pi-calculus is an illuminating test of the expressiveness of logical frameworks and mechanised metatheory systems, because of the presence of name binding, labelled transitions with name extrusion, bisimulation, and structural congruence. Formalisations have been undertaken in a variety of systems, primarily focusing on well-studied (and challenging) properties such as the theory of process bisimulation. We present a formalisation in Agda that instead explores the theory of concurrent transitions, residuation, and causal equivalence of traces, which has not previously been formalised for the pi-calculus. Our formalisation employs de Bruijn indices and dependently-typed syntax, and aligns the "proved transitions" proposed by Boudol and Castellani in the context of CCS with the proof terms naturally present in Agda's representation of the labelled transition relation. Our main contributions are proofs of the "diamond lemma" for residuation of concurrent transitions and a formal definition of equivalence of traces up to permutation of transitions.
Sequent Calculus and Equational Programming
Venue: arXiv cs.LO 2015
Year: 2015

Proof assistants and programming languages based on type theories usually come in two flavours: one is based on the standard natural deduction presentation of type theory and involves eliminators, while the other provides a syntax in equational style. We show here that the equational approach corresponds to the use of a focused presentation of a type theory expressed as a sequent calculus. A typed functional language is presented, based on a sequent calculus, that we relate to the syntax and internal language of Agda. In particular, we discuss the use of patterns and case splittings, as well as rules implementing inductive reasoning and dependent products and sums.
Communication: Words and Conceptual Systems
Venue: arXiv cs.AI 2015
Year: 2015

Words (phrases or symbols) play a key role in human life. Word (phrase or symbol) representation is the fundamental problem for knowledge representation and understanding. A word (phrase or symbol) usually represents a name of a category. However, it is always a challenge that how to represent a category can make it easily understood. In this paper, a new representation for a category is discussed, which can be considered a generalization of classic set. In order to reduce representation complexity, the economy principle of category representation is proposed. The proposed category representation provides a powerful tool for analyzing conceptual systems, relations between words, communication, knowledge, situations. More specifically, the conceptual system, word relations and communication are mathematically defined and classified such as ideal conceptual system, perfect communication and so on; relation between words and sentences is also studied, which shows that knowledge are words. Furthermore, how conceptual systems and words depend on situations is presented, and how truth is defined is also discussed.
STC Anti-spoofing Systems for the ASVspoof 2015 Challenge
Venue: arXiv cs.SD 2015
Year: 2015

This paper presents the Speech Technology Center (STC) systems submitted to Automatic Speaker Verification Spoofing and Countermeasures (ASVspoof) Challenge 2015. In this work we investigate different acoustic feature spaces to determine reliable and robust countermeasures against spoofing attacks. In addition to the commonly used front-end MFCC features we explored features derived from phase spectrum and features based on applying the multiresolution wavelet transform. Similar to state-of-the-art ASV systems, we used the standard TV-JFA approach for probability modelling in spoofing detection systems. Experiments performed on the development and evaluation datasets of the Challenge demonstrate that the use of phase-related and wavelet-based features provides a substantial input into the efficiency of the resulting STC systems. In our research we also focused on the comparison of the linear (SVM) and nonlinear (DBN) classifiers.
Improving Reachability and Navigability in Recommender Systems
Venue: arXiv cs.IR 2015
Year: 2015

In this paper, we investigate recommender systems from a network perspective and investigate recommendation networks, where nodes are items (e.g., movies) and edges are constructed from top-N recommendations (e.g., related movies). In particular, we focus on evaluating the reachability and navigability of recommendation networks and investigate the following questions: (i) How well do recommendation networks support navigation and exploratory search? (ii) What is the influence of parameters, in particular different recommendation algorithms and the number of recommendations shown, on reachability and navigability? and (iii) How can reachability and navigability be improved in these networks? We tackle these questions by first evaluating the reachability of recommendation networks by investigating their structural properties. Second, we evaluate navigability by simulating three different models of information seeking scenarios. We find that with standard algorithms, recommender systems are not well suited to navigation and exploration and propose methods to modify recommendations to improve this. Our work extends from one-click-based evaluations of recommender systems towards multi-click analysis (i.e., sequences of dependent clicks) and presents a general, comprehensive approach to evaluating navigability of arbitrary recommendation networks.
A Declarative Framework for Specifying and Enforcing Purpose-aware Policies
Venue: arXiv cs.CR 2015
Year: 2015

Purpose is crucial for privacy protection as it makes users confident that their personal data are processed as intended. Available proposals for the specification and enforcement of purpose-aware policies are unsatisfactory for their ambiguous semantics of purposes and/or lack of support to the run-time enforcement of policies. In this paper, we propose a declarative framework based on a first-order temporal logic that allows us to give a precise semantics to purpose-aware policies and to reuse algorithms for the design of a run-time monitor enforcing purpose-aware policies. We also show the complexity of the generation and use of the monitor which, to the best of our knowledge, is the first such a result in literature on purpose-aware policies.
Session-based Communication for Vital Machine-to-Machine Applications
Venue: arXiv cs.NI 2015
Year: 2015

Although the machine to machine (M2M) communication has been emerging in recent years, many vendors' specific proprietary solutions are not suitable for vital M2M applications. While the main focus of those solutions is management and provisioning of machines, real-time monitoring and communication control are also required to handle a variety of access technologies, like WiFi and LTE, and unleash machine deployment. In this paper, we present a new architecture addressing these issues by leveraging the IP Multimedia Subsystem (IMS) deployed in operator's networks for RCS and VoLTE.
Deep Learning for Single-View Instance Recognition
Venue: arXiv cs.CV 2015
Year: 2015

Deep learning methods have typically been trained on large datasets in which many training examples are available. However, many real-world product datasets have only a small number of images available for each product. We explore the use of deep learning methods for recognizing object instances when we have only a single training example per class. We show that feedforward neural networks outperform state-of-the-art methods for recognizing objects from novel viewpoints even when trained from just a single image per object. To further improve our performance on this task, we propose to take advantage of a supplementary dataset in which we observe a separate set of objects from multiple viewpoints. We introduce a new approach for training deep learning methods for instance recognition with limited training data, in which we use an auxiliary multi-view dataset to train our network to be robust to viewpoint changes. We find that this approach leads to a more robust classifier for recognizing objects from novel viewpoints, outperforming previous state-of-the-art approaches including keypoint-matching, template-based techniques, and sparse coding.
When VLAD met Hilbert
Venue: arXiv cs.CV 2015
Year: 2015

Vectors of Locally Aggregated Descriptors (VLAD) have emerged as powerful image/video representations that compete with or even outperform state-of-the-art approaches on many challenging visual recognition tasks. In this paper, we address two fundamental limitations of VLAD: its requirement for the local descriptors to have vector form and its restriction to linear classifiers due to its high-dimensionality. To this end, we introduce a kernelized version of VLAD. This not only lets us inherently exploit more sophisticated classification schemes, but also enables us to efficiently aggregate non-vector descriptors (e.g., tensors) in the VLAD framework. Furthermore, we propose three approximate formulations that allow us to accelerate the coding process while still benefiting from the properties of kernel VLAD. Our experiments demonstrate the effectiveness of our approach at handling manifold-valued data, such as covariance descriptors, on several classification tasks. Our results also evidence the benefits of our nonlinear VLAD descriptors against the linear ones in Euclidean space using several standard benchmark datasets.
Almost Optimal Energy-Efficient Cognitive Communications in Unknown Environments
Venue: arXiv cs.NI 2015
Year: 2015

Cognitive (Radio) (CR) Communications (CC) are mainly deployed within the environments of primary (user) communications, where the channel states and accessibility are usually stochastically distributed (benign or IID). However, many practical CC are also exposed to disturbing events (contaminated) and vulnerable jamming attacks (adversarial or non-IID). Thus, the channel state distribution of spectrum could be stochastic, contaminated or adversarial at different temporal and spatial locations. Without any a priori, facilitating optimal CC is a very challenging issue. In this paper, we propose an online learning algorithm that performs the joint channel sensing, probing and adaptive channel access for multi-channel CC in general unknown environments. We take energy-efficient CC (EECC) into our special attention, which is highly desirable for green wireless communications and demanding to combat with potential jamming attack who could greatly mar the energy and spectrum efficiency of CC. The EECC is formulated as a constrained regret minimization problem with power budget constraints. By tuning a novel exploration parameter, our algorithms could adaptively find the optimal channel access strategies and achieve the almost optimal learning performance of EECC in different scenarios provided with the vanishing long-term power budget violations. We also consider the important scenario that cooperative learning and information sharing among multiple CR users to see further performance improvements. The proposed algorithms are resilient to both oblivious and adaptive jamming attacks with different intelligence and attacking strength. Extensive numerical results are conducted to validate our theory.
Ethical, Legal and Social aspects of Information and Communication Technology
Venue: arXiv cs.CY 2015
Year: 2015

In this era of computers and communication technology where computers and internet have made their ways to every sphere of life from offices to residences, reservation counters to banks to post offices, small retail shops to big organizations, health care units to entertainment industries etc., there emerged numerous questions regarding the ethical and legal uses of Information and Communication Technology (ICT). Like any other technological inventions ICT too has created both positive and negative impacts on the society. This paper aims at exploring some of these issues in brief.
Cost optimization of data flows based on task re-ordering
Venue: arXiv cs.DB 2015
Year: 2015

Analyzing big data in a highly dynamic environment becomes more and more critical because of the increasingly need for end-to-end processing of this data. Modern data flows are quite complex and there are not efficient, cost-based, fully-automated, scalable optimization solutions that can facilitate flow designers. The state-of-the-art proposals fail to provide near optimal solutions even for simple data flows. To tackle this problem, we introduce a set of approximate algorithms for defining the execution order of the constituent tasks, in order to minimize the total execution cost of a data flow. We also present the advantages of the parallel execution of data flows. We validated our proposals in both a real tool and synthetic flows and the results show that we can achieve significant speed-ups, moving much closer to optimal solutions.
When a Movement Becomes a Party: The 2015 Barcelona City Council Election
Venue: arXiv cs.SI 2015
Year: 2015

Barcelona en Comú, an emerging grassroots movement-party, won the 2015 Barcelona City Council election. This candidacy was devised by activists involved in the 15M movement in order to turn citizen outrage into political change. On the one hand, the 15M movement is based on a decentralized structure. On the other hand, political science literature postulates that parties historically develop oligarchical leadership structures. This tension motivates us to examine whether Barcelona en Comú preserved a decentralizated structure or adopted a conventional centralized organization. In this article we analyse the Twitter networks of the parties that ran for this election by measuring their hierarchical structure, information efficiency and social resilience. Our results show that in Barcelona en Comú two well-defined groups co-exist: a cluster dominated by the leader and the collective accounts, and another cluster formed by the movement activists. While the former group is highly centralized like the other major parties, the latter one stands out for its decentralized, cohesive and resilient structure.
Asymptotic Mutual Information for the Two-Groups Stochastic Block Model
Venue: arXiv cs.IT 2015
Year: 2015

We develop an information-theoretic view of the stochastic block model, a popular statistical model for the large-scale structure of complex networks. A graph $G$ from such a model is generated by first assigning vertex labels at random from a finite alphabet, and then connecting vertices with edge probabilities depending on the labels of the endpoints. In the case of the symmetric two-group model, we establish an explicit `single-letter' characterization of the per-vertex mutual information between the vertex labels and the graph. The explicit expression of the mutual information is intimately related to estimation-theoretic quantities, and --in particular-- reveals a phase transition at the critical point for community detection. Below the critical point the per-vertex mutual information is asymptotically the same as if edges were independent. Correspondingly, no algorithm can estimate the partition better than random guessing. Conversely, above the threshold, the per-vertex mutual information is strictly smaller than the independent-edges upper bound. In this regime there exists a procedure that estimates the vertex labels better than random guessing.
Systematic Verification of the Modal Logic Cube in Isabelle/HOL
Venue: arXiv cs.LO 2015
Year: 2015

We present an automated verification of the well-known modal logic cube in Isabelle/HOL, in which we prove the inclusion relations between the cube's logics using automated reasoning tools. Prior work addresses this problem but without restriction to the modal logic cube, and using encodings in first-order logic in combination with first-order automated theorem provers. In contrast, our solution is more elegant, transparent and effective. It employs an embedding of quantified modal logic in classical higher-order logic. Automated reasoning tools, such as Sledgehammer with LEO-II, Satallax and CVC4, Metis and Nitpick, are employed to achieve full automation. Though successful, the experiments also motivate some technical improvements in the Isabelle/HOL tool.
Analyzing Whole-Body Pose Transitions in Multi-Contact Motions
Venue: arXiv cs.RO 2015
Year: 2015

When executing whole-body motions, humans are able to use a large variety of support poses which not only utilize the feet, but also hands, knees and elbows to enhance stability. While there are many works analyzing the transitions involved in walking, very few works analyze human motion where more complex supports occur. In this work, we analyze complex support pose transitions in human motion involving locomotion and manipulation tasks (loco-manipulation). We have applied a method for the detection of human support contacts from motion capture data to a large-scale dataset of loco-manipulation motions involving multi-contact supports, providing a semantic representation of them. Our results provide a statistical analysis of the used support poses, their transitions and the time spent in each of them. In addition, our data partially validates our taxonomy of whole-body support poses presented in our previous work. We believe that this work extends our understanding of human motion for humanoids, with a long-term objective of developing methods for autonomous multi-contact motion planning.
Effective Capacity in Multiple Access Channels with Arbitrary Inputs
Venue: arXiv cs.IT 2015
Year: 2015

In this paper, we consider a two-user multiple access fading channel under quality-of-service (QoS) constraints. We initially formulate the transmission rates for both transmitters, where the transmitters have arbitrarily distributed input signals. We assume that the receiver performs successive decoding with a certain order. Then, we establish the effective capacity region that provides the maximum allowable sustainable arrival rate region at the transmitters' buffers under QoS guarantees. Assuming limited transmission power budgets at the transmitters, we attain the power allocation policies that maximize the effective capacity region. As for the decoding order at the receiver, we characterize the optimal decoding order regions in the plane of channel fading parameters for given power allocation policies. In order to accomplish the aforementioned objectives, we make use of the relationship between the minimum mean square error and the first derivative of the mutual information with respect to the power allocation policies. Through numerical results, we display the impact of input signal distributions on the effective capacity region performance of this two-user multiple access fading channel.