OpenRaiser/Intern-Atlas huggingface dataset:
Hybrid Automata for Formal Modeling and Verification of Cyber-Physical Systems
Venue: arXiv cs.LO 2015
Year: 2015

The presence of a tight integration between the discrete control (the "cyber") and the analog environment (the "physical")---via sensors and actuators over wired or wireless communication networks---is the defining feature of cyber-physical systems. Hence, the functional correctness of a cyber- physical system is crucially dependent not only on the dynamics of the analog physical environment, but also on the decisions taken by the discrete control that alter the dynamics of the environment. The framework of Hybrid automata---introduced by Alur, Courcoubetis, Henzinger, and Ho---provides a formal modeling and specification environment to analyze the interaction between the discrete and continuous parts of a cyber-physical system. Hybrid automata can be considered as generalizations of finite state automata augmented with a finite set of real-valued variables whose dynamics in each state is governed by a system of ordinary differential equations. Moreover, the discrete transitions of hybrid automata are guarded by constraints over the values of these real-valued variables, and enable discontinuous jumps in the evolution of these variables. Considering the richness of the dynamics in a hybrid automaton, it is perhaps not surprising that the fundamental verification questions, like reachability and schedulability, for the general model are undecidable. In this article we present a review of hybrid automata as modeling and verification framework for cyber-physical systems, and survey some of the key results related to practical verification questions related to hybrid automata.
Interactive MCQs as a tool for Knowledge Acquisition
Venue: arXiv cs.CY 2015
Year: 2015

Multiple Choice Questions or MCQs are very important for e-learning. Generally, MCQs are used as a tool for the assessment of student performance at the end of their learning sessions. Can MCQs become an important tool in the process of knowledge acquisition while attending a course? This paper intends to find out how MCQs could be used as a tool for the better understanding, coverage as well as knowledge acquisition.
Learning Sparse High Dimensional Filters: Image Filtering, Dense CRFs and Bilateral Neural Networks
Venue: arXiv cs.CV 2015
Year: 2015

Bilateral filters have wide spread use due to their edge-preserving properties. The common use case is to manually choose a parametric filter type, usually a Gaussian filter. In this paper, we will generalize the parametrization and in particular derive a gradient descent algorithm so the filter parameters can be learned from data. This derivation allows to learn high dimensional linear filters that operate in sparsely populated feature spaces. We build on the permutohedral lattice construction for efficient filtering. The ability to learn more general forms of high-dimensional filters can be used in several diverse applications. First, we demonstrate the use in applications where single filter applications are desired for runtime reasons. Further, we show how this algorithm can be used to learn the pairwise potentials in densely connected conditional random fields and apply these to different image segmentation tasks. Finally, we introduce layers of bilateral filters in CNNs and propose bilateral neural networks for the use of high-dimensional sparse data. This view provides new ways to encode model structure into network architectures. A diverse set of experiments empirically validates the usage of general forms of filters.
A Linear-Time Algorithm for Finding All Double-Vertex Dominators of a Given Vertex
Venue: arXiv cs.DS 2015
Year: 2015

Dominators provide a general mechanism for identifying reconverging paths in graphs. This is useful for a number of applications in Computer-Aided Design (CAD) including signal probability computation in biased random simulation, switching activity estimation in power and noise analysis, and cut points identification in equivalence checking. However, traditional single-vertex dominators are too rare in circuit graphs. In order to handle reconverging paths more efficiently, we consider the case of double-vertex dominators which occur more frequently. First, we derive a number of specific properties of double-vertex dominators. Then, we describe a data structure for representing all double-vertex dominators of a given vertex in linear space. Finally, we present an algorithm for finding all double-vertex dominators of a given vertex in linear time. Our results provide an efficient systematic way of partitioning large graphs along the reconverging points of the signal flow.
Modem Illumination of Monotone Polygons
Venue: arXiv cs.CG 2015
Year: 2015

We study a generalization of the classical problem of the illumination of polygons. Instead of modeling a light source we model a wireless device whose radio signal can penetrate a given number $k$ of walls. We call these objects $k$-modems and study the minimum number of $k$-modems sufficient and sometimes necessary to illuminate monotone and monotone orthogonal polygons. We show that every monotone polygon with $n$ vertices can be illuminated with $\big\lceil \frac{n-2}{2k+3} \big\rceil$ $k$-modems. In addition, we exhibit examples of monotone polygons requiring at least $\lceil \frac {n-2} {2k+3}\rceil$ $k$-modems to be illuminated. For monotone orthogonal polygons with $n$ vertices we show that for $k=1$ and for even $k$, every such polygon can be illuminated with $\big\lceil \frac{n-2}{2k+4} \big\rceil$ $k$-modems, while for odd $k\geq3$, $\big\lceil \frac{n-2}{2k+6} \big\rceil$ $k$-modems are always sufficient. Further, by presenting according examples of monotone orthogonal polygons, we show that both bounds are tight.
Quantifying Morphological Computation based on an Information Decomposition of the Sensorimotor Loop
Venue: arXiv cs.AI 2015
Year: 2015

