OpenRaiser/Intern-Atlas huggingface dataset:
Observer Based Path Following for Underactuated Marine Vessels in the Presence of Ocean Currents: A Local Approach - With proofs
Venue: arXiv cs.SY 2017
Year: 2017

In this article a solution to the problem of following a curved path in the presence of a constant unknown ocean current disturbance is presented. The path is parametrised by a path variable that is used to propagate a path-tangential reference frame. The update law for the path variable is chosen such that the motion of the path-tangential frame ensures that the vessel remains on the normal of the path-tangential reference frame. As shown in the seminal work [20] such a parametrisation is only possible locally. A tube is defined in which the aforementioned parametrisation is valid and the path-following problem is solved within this tube. The size of the tube is proportional to the maximum curvature of the path. It is shown that within this tube, the closed-loop system of the proposed controller, guidance law, and the ocean current observer provides exponential stability of the path-following error dynamics. The sway velocity dynamics are analysed taking into account couplings previously overlooked in the literature, and is shown to remain bounded. Simulation results are presented.
$α$Check: A mechanized metatheory model-checker
Venue: arXiv cs.PL 2017
Year: 2017

The problem of mechanically formalizing and proving metatheoretic properties of programming language calculi, type systems, operational semantics, and related formal systems has received considerable attention recently. However, the dual problem of searching for errors in such formalizations has attracted comparatively little attention. In this article, we present $α$Check, a bounded model-checker for metatheoretic properties of formal systems specified using nominal logic. In contrast to the current state of the art for metatheory verification, our approach is fully automatic, does not require expertise in theorem proving on the part of the user, and produces counterexamples in the case that a flaw is detected. We present two implementations of this technique, one based on negation-as-failure and one based on negation elimination, along with experimental results showing that these techniques are fast enough to be used interactively to debug systems as they are developed.
Wireless Health Monitoring using Passive WiFi Sensing
Venue: arXiv cs.OH 2017
Year: 2017

This paper presents a two-dimensional phase extraction system using passive WiFi sensing to monitor three basic elderly care activities including breathing rate, essential tremor and falls. Specifically, a WiFi signal is acquired through two channels where the first channel is the reference one, whereas the other signal is acquired by a passive receiver after reflection from the human target. Using signal processing of cross-ambiguity function, various features in the signal are extracted. The entire implementations are performed using software defined radios having directional antennas. We report the accuracy of our system in different conditions and environments and show that breathing rate can be measured with an accuracy of 87% when there are no obstacles. We also show a 98% accuracy in detecting falls and 93% accuracy in classifying tremor. The results indicate that passive WiFi systems show great promise in replacing typical invasive health devices as standard tools for health care.
Detection of Copy-move Image forgery using SVD and Cuckoo Search Algorithm
Venue: arXiv cs.MM 2017
Year: 2017

Copy-move forgery is one of the simple and effective operations to create forged images. Recently, techniques based on singular value decomposition (SVD) are widely used to detect copy-move forgery (CMF). Some approaches based on SVD are most acceptable to detect copy-move forgery but some copy-move forgery detection approaches can not produce satisfactory detection results. Sometimes these approaches may even produce error results. According to our observation, detection result produced using SVD depend highly on those parameters whose values are often determined with experiences. These values are only applicable to a few images, which limit their application. To solve this problem, a novel approach named as copy-move forgery detection using Cuckoo search algorithm (CMFD-CS) is proposed in this paper. CMFD-CS integrates the CS algorithm into SVD. It utilizes the CS algorithm to generate customized parameter values for images, which are used CMFD under block-based framework.
A survey on pseudonym changing strategies for Vehicular Ad-Hoc Networks
Venue: arXiv cs.CR 2017
Year: 2017

The initial phase of the deployment of Vehicular Ad-Hoc Networks (VANETs) has begun and many research challenges still need to be addressed. Location privacy continues to be in the top of these challenges. Indeed, both of academia and industry agreed to apply the pseudonym changing approach as a solution to protect the location privacy of VANETs'users. However, due to the pseudonyms linking attack, a simple changing of pseudonym shown to be inefficient to provide the required protection. For this reason, many pseudonym changing strategies have been suggested to provide an effective pseudonym changing. Unfortunately, the development of an effective pseudonym changing strategy for VANETs is still an open issue. In this paper, we present a comprehensive survey and classification of pseudonym changing strategies. We then discuss and compare them with respect to some relevant criteria. Finally, we highlight some current researches, and open issues and give some future directions.
Convolutional Polar Codes
Venue: arXiv cs.IT 2017
Year: 2017

