OpenRaiser/Intern-Atlas huggingface dataset:
Fair Termination for Parameterized Probabilistic Concurrent Systems (Technical Report)
Venue: arXiv cs.LO 2017
Year: 2017

We consider the problem of automatically verifying that a parameterized family of probabilistic concurrent systems terminates with probability one for all instances against adversarial schedulers. A parameterized family defines an infinite-state system: for each number n, the family consists of an instance with n finite-state processes. In contrast to safety, the parameterized verification of liveness is currently still considered extremely challenging especially in the presence of probabilities in the model. One major challenge is to provide a sufficiently powerful symbolic framework. One well-known symbolic framework for the parameterized verification of non-probabilistic concurrent systems is regular model checking. Although the framework was recently extended to probabilistic systems, incorporating fairness in the framework - often crucial for verifying termination - has been especially difficult due to the presence of an infinite number of fairness constraints (one for each process). Our main contribution is a systematic, regularity-preserving, encoding of finitary fairness (a realistic notion of fairness proposed by Alur & Henzinger) in the framework of regular model checking for probabilistic parameterized systems. Our encoding reduces termination with finitary fairness to verifying parameterized termination without fairness over probabilistic systems in regular model checking (for which a verification framework already exists). We show that our algorithm could verify termination for many interesting examples from distributed algorithms (Herman's protocol) and evolutionary biology (Moran process, cell cycle switch), which do not hold under the standard notion of fairness. To the best of our knowledge, our algorithm is the first fully-automatic method that can prove termination for these examples.
How deep learning works --The geometry of deep learning
Venue: arXiv cs.LG 2017
Year: 2017

Why and how that deep learning works well on different tasks remains a mystery from a theoretical perspective. In this paper we draw a geometric picture of the deep learning system by finding its analogies with two existing geometric structures, the geometry of quantum computations and the geometry of the diffeomorphic template matching. In this framework, we give the geometric structures of different deep learning systems including convolutional neural networks, residual networks, recursive neural networks, recurrent neural networks and the equilibrium prapagation framework. We can also analysis the relationship between the geometrical structures and their performance of different networks in an algorithmic level so that the geometric framework may guide the design of the structures and algorithms of deep learning systems.
2D Unitary ESPRIT Based Super-Resolution Channel Estimation for Millimeter-Wave Massive MIMO with Hybrid Precoding
Venue: arXiv cs.IT 2017
Year: 2017

Millimeter-wave (mmWave) massive multiple-input multiple-output (MIMO) with hybrid precoding is a promising technique for the future 5G wireless communications. Due to a large number of antennas but a much smaller number of radio frequency (RF) chains, estimating the high-dimensional mmWave massive MIMO channel will bring the large pilot overhead. To overcome this challenge, this paper proposes a super-resolution channel estimation scheme based on two-dimensional (2D) u- nitary ESPRIT algorithm. By exploiting the angular sparsity of mmWave channels, the continuously distributed angle of arrivals/departures (AoAs/AoDs) can be jointly estimated with high accuracy. Specifically, by designing the uplink training signals at both base station (BS) and mobile station (MS), we first use low pilot overhead to estimate a low-dimensional effective channel, which has the same shift-invariance of array response as the high-dimensional mmWave MIMO channel to be estimated. From the low-dimensional effective channel, the super- resolution estimates of AoAs and AoDs can be jointly obtained by exploiting the 2D unitary ESPRIT channel estimation algorithm. Furthermore, the associated path gains can be acquired based on the least squares (LS) criterion. Finally, we can reconstruct the high-dimensional mmWave MIMO channel according to the obtained AoAs, AoDs, and path gains. Simulation results have confirmed that the proposed scheme is superior to conventional schemes with a much lower pilot overhead.
Verification of BSF Parallel Computational Model
Venue: arXiv cs.DC 2017
Year: 2017

The article is devoted to the verification of the BSF parallel computing model. The BSF-model is an evolution of the "master-slave" model and SPMD-model. The BSF-model is oriented to iterative algorithms that are implemented in cluster computing systems. The article briefly describes the basics of the BSF-model and its cost metrics. The structure of the BSF program is shown in the form of a UML activity diagram. The simulator of BSF-programs, implemented in C++ language using the MPI-library, is described. The results of computational experiments confirming the adequacy of the cost metrics of the BSF-model are presented.
Device-centric Energy Optimization for Edge Cloud Offloading
Venue: arXiv cs.DC 2017
Year: 2017

A wireless system is considered, where, computationally complex algorithms are offloaded from user devices to an edge cloud server, for the purpose of efficient battery usage. The main focus of this paper is to characterize and analyze, the trade-off between the energy consumed for processing the data locally, and for offloading. An analytical framework is presented, that minimizes the in-device energy consumption, by providing an optimal offloading decision for multiple user devices. A closed form solution is obtained for the offloading decision. The solution also provides the amount of computational data that should be offloaded, for the given computational and communication resources. Consequently, reduction in the energy consumption is observed.
Structure-preserving discrete-time optimal maneuvers of a wheeled inverted pendulum
Venue: arXiv cs.SY 2017
Year: 2017

The Wheeled Inverted Pendulum (WIP) is a nonholonomic, underactuated mechanical system, and has been popularized commercially as the {\it Segway}. Designing optimal control laws for point-to-point state-transfer for this autonomous mechanical system, while respecting momentum and torque constraints as well as the underlying manifold, continues to pose challenging problems. In this article we present a successful effort in this direction: We employ geometric mechanics to obtain a discrete-time model of the system, followed by the synthesis of an energy-optimal control based on a discrete-time maximum principle applicable to mechanical systems whose configuration manifold is a Lie group. Moreover, we incorporate state and momentum constraints into the discrete-time control directly at the synthesis stage. The control is implemented on a WIP with parameters obtained from an existing prototype; the results are highly encouraging, as demonstrated by numerical experiments.
An Artificial-Noise-Aided Secure Scheme for Hybrid Parallel PLC/Wireless OFDM Systems
Venue: arXiv cs.IT 2017
Year: 2017

We investigate the physical-layer security of indoor hybrid parallel power-line/wireless orthogonal-frequency division-multiplexing (OFDM) communication systems. We propose an artificial-noise (AN) aided scheme to enhance the system's security in the presence of an eavesdropper by exploiting the decoupled nature of the power-line and wireless communication media. The proposed scheme does not require the instantaneous channel state information of the eavesdropper's links to be known at the legitimate nodes. In our proposed scheme, the legitimate transmitter (Alice) and the legitimate receiver (Bob) cooperate to secure the hybrid system where an AN signal is shared from Bob to Alice on the link with the lower channel-to-noise ratio (CNR) while the information stream in addition to a noisy-amplified version of the received AN signal is transmitted from Alice to Bob on the link with higher CNR at each OFDM sub-channel. In addition, we investigate the effect of the transmit power levels at both Alice and Bob and the power allocation ratio between the data and AN signals at Alice on the secure throughput. We investigate both single-link eavesdropping attacks, where only one link is exposed to eavesdropping attacks, and two-link eavesdropping attacks, where the two links are exposed to eavesdropping attacks.
How Should a Robot Assess Risk? Towards an Axiomatic Theory of Risk in Robotics
Venue: arXiv cs.RO 2017
Year: 2017

Endowing robots with the capability of assessing risk and making risk-aware decisions is widely considered a key step toward ensuring safety for robots operating under uncertainty. But, how should a robot quantify risk? A natural and common approach is to consider the framework whereby costs are assigned to stochastic outcomes - an assignment captured by a cost random variable. Quantifying risk then corresponds to evaluating a risk metric, i.e., a mapping from the cost random variable to a real number. Yet, the question of what constitutes a "good" risk metric has received little attention within the robotics community. The goal of this paper is to explore and partially address this question by advocating axioms that risk metrics in robotics applications should satisfy in order to be employed as rational assessments of risk. We discuss general representation theorems that precisely characterize the class of metrics that satisfy these axioms (referred to as distortion risk metrics), and provide instantiations that can be used in applications. We further discuss pitfalls of commonly used risk metrics in robotics, and discuss additional properties that one must consider in sequential decision making tasks. Our hope is that the ideas presented here will lead to a foundational framework for quantifying risk (and hence safety) in robotics applications.
Continuous Authentication Using One-class Classifiers and their Fusion
Venue: arXiv cs.CV 2017
Year: 2017

While developing continuous authentication systems (CAS), we generally assume that samples from both genuine and impostor classes are readily available. However, the assumption may not be true in certain circumstances. Therefore, we explore the possibility of implementing CAS using only genuine samples. Specifically, we investigate the usefulness of four one-class classifiers OCC (elliptic envelope, isolation forest, local outliers factor, and one-class support vector machines) and their fusion. The performance of these classifiers was evaluated on four distinct behavioral biometric datasets, and compared with eight multi-class classifiers (MCC). The results demonstrate that if we have sufficient training data from the genuine user the OCC, and their fusion can closely match the performance of the majority of MCC. Our findings encourage the research community to use OCC in order to build CAS as they do not require knowledge of impostor class during the enrollment process.
Indirect Supervision for Relation Extraction using Question-Answer Pairs
Venue: arXiv cs.CL 2017
Year: 2017

Automatic relation extraction (RE) for types of interest is of great importance for interpreting massive text corpora in an efficient manner. Traditional RE models have heavily relied on human-annotated corpus for training, which can be costly in generating labeled data and become obstacles when dealing with more relation types. Thus, more RE extraction systems have shifted to be built upon training data automatically acquired by linking to knowledge bases (distant supervision). However, due to the incompleteness of knowledge bases and the context-agnostic labeling, the training data collected via distant supervision (DS) can be very noisy. In recent years, as increasing attention has been brought to tackling question-answering (QA) tasks, user feedback or datasets of such tasks become more accessible. In this paper, we propose a novel framework, ReQuest, to leverage question-answer pairs as an indirect source of supervision for relation extraction, and study how to use such supervision to reduce noise induced from DS. Our model jointly embeds relation mentions, types, QA entity mention pairs and text features in two low-dimensional spaces (RE and QA), where objects with same relation types or semantically similar question-answer pairs have similar representations. Shared features connect these two spaces, carrying clearer semantic knowledge from both sources. ReQuest, then use these learned embeddings to estimate the types of test relation mentions. We formulate a global objective function and adopt a novel margin-based QA loss to reduce noise in DS by exploiting semantic evidence from the QA dataset. Our experimental results achieve an average of 11% improvement in F1 score on two public RE datasets combined with TREC QA dataset.
The Exact Solution to Rank-1 L1-norm TUCKER2 Decomposition
Venue: arXiv cs.DS 2017
Year: 2017

We study rank-1 {L1-norm-based TUCKER2} (L1-TUCKER2) decomposition of 3-way tensors, treated as a collection of $N$ $D \times M$ matrices that are to be jointly decomposed. Our contributions are as follows. i) We prove that the problem is equivalent to combinatorial optimization over $N$ antipodal-binary variables. ii) We derive the first two algorithms in the literature for its exact solution. The first algorithm has cost exponential in $N$; the second one has cost polynomial in $N$ (under a mild assumption). Our algorithms are accompanied by formal complexity analysis. iii) We conduct numerical studies to compare the performance of exact L1-TUCKER2 (proposed) with standard HOSVD, HOOI, GLRAM, PCA, L1-PCA, and TPCA-L1. Our studies show that L1-TUCKER2 outperforms (in tensor approximation) all the above counterparts when the processed data are outlier corrupted.
Global Rank Estimation
Venue: arXiv cs.SI 2017
Year: 2017