The question how an agent is affected by its embodiment has attracted growing attention in recent years. A new field of artificial intelligence has emerged, which is based on the idea that intelligence cannot be understood without taking into account embodiment. We believe that a formal approach to quantifying the embodiment's effect on the agent's behaviour is beneficial to the fields of artificial life and artificial intelligence. The contribution of an agent's body and environment to its behaviour is also known as morphological computation. Therefore, in this work, we propose a quantification of morphological computation, which is based on an information decomposition of the sensorimotor loop into shared, unique and synergistic information. In numerical simulation based on a formal representation of the sensorimotor loop, we show that the unique information of the body and environment is a good measure for morphological computation. The results are compared to our previously derived quantification of morphological computation.
Quality Assessment of Linked Datasets using Probabilistic Approximation
Venue: arXiv cs.DB 2015
Year: 2015

With the increasing application of Linked Open Data, assessing the quality of datasets by computing quality metrics becomes an issue of crucial importance. For large and evolving datasets, an exact, deterministic computation of the quality metrics is too time consuming or expensive. We employ probabilistic techniques such as Reservoir Sampling, Bloom Filters and Clustering Coefficient estimation for implementing a broad set of data quality metrics in an approximate but sufficiently accurate way. Our implementation is integrated in the comprehensive data quality assessment framework Luzzu. We evaluated its performance and accuracy on Linked Open Datasets of broad relevance.
Analysis of PCA Algorithms in Distributed Environments
Venue: arXiv cs.DC 2015
Year: 2015

Classical machine learning algorithms often face scalability bottlenecks when they are applied to large-scale data. Such algorithms were designed to work with small data that is assumed to fit in the memory of one machine. In this report, we analyze different methods for computing an important machine learing algorithm, namely Principal Component Analysis (PCA), and we comment on its limitations in supporting large datasets. The methods are analyzed and compared across two important metrics: time complexity and communication complexity. We consider the worst-case scenarios for both metrics, and we identify the software libraries that implement each method. The analysis in this report helps researchers and engineers in (i) understanding the main bottlenecks for scalability in different PCA algorithms, (ii) choosing the most appropriate method and software library for a given application and data set characteristics, and (iii) designing new scalable PCA algorithms.
Improved Calibration of Near-Infrared Spectra by Using Ensembles of Neural Network Models
Venue: arXiv cs.NE 2015
Year: 2015

IR or near-infrared (NIR) spectroscopy is a method used to identify a compound or to analyze the composition of a material. Calibration of NIR spectra refers to the use of the spectra as multivariate descriptors to predict concentrations of the constituents. To build a calibration model, state-of-the-art software predominantly uses linear regression techniques. For nonlinear calibration problems, neural network-based models have proved to be an interesting alternative. In this paper, we propose a novel extension of the conventional neural network-based approach, the use of an ensemble of neural network models. The individual neural networks are obtained by resampling the available training data with bootstrapping or cross-validation techniques. The results obtained for a realistic calibration example show that the ensemble-based approach produces a significantly more accurate and robust calibration model than conventional regression methods.
Adjusted Haar Wavelet for Application in the Power Systems Disturbance Analysis
Venue: arXiv cs.OH 2015
Year: 2015

Abrupt change detection based on the wavelet transform and threshold method is very effective in detecting the abrupt changes and hence segmenting the signals recorded during disturbances in the electrical power network. The wavelet method estimates the time-instants of the changes in the signal model parameters during the pre-fault condition, after initiation of fault, after circuit-breaker opening and auto-reclosure. Certain kinds of disturbance signals do not show distinct abrupt changes in the signal parameters. In those cases, the standard mother wavelets fail to achieve correct event-specific segmentations. A new adjustment technique to the standard Haar wavelet is proposed in this paper, by introducing 2n adjusting zeros in the Haar wavelet scaling filter, n being a positive integer. This technique is quite effective in segmenting those fault signals into pre- and post-fault segments, and it is an improvement over the standard mother wavelets for this application. This paper presents many practical examples where recorded signals from the power network in South Africa have been used.
Easy and Fast Design and Implementation of PostgreSQL based image handling application
Venue: arXiv cs.DB 2015
Year: 2015

In modern computing, RDBMS are great to store different types of data. To a developer, one of the major objectives is to provide a very low cost and easy to use solution to an existing problem. While commercial databases are more easy to use along with their new as well as documented features come with complicated licensing cost, free open source databases are not that straightforward under many situations. This paper shows how a completely free advanced open source RDBMS like PostgreSQL could be designed and modified to store and retrieve high quality images in order to use them along with a frontend application.
Discrete Signal Reconstruction by Sum of Absolute Values
Venue: arXiv cs.IT 2015
Year: 2015