Arikan's Polar codes attracted much attention as the first efficiently decodable and capacity achieving codes. Furthermore, Polar codes exhibit an exponentially decreasing block error probability with an asymptotic error exponent upper bounded by 1/2. Since their discovery, many attempts have been made to improve the error exponent and the finite block-length performance, while keeping the bloc-structured kernel. Recently, two of us introduced a new family of efficiently decodable error-correction codes based on a recently discovered efficiently-contractible tensor network family in quantum many-body physics, called branching MERA. These codes, called branching MERA codes, include Polar codes and also extend them in a non-trivial way by substituting the bloc-structured kernel by a convolutional structure. Here, we perform an in-depth study of a particular example that can be thought of as a direct extension to Arikan's Polar code, which we therefore name Convolutional Polar codes. We prove that these codes polarize and exponentially suppress the channel's error probability, with an asymptotic error exponent log_2(3)/2 which is provably better than for Polar codes under successive cancellation decoding. We also perform finite block-size numerical simulations which display improved error-correcting capability with only a minor impact on decoding complexity.
Studying the Prevalence of Exception Handling Anti-Patterns
Venue: arXiv cs.SE 2017
Year: 2017

Modern programming languages, such as Java and C#, typically provide features that handle exceptions. These features separate error-handling code from regular source code and are proven to enhance the practice of software reliability, comprehension, and maintenance. Having acknowledged the advantages of exception handling features, the misuse of them can still cause catastrophic software failures, such as application crash. Prior studies suggested anti-patterns of exception handling; while little knowledge was shared about the prevalence of these anti-patterns. In this paper, we investigate the prevalence of exception-handling anti-patterns. We collected a thorough list of exception anti-patterns from 16 open-source Java and C# libraries and applications using an automated exception flow analysis tool. We found that although exception handling anti- patterns widely exist in all of our subjects, only a few anti- patterns (e.g. Unhandled Exceptions, Catch Generic, Unreachable Handler, Over-catch, and Destructive Wrapping) can be commonly identified. On the other hand, we find that the prevalence of anti- patterns illustrates differences between C# and Java. Our results call for further in-depth analyses on the exception handling practices across different languages.
Guided Proofreading of Automatic Segmentations for Connectomics
Venue: arXiv cs.CV 2017
Year: 2017

Automatic cell image segmentation methods in connectomics produce merge and split errors, which require correction through proofreading. Previous research has identified the visual search for these errors as the bottleneck in interactive proofreading. To aid error correction, we develop two classifiers that automatically recommend candidate merges and splits to the user. These classifiers use a convolutional neural network (CNN) that has been trained with errors in automatic segmentations against expert-labeled ground truth. Our classifiers detect potentially-erroneous regions by considering a large context region around a segmentation boundary. Corrections can then be performed by a user with yes/no decisions, which reduces variation of information 7.5x faster than previous proofreading methods. We also present a fully-automatic mode that uses a probability threshold to make merge/split decisions. Extensive experiments using the automatic approach and comparing performance of novice and expert users demonstrate that our method performs favorably against state-of-the-art proofreading methods on different connectomics datasets.
On the Estimation and Control of Human Body Composition
Venue: arXiv cs.SY 2017
Year: 2017

Obesity is a chronic disease that can lead to an increased risk of other serious chronic diseases and even death. We present switching and time-delayed feedback-based model free control methods for the dynamic management of body mass and its major components. The estimation of body composition based on human body weight dynamics is proposed using a soft switching-based observer. Additionally, this paper addresses the control allocation problem for optimal body weight management using linear algebraic equivalence of the nonlinear controllers based on dynamic behavior of body composition described in literature. A control allocator system computes the required energy intake and energy expenditure from a controlling range of inputs to track a desired trajectory of body mass by optimizing a weighted quadratic function. Simulation results validate the performance of the proposed controllers and the observer under disturbances in recording energy intake and energy expenditure figures.
High-Speed Trajectory Planning for Autonomous Vehicles Using a Simple Dynamic Model
Venue: arXiv cs.SY 2017
Year: 2017

To improve safety and energy efficiency, autonomous vehicles are expected to drive smoothly in most situations, while maintaining their velocity below a predetermined speed limit. However, some scenarios such as low road adherence or inadequate speed limit may require vehicles to automatically adapt their velocity without external input, while nearing the limits of their dynamic capacities. Many of the existing trajectory planning approaches are incapable of making such adjustments, since they assume a feasible velocity reference is given. Moreover, near-limits trajectory planning often implies high-complexity dynamic vehicle models, making computations difficult. In this article, we use a simple dynamic model derived from numerical simulations to design a trajectory planner for high-speed driving of an autonomous vehicle based on model predictive control. Unlike existing techniques, our formulation includes the selection of a feasible velocity to track a predetermined path while avoiding obstacles. Simulation results on a highly precise vehicle model show that our approach can be used in real-time to provide feasible trajectories that can be tracked using a simple control architecture. Moreover, the use of our simplified model makes the planner more robust and yields better trajectories compared to kinematic models commonly used in trajectory planning.
Homotopy Parametric Simplex Method for Sparse Learning
Venue: arXiv cs.LG 2017
Year: 2017

