OpenRaiser/Intern-Atlas huggingface dataset:
Content Retrieval At the Edge: A Social-aware and Named Data Cooperative Framework
Venue: arXiv cs.NI 2016
Year: 2016

Recent years with the popularity of mobile devices have witnessed an explosive growth of mobile multimedia contents which dominate more than 50\% of mobile data traffic. This significant growth poses a severe challenge for future cellular networks. As a promising approach to overcome the challenge, we advocate Content Retrieval At the Edge, a content-centric cooperative service paradigm via device-to-device (D2D) communications to reduce cellular traffic volume in mobile networks. By leveraging the Named Data Networking (NDN) principle, we propose sNDN, a social-aware named data framework to achieve efficient cooperative content retrieval. Specifically, sNDN introduces Friendship Circle by grouping a user with her close friends of both high mobility similarity and high content similarity. We construct NDN routing tables conditioned on Friendship Circle encounter frequency to navigate a content request and a content reply packet between Friendship Circles, and leverage social properties in Friendship Circle to search for the final target as inner-Friendship Circle routing. The evaluation results demonstrate that sNDN can save cellular capacity greatly and outperform other content retrieval schemes significantly.
Optimal Storage Aware Caching Policies for Content-Centric Clouds
Venue: arXiv cs.NI 2016
Year: 2016

Caches in Content-Centric Networks (CCN) are increasingly adopting flash memory based storage. The current flash cache technology stores all files with the largest possible expiry date, i.e. the files are written in the memory so that they are retained for as long as possible. This, however, does not leverage the CCN data characteristics where content is typically short-lived and has a distinct popularity profile. Writing files in a cache using the longest retention time damages the memory device thus reducing its lifetime. However, writing using a small retention time can increase the content retrieval delay, since, at the time a file is requested, the file may already have been expired from the memory. This motivates us to consider a joint optimization wherein we obtain optimal policies for jointly minimizing the content retrieval delay (which is a network-centric objective) and the flash damage (which is a device-centric objective). Caching decisions now not only involve what to cache but also for how long to cache each file. We design provably optimal policies and numerically compare them against prior policies.
Answer-Type Modification without Tears: Prompt-Passing Style Translation for Typed Delimited-Control Operators
Venue: arXiv cs.PL 2016
Year: 2016

The salient feature of delimited-control operators is their ability to modify answer types during computation. The feature, answer-type modification (ATM for short), allows one to express various interesting programs such as typed printf compactly and nicely, while it makes it difficult to embed these operators in standard functional languages. In this paper, we present a typed translation of delimited-control operators shift and reset with ATM into a familiar language with multi-prompt shift and reset without ATM, which lets us use ATM in standard languages without modifying the type system. Our translation generalizes Kiselyov's direct-style implementation of typed printf, which uses two prompts to emulate the modification of answer types, and passes them during computation. We prove that our translation preserves typing. As the naive prompt-passing style translation generates and passes many prompts even for pure terms, we show an optimized translation that generate prompts only when needed, which is also type-preserving. Finally, we give an implementation in the tagless-final style which respects typing by construction.
Denotational Semantics of the Simplified Lambda-Mu Calculus and a New Deduction System of Classical Type Theory
Venue: arXiv cs.LO 2016
Year: 2016

Classical (or Boolean) type theory is the type theory that allows the type inference $σ\to \bot) \to \bot => σ$ (the type counterpart of double-negation elimination), where $σ$ is any type and $\bot$ is absurdity type. This paper first presents a denotational semantics for a simplified version of Parigot's lambda-mu calculus, a premier example of classical type theory. In this semantics the domain of each type is divided into infinitely many ranks and contains not only the usual members of the type at rank 0 but also their negative, conjunctive, and disjunctive shadows in the higher ranks, which form an infinitely nested Boolean structure. Absurdity type $\bot$ is identified as the type of truth values. The paper then presents a new deduction system of classical type theory, a sequent calculus called the classical type system (CTS), which involves the standard logical operators such as negation, conjunction, and disjunction and thus reflects the discussed semantic structure in a more straightforward fashion.
A note on strong normalization in classical natural deduction
Venue: arXiv cs.LO 2016
Year: 2016

In the context of natural deduction for propositional classical logic, with classicality given by the inference rule reductio ad absurdum, we investigate the De Morgan translation of disjunction in terms of negation and conjunction. Once the translation is extended to proofs, it obtains a reduction of provability to provability in the disjunction-free subsystem. It is natural to ask whether a reduction is also obtained for, say, strong normalization; that is, whether strong normalization for the disjunction-free system implies the same property for the full system, and whether such lifting of the property can be done along the De Morgan translation. Although natural, these questions are neglected by the literature. We spell out the map of reduction steps induced by the De Morgan translation of proofs. But we need to "optimize" such a map in order to show that a reduction sequence in the full system from a proof determines, in a length-preserving way, a reduction sequence in the disjunction-free system from the De Morgan translation of the proof. In this sense, the above questions have a positive answer.
Uniqueness Trees: A Possible Polynomial Approach to the Graph Isomorphism Problem
Venue: arXiv cs.DM 2016
Year: 2016

