OpenRaiser/Intern-Atlas huggingface dataset:
Towards parallelizable sampling-based Nonlinear Model Predictive Control
Venue: arXiv cs.SY 2017
Year: 2017

This paper proposes a new sampling-based nonlinear model predictive control (MPC) algorithm, with a bound on complexity quadratic in the prediction horizon N and linear in the number of samples. The idea of the proposed algorithm is to use the sequence of predicted inputs from the previous time step as a warm start, and to iteratively update this sequence by changing its elements one by one, starting from the last predicted input and ending with the first predicted input. This strategy, which resembles the dynamic programming principle, allows for parallelization up to a certain level and yields a suboptimal nonlinear MPC algorithm with guaranteed recursive feasibility, stability and improved cost function at every iteration, which is suitable for real-time implementation. The complexity of the algorithm per each time step in the prediction horizon depends only on the horizon, the number of samples and parallel threads, and it is independent of the measured system state. Comparisons with the fmincon nonlinear optimization solver on benchmark examples indicate that as the simulation time progresses, the proposed algorithm converges rapidly to the "optimal" solution, even when using a small number of samples.
WiLiTV: A Low-Cost Wireless Framework for Live TV Services
Venue: arXiv cs.MM 2017
Year: 2017

With the evolution of HDTV and Ultra HDTV, the bandwidth requirement for IP-based TV content is rapidly increasing. Consumers demand uninterrupted service with a high Quality of Experience (QoE). Service providers are constantly trying to differentiate themselves by innovating new ways of distributing content more efficiently with lower cost and higher penetration. In this work, we propose a cost-efficient wireless framework (WiLiTV) for delivering live TV services, consisting of a mix of wireless access technologies (e.g. Satellite, WiFi and LTE overlay links). In the proposed architecture, live TV content is injected into the network at a few residential locations using satellite dishes. The content is then further distributed to other homes using a house-to-house WiFi network or via an overlay LTE network. Our problem is to construct an optimal TV distribution network with the minimum number of satellite injection points, while preserving the highest QoE, for different neighborhood densities. We evaluate the framework using realistic time-varying demand patterns and a diverse set of home location data. Our study demonstrates that the architecture requires 75 - 90% fewer satellite injection points, compared to traditional architectures. Furthermore, we show that most cost savings can be obtained using simple and practical relay routing solutions.
A Crevice on the Crane Beach: Finite-Degree Predicates
Venue: arXiv cs.LO 2017
Year: 2017

First-order logic (FO) over words is shown to be equiexpressive with FO equipped with a restricted set of numerical predicates, namely the order, a binary predicate MSB$_0$, and the finite-degree predicates: FO[Arb] = FO[<, MSB$_0$, Fin]. The Crane Beach Property (CBP), introduced more than a decade ago, is true of a logic if all the expressible languages admitting a neutral letter are regular. Although it is known that FO[Arb] does not have the CBP, it is shown here that the (strong form of the) CBP holds for both FO[<, Fin] and FO[<, MSB$_0$]. Thus FO[<, Fin] exhibits a form of locality and the CBP, and can still express a wide variety of languages, while being one simple predicate away from the expressive power of FO[Arb]. The counting ability of FO[<, Fin] is studied as an application.
Multiset Combinatorial Batch Codes
Venue: arXiv cs.DM 2017
Year: 2017