In real world complex networks, the importance of a node depends on two important parameters: 1. characteristics of the node, and 2. the context of the given application. The current literature contains several centrality measures that have been defined to measure the importance of a node based on the given application requirements. These centrality measures assign a centrality value to each node that denotes its importance index. But in real life applications, we are more interested in the relative importance of the node that can be measured using its centrality rank based on the given centrality measure. To compute the centrality rank of a node, we need to compute the centrality value of all the nodes and compare them to get the rank. This process requires the entire network. So, it is not feasible for real-life applications due to the large size and dynamic nature of real world networks. In the present project, we aim to propose fast and efficient methods to estimate the global centrality rank of a node without computing the centrality value of all nodes. These methods can be further extended to estimate the rank without having the entire network. The proposed methods use the structural behavior of centrality measures, sampling techniques, or the machine learning models. In this work, we also discuss how to apply these methods for degree and closeness centrality rank estimation.
Tensor Regression Meets Gaussian Processes
Venue: arXiv cs.LG 2017
Year: 2017

Low-rank tensor regression, a new model class that learns high-order correlation from data, has recently received considerable attention. At the same time, Gaussian processes (GP) are well-studied machine learning models for structure learning. In this paper, we demonstrate interesting connections between the two, especially for multi-way data analysis. We show that low-rank tensor regression is essentially learning a multi-linear kernel in Gaussian processes, and the low-rank assumption translates to the constrained Bayesian inference problem. We prove the oracle inequality and derive the average case learning curve for the equivalent GP model. Our finding implies that low-rank tensor regression, though empirically successful, is highly dependent on the eigenvalues of covariance functions as well as variable correlations.
Spatio-temporal interaction model for crowd video analysis
Venue: arXiv cs.CV 2017
Year: 2017