This paper presents the novel `uniqueness tree' algorithm, as one possible method for determining whether two finite, undirected graphs are isomorphic. We prove that the algorithm has polynomial time complexity in the worst case, and that it will always detect the presence of an isomorphism whenever one exists. We also propose that the algorithm will equivalently discern the lack of an isomorphism whenever one does not exist, and some initial justifications are given for this proposition, although it cannot yet be rigorously proven. Finally, we present experimental evidence for both the effectiveness and efficiency of the uniqueness tree method, using data gathered from a practical implementation of the algorithm. Some consequences and directions for further research are discussed.
Weakly True Concurrency and Its Logic
Venue: arXiv cs.LO 2016
Year: 2016

We firstly find the existence of silent event $τ$ in true concurrency (named weakly true concurrency) by defining weakly true concurrent behaviors and weakly true concurrent logics. Based on Paolo Baldan and Silvia Crafa's comprehensive work on (strongly) true concurrency, we find the correspondence between weakly true concurrent equivalences and weakly true concurrent logics.
The Schema Editor of OpenIoT for Semantic Sensor Networks
Venue: arXiv cs.AI 2016
Year: 2016

Ontologies provide conceptual abstractions over data, in domains such as the Internet of Things, in a way that sensor data can be harvested and interpreted by people and applications. The Semantic Sensor Network (SSN) ontology is the de-facto standard for semantic representation of sensor observations and metadata, and it is used at the core of the open source platform for the Internet of Things, OpenIoT. In this paper we present a Schema Editor that provides an intuitive web interface for defining new types of sensors, and concrete instances of them, using the SSN ontology as the core model. This editor is fully integrated with the OpenIoT platform for generating virtual sensor descriptions and automating their semantic annotation and registration process.
Reliability-Aware Overlay Architectures for FPGAs: Features and Design Challenges
Venue: arXiv cs.AR 2016
Year: 2016

The FPGA overlay architectures have been mainly proposed to improve design productivity, circuit portability and system debugging. In this paper, we address the use of overlay architectures for building fault tolerant SRAM-based FPGA systems and discuss the main features and design challenges of a reliability-aware overlay architecture.
User fluctuation in communities: a forum case
Venue: arXiv cs.SI 2016
Year: 2016

Understanding fluctuation of users help stakeholders to provide a better support to communities. Below we present an experiment where we detect communities, their evolution and based on the data characterize users that stay, leave or join a community. Using a resulted feature set and logistic regression we operate with models of users that are joining and users that are staying in a community. In the related work we emphasize a number of features we will include in our future experiments to enhance train accuracy. This work represents a first from a series of experiments devoted to user fluctuation in communities.
Neural Morphological Tagging from Characters for Morphologically Rich Languages
Venue: arXiv cs.CL 2016
Year: 2016

This paper investigates neural character-based morphological tagging for languages with complex morphology and large tag sets. We systematically explore a variety of neural architectures (DNN, CNN, CNNHighway, LSTM, BLSTM) to obtain character-based word vectors combined with bidirectional LSTMs to model across-word context in an end-to-end setting. We explore supplementary use of word-based vectors trained on large amounts of unlabeled data. Our experiments for morphological tagging suggest that for "simple" model configurations, the choice of the network architecture (CNN vs. CNNHighway vs. LSTM vs. BLSTM) or the augmentation with pre-trained word embeddings can be important and clearly impact the accuracy. Increasing the model capacity by adding depth, for example, and carefully optimizing the neural networks can lead to substantial improvements, and the differences in accuracy (but not training time) become much smaller or even negligible. Overall, our best morphological taggers for German and Czech outperform the best results reported in the literature by a large margin.
Adaptive Just-in-time Value Class Optimization for Lowering Memory Consumption and Improving Execution Time Performance
Venue: arXiv cs.PL 2016
Year: 2016

The performance of value classes is highly dependent on how they are represented in the virtual machine. Value class instances are immutable, have no identity, and can only refer to other value objects or primitive values and since they should be very lightweight and fast, it is important to optimize them carefully. In this paper we present a technique to detect and compress common patterns of value class usage to improve memory usage and performance. The technique identifies patterns of frequent value object references and introduces abbreviated forms for them. This allows to store multiple inter-referenced value objects in an inlined memory representation, reducing the overhead stemming from meta-data and object references. Applied to a small prototype and an implementation of the Racket language, we found improvements in memory usage and execution time for several micro-benchmarks.
Quantum Probability as an Application of Data Compression Principles
Venue: arXiv cs.IT 2016
Year: 2016

Realist, no-collapse interpretations of quantum mechanics, such as Everett's, face the probability problem: how to justify the norm-squared (Born) rule from the wavefunction alone. While any basis-independent measure can only be norm-squared (due to the Gleason-Busch Theorem) this fact conflicts with various popular, non-wavefunction-based phenomenological measures - such as observer, outcome or world counting - that are frequently demanded of Everettians. These alternatives conflict, however, with the wavefunction realism upon which Everett's approach rests, which seems to call for an objective, basis-independent measure based only on wavefunction amplitudes. The ability of quantum probabilities to destructively interfere with each other, however, makes it difficult to see how probabilities can be derived solely from amplitudes in an intuitively appealing way. I argue that the use of algorithmic probability can solve this problem, since the objective, single-case probability measure that wavefunction realism demands is exactly what algorithmic information theory was designed to provide. The result is an intuitive account of complex-valued amplitudes, as coefficients in an optimal lossy data compression, such that changes in algorithmic information content (entropy deltas) are associated with phenomenal transitions.
Physical Computation, P/poly and P/log*
Venue: arXiv cs.CC 2016
Year: 2016

In this paper we give a framework for describing how abstract systems can be used to compute if no randomness or error is involved. Using this we describe a class of classical "physical" computation systems whose computational capabilities in polynomial time are equivalent to P/poly. We then extend our framework to describe how measurement and transformation times may vary depending on their input. Finally we describe two classes of classical "physical" computation systems in this new framework whose computational capabilities in polynomial time are equivalent to P/poly and P/log*.
Formal Dependability Modeling and Analysis: A Survey
Venue: arXiv cs.SE 2016
Year: 2016

Dependability is an umbrella concept that subsumes many key properties about a system, including reliability, maintainability, safety, availability, confidentiality, and integrity. Various dependability modeling techniques have been developed to effectively capture the failure characteristics of systems over time. Traditionally, dependability models are analyzed using paper-and-pencil proof methods and computer based simulation tools but their results cannot be trusted due to their inherent inaccuracy limitations. The recent developments in probabilistic analysis support using formal methods have enabled the possibility of accurate and rigorous dependability analysis. Thus, the usage of formal methods for dependability analysis is widely advocated for safety-critical domains, such as transportation, aerospace and health. Given the complementary strengths of mainstream formal methods, like theorem proving and model checking, and the variety of dependability models judging the most suitable formal technique for a given dependability model is not a straightforward task. In this paper, we present a comprehensive review of existing formal dependability analysis techniques along with their pros and cons for handling a particular dependability model.
Mobile Converged Networks: Framework, Optimization and Challenges
Venue: arXiv cs.NI 2016
Year: 2016

In this paper, a new framework of mobile converged networks is proposed for flexible resource optimization over multi-tier wireless heterogeneous networks. Design principles and advantages of this new framework of mobile converged networks are discussed. Moreover, mobile converged network models based on interference coordination and energy efficiency are presented and the corresponding optimization algorithms are developed. Furthermore, future challenges of mobile converged networks are identified to promote the study in modeling and performance analysis of mobile converged networks.
Adaptive Task Assignment in Online Learning Environments
Venue: arXiv cs.AI 2016
Year: 2016

With the increasing popularity of online learning, intelligent tutoring systems are regaining increased attention. In this paper, we introduce adaptive algorithms for personalized assignment of learning tasks to student so that to improve his performance in online learning environments. As main contribution of this paper, we propose a a novel Skill-Based Task Selector (SBTS) algorithm which is able to approximate a student's skill level based on his performance and consequently suggest adequate assignments. The SBTS is inspired by the class of multi-armed bandit algorithms. However, in contrast to standard multi-armed bandit approaches, the SBTS aims at acquiring two criteria related to student learning, namely: which topics should the student work on, and what level of difficulty should the task be. The SBTS centers on innovative reward and punishment schemes in a task and skill matrix based on the student behaviour. To verify the algorithm, the complex student behaviour is modelled using a neighbour node selection approach based on empirical estimations of a students learning curve. The algorithm is evaluated with a practical scenario from a basic java programming course. The SBTS is able to quickly and accurately adapt to the composite student competency --- even with a multitude of student models.
Non Local Spatial and Angular Matching : Enabling higher spatial resolution diffusion MRI datasets through adaptive denoising
Venue: arXiv cs.CV 2016
Year: 2016

Diffusion magnetic resonance imaging datasets suffer from low Signal-to-Noise Ratio, especially at high b-values. Acquiring data at high b-values contains relevant information and is now of great interest for microstructural and connectomics studies. High noise levels bias the measurements due to the non-Gaussian nature of the noise, which in turn can lead to a false and biased estimation of the diffusion parameters. Additionally, the usage of in-plane acceleration techniques during the acquisition leads to a spatially varying noise distribution, which depends on the parallel acceleration method implemented on the scanner. This paper proposes a novel diffusion MRI denoising technique that can be used on all existing data, without adding to the scanning time. We first apply a statistical framework to convert the noise to Gaussian distributed noise, effectively removing the bias. We then introduce a spatially and angular adaptive denoising technique, the Non Local Spatial and Angular Matching (NLSAM) algorithm. Each volume is first decomposed in small 4D overlapping patches to capture the structure of the diffusion data and a dictionary of atoms is learned on those patches. A local sparse decomposition is then found by bounding the reconstruction error with the local noise variance. We compare against three other state-of-the-art denoising methods and show quantitative local and connectivity results on a synthetic phantom and on an in-vivo high resolution dataset. Overall, our method restores perceptual information, removes the noise bias in common diffusion metrics, restores the extracted peaks coherence and improves reproducibility of tractography. Our work paves the way for higher spatial resolution acquisition of diffusion MRI datasets, which could in turn reveal new anatomical details that are not discernible at the spatial resolution currently used by the diffusion MRI community.
Human Computer Interaction Using Marker Based Hand Gesture Recognition
Venue: arXiv cs.HC 2016
Year: 2016

Human Computer Interaction (HCI) has been redefined in this era. People want to interact with their devices in such a way that has physical significance in the real world, in other words, they want ergonomic input devices. In this paper, we propose a new method of interaction with computing devices having a consumer grade camera, that uses two colored markers (red and green) worn on tips of the fingers to generate desired hand gestures, and for marker detection and tracking we used template matching with kalman filter. We have implemented all the usual system commands, i.e., cursor movement, right click, left click, double click, going forward and backward, zoom in and out through different hand gestures. Our system can easily recognize these gestures and give corresponding system commands. Our system is suitable for both desktop devices and devices where touch screen is not feasible like large screens or projected screens.
Event Abstraction for Process Mining using Supervised Learning Techniques
Venue: arXiv cs.LG 2016
Year: 2016

Process mining techniques focus on extracting insight in processes from event logs. In many cases, events recorded in the event log are too fine-grained, causing process discovery algorithms to discover incomprehensible process models or process models that are not representative of the event log. We show that when process discovery algorithms are only able to discover an unrepresentative process model from a low-level event log, structure in the process can in some cases still be discovered by first abstracting the event log to a higher level of granularity. This gives rise to the challenge to bridge the gap between an original low-level event log and a desired high-level perspective on this log, such that a more structured or more comprehensible process model can be discovered. We show that supervised learning can be leveraged for the event abstraction task when annotations with high-level interpretations of the low-level events are available for a subset of the sequences (i.e., traces). We present a method to generate feature vector representations of events based on XES extensions, and describe an approach to abstract events in an event log with Condition Random Fields using these event features. Furthermore, we propose a sequence-focused metric to evaluate supervised event abstraction results that fits closely to the tasks of process discovery and conformance checking. We conclude this paper by demonstrating the usefulness of supervised event abstraction for obtaining more structured and/or more comprehensible process models using both real life event data and synthetic event data.
Explaining Predictions of Non-Linear Classifiers in NLP
Venue: arXiv cs.CL 2016
Year: 2016

Layer-wise relevance propagation (LRP) is a recently proposed technique for explaining predictions of complex non-linear classifiers in terms of input variables. In this paper, we apply LRP for the first time to natural language processing (NLP). More precisely, we use it to explain the predictions of a convolutional neural network (CNN) trained on a topic categorization task. Our analysis highlights which words are relevant for a specific prediction of the CNN. We compare our technique to standard sensitivity analysis, both qualitatively and quantitatively, using a "word deleting" perturbation experiment, a PCA analysis, and various visualizations. All experiments validate the suitability of LRP for explaining the CNN predictions, which is also in line with results reported in recent image classification studies.
Multiplierless 16-point DCT Approximation for Low-complexity Image and Video Coding
Venue: arXiv cs.CV 2016
Year: 2016

An orthogonal 16-point approximate discrete cosine transform (DCT) is introduced. The proposed transform requires neither multiplications nor bit-shifting operations. A fast algorithm based on matrix factorization is introduced, requiring only 44 additions---the lowest arithmetic cost in literature. To assess the introduced transform, computational complexity, similarity with the exact DCT, and coding performance measures are computed. Classical and state-of-the-art 16-point low-complexity transforms were used in a comparative analysis. In the context of image compression, the proposed approximation was evaluated via PSNR and SSIM measurements, attaining the best cost-benefit ratio among the competitors. For video encoding, the proposed approximation was embedded into a HEVC reference software for direct comparison with the original HEVC standard. Physically realized and tested using FPGA hardware, the proposed transform showed 35% and 37% improvements of area-time and area-time-squared VLSI metrics when compared to the best competing transform in the literature.