Batch codes, first introduced by Ishai, Kushilevitz, Ostrovsky, and Sahai, mimic a distributed storage of a set of $n$ data items on $m$ servers, in such a way that any batch of $k$ data items can be retrieved by reading at most some $t$ symbols from each server. Combinatorial batch codes, are replication-based batch codes in which each server stores a subset of the data items. In this paper, we propose a generalization of combinatorial batch codes, called multiset combinatorial batch codes (MCBC), in which $n$ data items are stored in $m$ servers, such that any multiset request of $k$ items, where any item is requested at most $r$ times, can be retrieved by reading at most $t$ items from each server. The setup of this new family of codes is motivated by recent work on codes which enable high availability and parallel reads in distributed storage systems. The main problem under this paradigm is to minimize the number of items stored in the servers, given the values of $n,m,k,r,t$, which is denoted by $N(n,k,m,t;r)$. We first give a necessary and sufficient condition for the existence of MCBCs. Then, we present several bounds on $N(n,k,m,t;r)$ and constructions of MCBCs. In particular, we determine the value of $N(n,k,m,1;r)$ for any $n\geq \left\lfloor\frac{k-1}{r}\right\rfloor{m\choose k-1}-(m-k+1)A(m,4,k-2)$, where $A(m,4,k-2)$ is the maximum size of a binary constant weight code of length $m$, distance four and weight $k-2$. We also determine the exact value of $N(n,k,m,1;r)$ when $r\in\{k,k-1\}$ or $k=m$.
Cyclic spectra for wavelength-routed optical networks
Venue: arXiv cs.NI 2017
Year: 2017

We propose occupying guard-bands in closely-spaced WDM systems with redundant signal spectral components, to increase tolerance to frequency misalignment and channel shaping from multiplexing elements. By cyclically repeating the spectrum of a modulated signal, we show improved tolerance to impairments due to add/drop multiplexing with a commercial wavelength selective switch, in systems using 5-20% guard bands on a 50-GHz DWDM grid.
Agile Inexact Methods for Spectral Projector-Based Graph Fourier Transforms
Venue: arXiv cs.SI 2017
Year: 2017

We propose an inexact method for the graph Fourier transform of a graph signal, as defined by the signal decomposition over the Jordan subspaces of the graph adjacency matrix. This method projects the signal over the generalized eigenspaces of the adjacency matrix, which accelerates the transform computation over large, sparse, and directed adjacency matrices. The trade-off between execution time and fidelity to the original graph structure is discussed. In addition, properties such as a generalized Parseval's identity and total variation ordering of the generalized eigenspaces are discussed. The method is applied to 2010-2013 NYC taxi trip data to identify traffic hotspots on the Manhattan grid. Our results show that identical highly expressed geolocations can be identified with the inexact method and the method based on eigenvector projections, while reducing computation time by a factor of 26,000 and reducing energy dispersal among the spectral components corresponding to the multiple zero eigenvalue.
Termination of Nondeterministic Recursive Probabilistic Programs
Venue: arXiv cs.PL 2017
Year: 2017

We study the termination problem for nondeterministic recursive probabilistic programs. First, we show that a ranking-supermartingales-based approach is both sound and complete for bounded terminiation (i.e., bounded expected termination time over all schedulers). Our result also clarifies previous results which claimed that ranking supermartingales are not a complete approach even for nondeterministic probabilistic programs without recursion. Second, we show that conditionally difference-bounded ranking supermartingales provide a sound approach for lower bounds of expected termination time. Finally, we show that supermartingales with lower bounds on conditional absolute difference provide a sound approach for almost-sure termination, along with explicit bounds on tail probabilities of nontermination within a given number of steps. We also present several illuminating counterexamples that establish the necessity of certain prerequisites (such as conditionally difference-bounded condition).
Liveness Verification and Synthesis: New Algorithms for Recursive Programs
Venue: arXiv cs.FL 2017
Year: 2017

We consider the problems of liveness verification and liveness synthesis for recursive programs. The liveness verification problem (LVP) is to decide whether a given omega-context-free language is contained in a given omega-regular language. The liveness synthesis problem (LSP) is to compute a strategy so that a given omega-context-free game, when played along the strategy, is guaranteed to derive a word in a given omega-regular language. The problems are known to be EXPTIME-complete and EXPTIME-complete, respectively. Our contributions are new algorithms with optimal time complexity. For LVP, we generalize recent lasso-finding algorithms (also known as Ramsey-based algorithms) from finite to recursive programs. For LSP, we generalize a recent summary-based algorithm from finite to infinite words. Lasso finding and summaries have proven to be efficient in a number of implementations for the finite state and finite word setting.
Distinguishing Antonyms and Synonyms in a Pattern-based Neural Network
Venue: arXiv cs.CL 2017
Year: 2017