In this letter, we consider a problem of reconstructing an unknown discrete signal taking values in a finite alphabet from incomplete linear measurements. The difficulty of this problem is that the computational complexity of the reconstruction is exponential as it is. To overcome this difficulty, we extend the idea of compressed sensing, and propose to solve the problem by minimizing the sum of weighted absolute values. We assume that the probability distribution defined on an alphabet is known, and formulate the reconstruction problem as linear programming. Examples are shown to illustrate that the proposed method is effective.
On the Performance of Turbo Signal Recovery with Partial DFT Sensing Matrices
Venue: arXiv cs.IT 2015
Year: 2015

This letter is on the performance of the turbo signal recovery (TSR) algorithm for partial discrete Fourier transform (DFT) matrices based compressed sensing. Based on state evolution analysis, we prove that TSR with a partial DFT sensing matrix outperforms the well-known approximate message passing (AMP) algorithm with an independent identically distributed (IID) sensing matrix.
A Transfer Learning Approach for Cache-Enabled Wireless Networks
Venue: arXiv cs.IT 2015
Year: 2015

Locally caching contents at the network edge constitutes one of the most disruptive approaches in $5$G wireless networks. Reaping the benefits of edge caching hinges on solving a myriad of challenges such as how, what and when to strategically cache contents subject to storage constraints, traffic load, unknown spatio-temporal traffic demands and data sparsity. Motivated by this, we propose a novel transfer learning-based caching procedure carried out at each small cell base station. This is done by exploiting the rich contextual information (i.e., users' content viewing history, social ties, etc.) extracted from device-to-device (D2D) interactions, referred to as source domain. This prior information is incorporated in the so-called target domain where the goal is to optimally cache strategic contents at the small cells as a function of storage, estimated content popularity, traffic load and backhaul capacity. It is shown that the proposed approach overcomes the notorious data sparsity and cold-start problems, yielding significant gains in terms of users' quality-of-experience (QoE) and backhaul offloading, with gains reaching up to $22\%$ in a setting consisting of four small cell base stations.
GSNs : Generative Stochastic Networks
Venue: arXiv cs.LG 2015
Year: 2015

We introduce a novel training principle for probabilistic models that is an alternative to maximum likelihood. The proposed Generative Stochastic Networks (GSN) framework is based on learning the transition operator of a Markov chain whose stationary distribution estimates the data distribution. Because the transition distribution is a conditional distribution generally involving a small move, it has fewer dominant modes, being unimodal in the limit of small moves. Thus, it is easier to learn, more like learning to perform supervised function approximation, with gradients that can be obtained by back-propagation. The theorems provided here generalize recent work on the probabilistic interpretation of denoising auto-encoders and provide an interesting justification for dependency networks and generalized pseudolikelihood (along with defining an appropriate joint distribution and sampling mechanism, even when the conditionals are not consistent). We study how GSNs can be used with missing inputs and can be used to sample subsets of variables given the rest. Successful experiments are conducted, validating these theoretical results, on two image datasets and with a particular architecture that mimics the Deep Boltzmann Machine Gibbs sampler but allows training to proceed with backprop, without the need for layerwise pretraining.
Hybrid Social Networking Application for a University Community
Venue: arXiv cs.SI 2015
Year: 2015

A hybrid social network for building social communities for a university community is presented. The system employed the semantic ontology for an offline/online social network site (SNS). It captures the core features of an SNS including profile creation, friend invite/search, group formation, chatting/messaging, blogging and voting. Three core frameworks - the peer2me framework, SMSN semantic mobile social network and Peoplepods framework were considered in the implementation phase. The results show remarkable matching performance for prosumers with similar interests with relevance close to unity. The social network was able to capture the needs of the university students by serving as a handy direction to popular locations within the campus.
Binary sequences with three-valued cross correlations of different lengths
Venue: arXiv cs.IT 2015
Year: 2015

In this paper, new pairs of binary sequences with three cross correlation values are presented. The cross correlation values are shown to be low. Finally we present some numerical results and some open problems.
Automatic Pollen Grain and Exine Segmentation from Microscope Images
Venue: arXiv cs.CV 2015
Year: 2015

In this article, we propose an automatic method for the segmentation of pollen grains from microscope images, followed by the automatic segmentation of their exine. The objective of exine segmentation is to separate the pollen grain in two regions of interest: exine and inner part. A coarse-to-fine approach ensures a smooth and accurate segmentation of both structures. As a rough stage, grain segmentation is performed by a procedure involving clustering and morphological operations, while the exine is approximated by an iterative procedure consisting in consecutive cropping steps of the pollen grain. A snake-based segmentation is performed to refine the segmentation of both structures. Results have shown that our segmentation method is able to deal with different pollen types, as well as with different types of exine and inner part appearance. The proposed segmentation method aims to be generic and has been designed as one of the core steps of an automatic pollen classification framework.
Interactive Illustrative Line Styles and Line Style Transfer Functions for Flow Visualization
Venue: arXiv cs.GR 2015
Year: 2015

We present a flexible illustrative line style model for the visualization of streamline data. Our model partitions view-oriented line strips into parallel bands whose basic visual properties can be controlled independently. We thus extend previous line stylization techniques specifically for visualization purposes by allowing the parametrization of these bands based on the local line data attributes. Moreover, our approach supports emphasis and abstraction by introducing line style transfer functions that map local line attribute values to complete line styles. With a flexible GPU implementation of this line style model we enable the interactive exploration of visual representations of streamlines. We demonstrate the effectiveness of our model by applying it to 3D flow field datasets.
Analysis and Throughput Optimization of Selective Chase Combining for OFDM Systems
Venue: arXiv cs.IT 2015
Year: 2015

In this paper, we present throughput analysis and optimization of bandwidth efficient selective retransmission method at modulation layer for conventional Chase Combining (CC) method under orthogonal frequency division multiplexing (OFDM) signaling. Most of the times, there are fewer errors in a failed packet and receiver can recover from errors receiving partial copy of original frame. The proposed selective retransmission method at modulation layer for OFDM modulation requests retransmission of information corresponding to the poor quality subcarriers. In this work, we propose cross-layer multiple selective Chase combining (MSCC) method and Chase combining with selective retransmission (CCWS) at modulation level. We also present bit-error rate (BER) and throughput analysis of the proposed MSCC and CCWS methods. In order to maximize throughput of the proposed methods under OFDM signaling, we formulate optimization problem with respect to amount of information to be retransmitted in selective retransmission in the event of packet failure. We present tight BER upper bounds and tight throughput lower bounds for the proposed selective Chase combining methods. The simulation results demonstrate significant throughput gain of the optimized selective retransmission methods over conventional retransmission methods. The throughput gain of the proposed selective retransmission atmodulation layer are also holds for conventional for hybrid automatic repeat request (HARQ) methods.
Regular realizability problems and regular languages
Venue: arXiv cs.FL 2015
Year: 2015

We investigate regular realizability (RR) problems, which are the problems of verifying whether intersection of a regular language -- the input of the problem -- and fixed language called filter is non-empty. We consider two kind of problems depending on representation of regular language. If a regular language on input is represented by a DFA, then we obtain (deterministic) regular realizability problem and we show that in this case the complexity of regular realizability problem for an arbitrary regular filter is either L-complete or NL-complete. We also show that in case of representation regular language on input by NFA the problem is always NL-complete.
Distributed Time-Sensitive Task Selection in Mobile Crowdsensing
Venue: arXiv cs.GT 2015
Year: 2015

With the rich set of embedded sensors installed in smartphones and the large number of mobile users, we witness the emergence of many innovative commercial mobile crowdsensing applications that combine the power of mobile technology with crowdsourcing to deliver time-sensitive and location-dependent information to their customers. Motivated by these real-world applications, we consider the task selection problem for heterogeneous users with different initial locations, movement costs, movement speeds, and reputation levels. Computing the social surplus maximization task allocation turns out to be an NP-hard problem. Hence we focus on the distributed case, and propose an asynchronous and distributed task selection (ADTS) algorithm to help the users plan their task selections on their own. We prove the convergence of the algorithm, and further characterize the computation time for users' updates in the algorithm. Simulation results suggest that the ADTS scheme achieves the highest Jain's fairness index and coverage comparing with several benchmark algorithms, while yielding similar user payoff to a greedy centralized benchmark. Finally, we illustrate how mobile users coordinate under the ADTS scheme based on some practical movement time data derived from Google Maps.
Tree spanners of small diameter
Venue: arXiv cs.DM 2015
Year: 2015

A graph that contains a spanning tree of diameter at most $t$ clearly admits a tree $t$-spanner, since a tree $t$-spanner of a graph $G$ is a sub tree of $G$ such that the distance between pairs of vertices in the tree is at most $t$ times their distance in $G$. In this paper, graphs that admit a tree $t$-spanner of diameter at most $t+1$ are studied. For $t$ equal to 1 or 2 the problem has been solved. For $t=3$ we present an algorithm that determines if a graph admits a tree 3-spanner of diameter at most 4. For $t\geq4$ it is proved that it is an NP-complete problem to decide whether a graph admits a tree $t$-spanner of diameter at most $t+1$.