We present an unsupervised approach to analyze crowd at various levels of granularity $-$ individual, group and collective. We also propose a motion model to represent the collective motion of the crowd. The model captures the spatio-temporal interaction pattern of the crowd from the trajectory data captured over a time period. Furthermore, we also propose an effective group detection algorithm that utilizes the eigenvectors of the interaction matrix of the model. We also show that the eigenvalues of the interaction matrix characterize various group activities such as being stationary, walking, splitting and approaching. The algorithm is also extended trivially to recognize individual activity. Finally, we discover the overall crowd behavior by classifying a crowd video in one of the eight categories. Since the crowd behavior is determined by its constituent groups, we demonstrate the usefulness of group level features during classification. Extensive experimentation on various datasets demonstrates a superlative performance of our algorithms over the state-of-the-art methods.
Image Patch Matching Using Convolutional Descriptors with Euclidean Distance
Venue: arXiv cs.CV 2017
Year: 2017

In this work we propose a neural network based image descriptor suitable for image patch matching, which is an important task in many computer vision applications. Our approach is influenced by recent success of deep convolutional neural networks (CNNs) in object detection and classification tasks. We develop a model which maps the raw input patch to a low dimensional feature vector so that the distance between representations is small for similar patches and large otherwise. As a distance metric we utilize L2 norm, i.e. Euclidean distance, which is fast to evaluate and used in most popular hand-crafted descriptors, such as SIFT. According to the results, our approach outperforms state-of-the-art L2-based descriptors and can be considered as a direct replacement of SIFT. In addition, we conducted experiments with batch normalization and histogram equalization as a preprocessing method of the input data. The results confirm that these techniques further improve the performance of the proposed descriptor. Finally, we show promising preliminary results by appending our CNNs with recently proposed spatial transformer networks and provide a visualisation and interpretation of their impact.
Capacity-Achieving PIR Schemes with Optimal Sub-Packetization
Venue: arXiv cs.IT 2017
Year: 2017