Distinguishing between antonyms and synonyms is a key task to achieve high performance in NLP systems. While they are notoriously difficult to distinguish by distributional co-occurrence models, pattern-based methods have proven effective to differentiate between the relations. In this paper, we present a novel neural network model AntSynNET that exploits lexico-syntactic patterns from syntactic parse trees. In addition to the lexical and syntactic information, we successfully integrate the distance between the related words along the syntactic path as a new pattern feature. The results from classification experiments show that AntSynNET improves the performance over prior pattern-based methods.
Towards Smart Proof Search for Isabelle
Venue: arXiv cs.AI 2017
Year: 2017

Despite the recent progress in automatic theorem provers, proof engineers are still suffering from the lack of powerful proof automation. In this position paper we first report our proof strategy language based on a meta-tool approach. Then, we propose an AI-based approach to drastically improve proof automation for Isabelle, while identifying three major challenges we plan to address for this objective.
CNN-based Segmentation of Medical Imaging Data
Venue: arXiv cs.CV 2017
Year: 2017

Convolutional neural networks have been applied to a wide variety of computer vision tasks. Recent advances in semantic segmentation have enabled their application to medical image segmentation. While most CNNs use two-dimensional kernels, recent CNN-based publications on medical image segmentation featured three-dimensional kernels, allowing full access to the three-dimensional structure of medical images. Though closely related to semantic segmentation, medical image segmentation includes specific challenges that need to be addressed, such as the scarcity of labelled data, the high class imbalance found in the ground truth and the high memory demand of three-dimensional images. In this work, a CNN-based method with three-dimensional filters is demonstrated and applied to hand and brain MRI. Two modifications to an existing CNN architecture are discussed, along with methods on addressing the aforementioned challenges. While most of the existing literature on medical image segmentation focuses on soft tissue and the major organs, this work is validated on data both from the central nervous system as well as the bones of the hand.
Job Detection in Twitter
Venue: arXiv cs.CL 2017
Year: 2017

In this report, we propose a new application for twitter data called \textit{job detection}. We identify people's job category based on their tweets. As a preliminary work, we limited our task to identify only IT workers from other job holders. We have used and compared both simple bag of words model and a document representation based on Skip-gram model. Our results show that the model based on Skip-gram, achieves a 76\% precision and 82\% recall.
Depicting urban boundaries from a mobility network of spatial interactions: A case study of Great Britain with geo-located Twitter data
Venue: arXiv cs.SI 2017
Year: 2017

Existing urban boundaries are usually defined by government agencies for administrative, economic, and political purposes. Defining urban boundaries that consider socio-economic relationships and citizen commute patterns is important for many aspects of urban and regional planning. In this paper, we describe a method to delineate urban boundaries based upon human interactions with physical space inferred from social media. Specifically, we depicted the urban boundaries of Great Britain using a mobility network of Twitter user spatial interactions, which was inferred from over 69 million geo-located tweets. We define the non-administrative anthropographic boundaries in a hierarchical fashion based on different physical movement ranges of users derived from the collective mobility patterns of Twitter users in Great Britain. The results of strongly connected urban regions in the form of communities in the network space yield geographically cohesive, non-overlapping urban areas, which provide a clear delineation of the non-administrative anthropographic urban boundaries of Great Britain. The method was applied to both national (Great Britain) and municipal scales (the London metropolis). While our results corresponded well with the administrative boundaries, many unexpected and interesting boundaries were identified. Importantly, as the depicted urban boundaries exhibited a strong instance of spatial proximity, we employed a gravity model to understand the distance decay effects in shaping the delineated urban boundaries. The model explains how geographical distances found in the mobility patterns affect the interaction intensity among different non-administrative anthropographic urban areas, which provides new insights into human spatial interactions with urban space.
High-Mobility OFDM Downlink Transmission with Large-Scale Antenna Array
Venue: arXiv cs.IT 2017
Year: 2017