High dimensional sparse learning has imposed a great computational challenge to large scale data analysis. In this paper, we are interested in a broad class of sparse learning approaches formulated as linear programs parametrized by a {\em regularization factor}, and solve them by the parametric simplex method (PSM). Our parametric simplex method offers significant advantages over other competing methods: (1) PSM naturally obtains the complete solution path for all values of the regularization parameter; (2) PSM provides a high precision dual certificate stopping criterion; (3) PSM yields sparse solutions through very few iterations, and the solution sparsity significantly reduces the computational cost per iteration. Particularly, we demonstrate the superiority of PSM over various sparse learning approaches, including Dantzig selector for sparse linear regression, LAD-Lasso for sparse robust linear regression, CLIME for sparse precision matrix estimation, sparse differential network estimation, and sparse Linear Programming Discriminant (LPD) analysis. We then provide sufficient conditions under which PSM always outputs sparse solutions such that its computational performance can be significantly boosted. Thorough numerical experiments are provided to demonstrate the outstanding performance of the PSM method.
Probabilistic Search for Structured Data via Probabilistic Programming and Nonparametric Bayes
Venue: arXiv cs.AI 2017
Year: 2017

Databases are widespread, yet extracting relevant data can be difficult. Without substantial domain knowledge, multivariate search queries often return sparse or uninformative results. This paper introduces an approach for searching structured data based on probabilistic programming and nonparametric Bayes. Users specify queries in a probabilistic language that combines standard SQL database search operators with an information theoretic ranking function called predictive relevance. Predictive relevance can be calculated by a fast sparse matrix algorithm based on posterior samples from CrossCat, a nonparametric Bayesian model for high-dimensional, heterogeneously-typed data tables. The result is a flexible search technique that applies to a broad class of information retrieval problems, which we integrate into BayesDB, a probabilistic programming platform for probabilistic data analysis. This paper demonstrates applications to databases of US colleges, global macroeconomic indicators of public health, and classic cars. We found that human evaluators often prefer the results from probabilistic search to results from a standard baseline.
A study of posture judgement on vehicles using wearable acceleration sensor
Venue: arXiv cs.CY 2017
Year: 2017

We study methods to estimate drivers' posture in vehicles using acceleration data of wearable sensor and conduct field tests. To prevent fatal accidents, demands for safety management of bus and taxi are high. However, acceleration of vehicles is added to wearable sensor in vehicles. Therefore, we study methods to estimate driving posture using acceleration data acquired from shirt type wearable sensor hitoe and conduct field tests.
Finite Sample Analyses for TD(0) with Function Approximation
Venue: arXiv cs.AI 2017
Year: 2017

TD(0) is one of the most commonly used algorithms in reinforcement learning. Despite this, there is no existing finite sample analysis for TD(0) with function approximation, even for the linear case. Our work is the first to provide such results. Existing convergence rates for Temporal Difference (TD) methods apply only to somewhat modified versions, e.g., projected variants or ones where stepsizes depend on unknown problem parameters. Our analyses obviate these artificial alterations by exploiting strong properties of TD(0). We provide convergence rates both in expectation and with high-probability. The two are obtained via different approaches that use relatively unknown, recently developed stochastic approximation techniques.
Towards an IT Security Risk Assessment Framework for Railway Automation
Venue: arXiv cs.CR 2017
Year: 2017

Some recent incidents have shown that possibly the vulnerability of IT systems in railway automation has been underestimated. Fortunately, so far, almost only denial-of-service attacks were successful, but due to several trends, such as the use of commercial IT and communication systems or privatization, the threat potential could increase in the near future. However, up to now, no harmonized IT security risk assessment framework for railway automation exists. This paper defines an IT security risk assessment framework which aims to separate IT security and safety requirements as well as certification processes as far as possible. It builds on the well-known safety and approval processes from IEC 62425 and integrates IT security requirements based on the ISA99/IEC62443 standard series. While the detailed results are related to railway automation the general concepts are also applicable to other safety-critical application areas.
The integrality gap of the Goemans--Linial SDP relaxation for Sparsest Cut is at least a constant multiple of $\sqrt{\log n}$
Venue: arXiv cs.DS 2017
Year: 2017

We prove that the integrality gap of the Goemans--Linial semidefinite programming relaxation for the Sparsest Cut Problem is $Ω(\sqrt{\log n})$ on inputs with $n$ vertices.
The adaptive zero-error capacity for a class of channels with noisy feedback
Venue: arXiv cs.IT 2017
Year: 2017