Suppose a database containing $M$ records is replicated across $N$ servers, and a user wants to privately retrieve one record by accessing the servers such that identity of the retrieved record is secret against any up to $T$ servers. A scheme designed for this purpose is called a private information retrieval (PIR) scheme. In practice, capacity-achieving and small sub-packetization are both desired for PIR schemes, because the former implies the highest download rate and the latter usually means simple realization. For general values of $N,T,M$, the only known capacity-achieving PIR scheme was designed by Sun and Jafar in 2016 with sub-packetization $N^M$. In this paper, we design a linear capacity-achieving PIR scheme with much smaller sub-packetization $dn^{M-1}$, where $d={\rm gcd}(N,T)$ and $n=N/d$. Furthermore, we prove that for any linear capacity-achieving PIR scheme it must have sub-packetization no less than $dn^{M-1}$, implying our scheme has the optimal sub-packetization. Moreover, comparing with Sun and Jafar's scheme, our scheme reduces the field size by a factor of $\frac{1}{Nd^{M-2}}$.
Updating the VESICLE-CNN Synapse Detector
Venue: arXiv cs.CV 2017
Year: 2017

We present an updated version of the VESICLE-CNN algorithm presented by Roncal et al. (2014). The original implementation makes use of a patch-based approach. This methodology is known to be slow due to repeated computations. We update this implementation to be fully convolutional through the use of dilated convolutions, recovering the expanded field of view achieved through the use of strided maxpools, but without a degradation of spatial resolution. This updated implementation performs as well as the original implementation, but with a $600\times$ speedup at test time. We release source code and data into the public domain.
Improved Bounds for Online Dominating Sets of Trees
Venue: arXiv cs.DS 2017
Year: 2017