In this correspondence, we propose a new receiver design for high-mobility orthogonal frequency division multiplexing (OFDM) downlink transmissions with a large-scale antenna array. The downlink signal experiences the challenging fast time-varying propagation channel. The time-varying nature originates from the multiple carrier frequency offsets (CFOs) due to the transceiver oscillator frequency offset (OFO) and multiple Doppler shifts. Let the received signal first go through a carefully designed beamforming network, which could separate multiple CFOs in the spatial domain with sufficient number of receive antennas. A joint estimation method for the Doppler shifts and the OFO is further developed. Then the conventional single-CFO compensation and channel estimation method can be carried out for each beamforming branch. The proposed receiver design avoids the complicated time-varying channel estimation, which differs a lot from the conventional methods. More importantly, the proposed scheme can be applied to the commonly used time-varying channel models, such as the Jakes' channel model.
Prior matters: simple and general methods for evaluating and improving topic quality in topic modeling
Venue: arXiv cs.CL 2017
Year: 2017

Latent Dirichlet Allocation (LDA) models trained without stopword removal often produce topics with high posterior probabilities on uninformative words, obscuring the underlying corpus content. Even when canonical stopwords are manually removed, uninformative words common in that corpus will still dominate the most probable words in a topic. In this work, we first show how the standard topic quality measures of coherence and pointwise mutual information act counter-intuitively in the presence of common but irrelevant words, making it difficult to even quantitatively identify situations in which topics may be dominated by stopwords. We propose an additional topic quality metric that targets the stopword problem, and show that it, unlike the standard measures, correctly correlates with human judgements of quality. We also propose a simple-to-implement strategy for generating topics that are evaluated to be of much higher quality by both human assessment and our new metric. This approach, a collection of informative priors easily introduced into most LDA-style inference methods, automatically promotes terms with domain relevance and demotes domain-specific stop words. We demonstrate this approach's effectiveness in three very different domains: Department of Labor accident reports, online health forum posts, and NIPS abstracts. Overall we find that current practices thought to solve this problem do not do so adequately, and that our proposal offers a substantial improvement for those interested in interpreting their topics as objects in their own right.
Error modeling for surrogates of dynamical systems using machine learning
Venue: arXiv cs.NA 2017
Year: 2017

A machine-learning-based framework for modeling the error introduced by surrogate models of parameterized dynamical systems is proposed. The framework entails the use of high-dimensional regression techniques (e.g., random forests, LASSO) to map a large set of inexpensively computed `error indicators' (i.e., features) produced by the surrogate model at a given time instance to a prediction of the surrogate-model error in a quantity of interest (QoI). This eliminates the need for the user to hand-select a small number of informative features. The methodology requires a training set of parameter instances at which the time-dependent surrogate-model error is computed by simulating both the high-fidelity and surrogate models. Using these training data, the method first determines regression-model locality (via classification or clustering), and subsequently constructs a `local' regression model to predict the time-instantaneous error within each identified region of feature space. We consider two uses for the resulting error model: (1) as a correction to the surrogate-model QoI prediction at each time instance, and (2) as a way to statistically model arbitrary functions of the time-dependent surrogate-model error (e.g., time-integrated errors). We apply the proposed framework to model errors in reduced-order models of nonlinear oil--water subsurface flow simulations. The reduced-order models used in this work entail application of trajectory piecewise linearization with proper orthogonal decomposition. When the first use of the method is considered, numerical experiments demonstrate consistent improvement in accuracy in the time-instantaneous QoI prediction relative to the original surrogate model, across a large number of test cases. When the second use is considered, results show that the proposed method provides accurate statistical predictions of the time- and well-averaged errors.
Log-based Anomaly Detection of CPS Using a Statistical Method
Venue: arXiv cs.SE 2017
Year: 2017