The adaptive zero-error capacity of discrete memoryless channels (DMC) with noiseless feedback has been shown to be positive whenever there exists at least one channel output "disprover", i.e. a channel output that cannot be reached from at least one of the inputs. Furthermore, whenever there exists a disprover, the adaptive zero-error capacity attains the Shannon (small-error) capacity. Here, we study the zero-error capacity of a DMC when the channel feedback is noisy rather than perfect. We show that the adaptive zero-error capacity with noisy feedback is lower bounded by the forward channel's zero-undetected error capacity, and show that under certain conditions this is tight.
Greedy Sampling of Graph Signals
Venue: arXiv cs.IT 2017
Year: 2017

Sampling is a fundamental topic in graph signal processing, having found applications in estimation, clustering, and video compression. In contrast to traditional signal processing, the irregularity of the signal domain makes selecting a sampling set non-trivial and hard to analyze. Indeed, though conditions for graph signal interpolation from noiseless samples exist, they do not lead to a unique sampling set. The presence of noise makes choosing among these sampling sets a hard combinatorial problem. Although greedy sampling schemes are commonly used in practice, they have no performance guarantee. This work takes a twofold approach to address this issue. First, universal performance bounds are derived for the Bayesian estimation of graph signals from noisy samples. In contrast to currently available bounds, they are not restricted to specific sampling schemes and hold for any sampling sets. Second, this paper provides near-optimal guarantees for greedy sampling by introducing the concept of approximate submodularity and updating the classical greedy bound. It then provides explicit bounds on the approximate supermodularity of the interpolation mean-square error showing that it can be optimized with worst-case guarantees using greedy search even though it is not supermodular. Simulations illustrate the derived bound for different graph models and show an application of graph signal sampling to reduce the complexity of kernel principal component analysis.
Relative Learning from Web Images for Content-adaptive Enhancement
Venue: arXiv cs.CV 2017
Year: 2017

Personalized and content-adaptive image enhancement can find many applications in the age of social media and mobile computing. This paper presents a relative-learning-based approach, which, unlike previous methods, does not require matching original and enhanced images for training. This allows the use of massive online photo collections to train a ranking model for improved enhancement. We first propose a multi-level ranking model, which is learned from only relatively-labeled inputs that are automatically crawled. Then we design a novel parameter sampling scheme under this model to generate the desired enhancement parameters for a new image. For evaluation, we first verify the effectiveness and the generalization abilities of our approach, using images that have been enhanced/labeled by experts. Then we carry out subjective tests, which show that users prefer images enhanced by our approach over other existing methods.
Profit Maximization Auction and Data Management in Big Data Markets
Venue: arXiv cs.GT 2017
Year: 2017

A big data service is any data-originated resource that is offered over the Internet. The performance of a big data service depends on the data bought from the data collectors. However, the problem of optimal pricing and data allocation in big data services is not well-studied. In this paper, we propose an auction-based big data market model. We first define the data cost and utility based on the impact of data size on the performance of big data analytics, e.g., machine learning algorithms. The big data services are considered as digital goods and uniquely characterized with "unlimited supply" compared to conventional goods which are limited. We therefore propose a Bayesian profit maximization auction which is truthful, rational, and computationally efficient. The optimal service price and data size are obtained by solving the profit maximization auction. Finally, experimental results on a real-world taxi trip dataset show that our big data market model and auction mechanism effectively solve the profit maximization problem of the service provider.
Proof of a conjecture of Kløve on permutation codes under the Chebychev distance
Venue: arXiv cs.IT 2017
Year: 2017

Let $d$ be a positive integer and $x$ a real number. Let $A_{d, x}$ be a $d\times 2d$ matrix with its entries $$ a_{i,j}=\left\{ \begin{array}{ll} x\ \ & \mbox{for} \ 1\leqslant j\leqslant d+1-i, 1\ \ & \mbox{for} \ d+2-i\leqslant j\leqslant d+i, 0\ \ & \mbox{for} \ d+1+i\leqslant j\leqslant 2d. \end{array} \right. $$ Further, let $R_d$ be a set of sequences of integers as follows: $$R_d=\{(ρ_1, ρ_2,\ldots, ρ_d)|1\leqslant ρ_i\leqslant d+i, 1\leqslant i \leqslant d,\ \mbox{and}\ ρ_r\neq ρ_s\ \mbox{for}\ r\neq s\}.$$ and define $$Ω_d(x)=\sum_{ρ\in R_d}a_{1,ρ_1}a_{2, ρ_2}\ldots a_{d,ρ_d}.$$ In order to give a better bound on the size of spheres of permutation codes under the Chebychev distance, Kløve introduced the above function and conjectured that $$Ω_d(x)=\sum_{m=0}^d{d\choose m}(m+1)^d(x-1)^{d-m}.$$ In this paper, we settle down this conjecture positively.