The online dominating set problem is an online variant of the minimum dominating set problem, which is one of the most important NP-hard problems on graphs. This problem is defined as follows: Given an undirected graph $G = (V, E)$, in which $V$ is a set of vertices and $E$ is a set of edges. We say that a set $D \subseteq V$ of vertices is a {\em dominating set} of $G$ if for each $v \in V \setminus D$, there exists a vertex $u \in D$ such that $\{ u, v \} \in E$. The vertices are revealed to an online algorithm one by one over time. When a vertex is revealed, edges between the vertex and vertices revealed in the past are also revealed. A revelaed subtree is connected at any time. Immediately after the revelation of each vertex, an online algorithm can choose vertices which were already revealed irrevocably and must maintain a dominating set of a graph revealed so far. The cost of an algorithm on a given tree is the number of vertices chosen by it, and its objective is to minimize the cost. Eidenbenz (Technical report, Institute of Theoretical Computer Science, ETH Zürich, 2002) and Boyar et al.\ (SWAT 2016) studied the case in which given graphs are trees. They designed a deterministic online algorithm whose competitive ratio is at most three, and proved that a lower bound on the competitive ratio of any deterministic algorithm is two. In this paper, we also focus on trees. We establish a matching lower bound for any deterministic algorithm. Moreover, we design a randomized online algorithm whose competitive ratio is at most $5/2 = 2.5$, and show that the competitive ratio of any randomized algorithm is at least $4/3 \approx 1.333$.
Behavioural Change Support Intelligent Transportation Applications
Venue: arXiv cs.HC 2017
Year: 2017

This workshop invites researchers and practitioners to participate in exploring behavioral change support intelligent transportation applications. We welcome submissions that explore intelligent transportation systems (ITS), which interact with travelers in order to persuade them or nudge them towards sustainable transportation behaviors and decisions. Emerging opportunities including the use of data and information generated by ITS and users' mobile devices in order to render personalized, contextualized and timely transport behavioral change interventions are in our focus. We invite submissions and ideas from domains of ITS including, but not limited to, multi-modal journey planners, advanced traveler information systems and in-vehicle systems. The expected outcome will be a deeper understanding of the challenges and future research directions with respect to behavioral change support through ITS.