Detecting anomalies of a cyber physical system (CPS), which is a complex system consisting of both physical and software parts, is important because a CPS often operates autonomously in an unpredictable environment. However, because of the ever-changing nature and lack of a precise model for a CPS, detecting anomalies is still a challenging task. To address this problem, we propose applying an outlier detection method to a CPS log. By using a log obtained from an actual aquarium management system, we evaluated the effectiveness of our proposed method by analyzing outliers that it detected. By investigating the outliers with the developer of the system, we confirmed that some outliers indicate actual faults in the system. For example, our method detected failures of mutual exclusion in the control system that were unknown to the developer. Our method also detected transient losses of functionalities and unexpected reboots. On the other hand, our method did not detect anomalies that were too many and similar. In addition, our method reported rare but unproblematic concurrent combinations of operations as anomalies. Thus, our approach is effective at finding anomalies, but there is still room for improvement.
On the Complexity of L-reachability
Venue: arXiv cs.CC 2017
Year: 2017

We initiate a complexity theoretic study of the language based graph reachability problem (L-REACH) : Fix a language L. Given a graph whose edges are labeled with alphabet symbols of the language L and two special vertices s and t, test if there is path P from s to t in the graph such that the concatenation of the symbols seen from s to t in the path P forms a string in the language L. We study variants of this problem with different graph classes and different language classes and obtain complexity theoretic characterizations for all of them. Our main results are the following: 1.Restricting the language using formal language theory we show that the complexity of L-REACH increases with the power of the formal language class. We show that there is a regular language for which the L-REACH is NL-complete even for undirected graphs. In the case of linear languages, the complexity of L-REACH does not go beyond the complexity of L itself. Further, there is a deterministic context-free language L for which L-DAGREACH is LogCFL-complete. 2.We use L-REACH as a lens to study structural complexity. In this direction we show that there is a language A in TC0 for which A-DAGREACH is NP-complete. Using this we show that P vs NP question is equivalent to P vs DAGREACH-1(P) question. This leads to the intriguing possibility that by proving DAGREACH-1(P) is contained in some subclass of P, we can prove an upward translation of separation of complexity classes. Note that we do not know a way to upward translate the separation of complexity classes.
An EPTAS for Scheduling on Unrelated Machines of Few Different Types
Venue: arXiv cs.DS 2017
Year: 2017

In the classical problem of scheduling on unrelated parallel machines, a set of jobs has to be assigned to a set of machines. The jobs have a processing time depending on the machine and the goal is to minimize the makespan, that is the maximum machine load. It is well known that this problem is NP-hard and does not allow polynomial time approximation algorithms with approximation guarantees smaller than $1.5$ unless P$=$NP. We consider the case that there are only a constant number $K$ of machine types. Two machines have the same type if all jobs have the same processing time for them. This variant of the problem is strongly NP-hard already for $K=1$. We present an efficient polynomial time approximation scheme (EPTAS) for the problem, that is, for any $\varepsilon > 0$ an assignment with makespan of length at most $(1+\varepsilon)$ times the optimum can be found in polynomial time in the input length and the exponent is independent of $1/\varepsilon$. In particular we achieve a running time of $2^{\mathcal{O}(K\log(K) \frac{1}{\varepsilon}\log^4 \frac{1}{\varepsilon})}+\mathrm{poly}(|I|)$, where $|I|$ denotes the input length. Furthermore, we study three other problem variants and present an EPTAS for each of them: The Santa Claus problem, where the minimum machine load has to be maximized; the case of scheduling on unrelated parallel machines with a constant number of uniform types, where machines of the same type behave like uniformly related machines; and the multidimensional vector scheduling variant of the problem where both the dimension and the number of machine types are constant. For the Santa Claus problem we achieve the same running time. The results are achieved, using mixed integer linear programming and rounding techniques.