OpenRaiser/Intern-Atlas huggingface dataset:
An Energy-aware Mutation Testing Framework for EAST-ADL Architectural Models
Venue: arXiv cs.SE 2018
Year: 2018

Early design artifacts of embedded systems, such as architectural models, represent convenient abstractions for reasoning about a system's structure and functionality. One such example is the Electronic Architecture and Software Tools-Architecture Description Language (EAST-ADL), a domain-specific architectural language that targets the automotive industry. EAST-ADL is used to represent both hardware and software elements, as well as related extra-functional information (e.g., timing properties, triggering information, resource consumption). Testing architectural models is an important activity in engineering large-scale industrial systems, which sparks a growing research interest. The main contributions of this paper are: (i) an approach for creating energy-related mutants for EAST-ADL architectural models, (ii) a method for overcoming the equivalent mutant problem (i.e., the problem of finding a test case which can distinguish the observable behavior of a mutant from the original one), (iii) a test generation approach based on UPPAAL Statistical Model Checker (SMC), and (iv) a test selection criteria based on mutation analysis using our MATS tool.
Desingularization of First Order Linear Difference Systems with Rational Function Coefficients
Venue: arXiv cs.SC 2018
Year: 2018

It is well known that for a first order system of linear difference equations with rational function coefficients, a solution that is holomorphic in some left half plane can be analytically continued to a meromorphic solution in the whole complex plane. The poles stem from the singularities of the rational function coefficients of the system. Just as for differential equations, not all of these singularities necessarily lead to poles in solutions, as they might be what is called removable. In our work, we show how to detect and remove these singularities and further study the connection between poles of solutions and removable singularities. We describe two algorithms to (partially) desingularize a given difference system and present a characterization of removable singularities in terms of shifts of the original system.
Channel Model of Molecular Communication via Diffusion in a Vessel-like Environment Considering a Partially Covering Receiver
Venue: arXiv cs.ET 2018
Year: 2018

By considering potential health problems that a fully covering receiver may cause in vessel-like environments, the implementation of a partially covering receiver is needed. To this end, distribution of hitting location of messenger molecules (MM) is analyzed within the context of molecular communication via diffusion with the aim of channel modeling. The distribution of these MMs for a fully covering receiver is analyzed in two parts: angular and radial dimensions. For the angular distribution analysis, the receiver is divided into 180 slices to analyze the mean, standard deviation, and coefficient of variation of these slices. For the axial distance distribution analysis, Kolmogorov- Smirnov test is applied for different significance levels. Also, two different implementations of the reflection from the vessel surface (i.e., rollback and elastic reflection) are compared and mathematical representation of elastic reflection is given. The results show that MMs have tendency to spread uniformly beyond a certain ratio of the distance to the vessel radius. By utilizing the uniformity, we propose a channel model for the partially covering receiver in vessel-like environments and validate the proposed model by simulations.
Development of c-means Clustering Based Adaptive Fuzzy Controller for A Flapping Wing Micro Air Vehicle
Venue: arXiv cs.SY 2018
Year: 2018

Advanced and accurate modelling of a Flapping Wing Micro Air Vehicle (FW MAV) and its control is one of the recent research topics related to the field of autonomous Unmanned Aerial Vehicles (UAVs). In this work, a four wing Natureinspired (NI) FW MAV is modeled and controlled inspiring by its advanced features like quick flight, vertical take-off and landing, hovering, and fast turn, and enhanced manoeuvrability when contrasted with comparable-sized fixed and rotary wing UAVs. The Fuzzy C-Means (FCM) clustering algorithm is utilized to demonstrate the NIFW MAV model, which has points of interest over first principle based modelling since it does not depend on the system dynamics, rather based on data and can incorporate various uncertainties like sensor error. The same clustering strategy is used to develop an adaptive fuzzy controller. The controller is then utilized to control the altitude of the NIFW MAV, that can adapt with environmental disturbances by tuning the antecedent and consequent parameters of the fuzzy system.
ClassSim: Similarity between Classes Defined by Misclassification Ratios of Trained Classifiers
Venue: arXiv cs.CV 2018
Year: 2018

Deep neural networks (DNNs) have achieved exceptional performances in many tasks, particularly, in supervised classification tasks. However, achievements with supervised classification tasks are based on large datasets with well-separated classes. Typically, real-world applications involve wild datasets that include similar classes; thus, evaluating similarities between classes and understanding relations among classes are important. To address this issue, a similarity metric, ClassSim, based on the misclassification ratios of trained DNNs is proposed herein. We conducted image recognition experiments to demonstrate that the proposed method provides better similarities compared with existing methods and is useful for classification problems. Source code including all experimental results is available at https://github.com/karino2/ClassSim/.
Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle
Venue: arXiv cs.LO 2018
Year: 2018

We present a framework in Isabelle for verifying asymptotic time complexity of imperative programs. We build upon an extension of Imperative HOL and its separation logic to include running time. In addition to the basic arguments, our framework is able to handle advanced techniques for time complexity analysis, such as the use of the Akra-Bazzi theorem and amortized analysis. Various automation is built and incorporated into the auto2 prover to reason about separation logic with time credits, and to derive asymptotic behavior of functions. As case studies, we verify the asymptotic time complexity (in addition to functional correctness) of imperative algorithms and data structures such as median of medians selection, Karatsuba's algorithm, and splay trees.
Continuous-Domain Solutions of Linear Inverse Problems with Tikhonov vs. Generalized TV Regularization
Venue: arXiv cs.IT 2018
Year: 2018

We consider linear inverse problems that are formulated in the continuous domain. The object of recovery is a function that is assumed to minimize a convex objective functional. The solutions are constrained by imposing a continuous-domain regularization. We derive the parametric form of the solution (representer theorems) for Tikhonov (quadratic) and generalized total-variation (gTV) regularizations. We show that, in both cases, the solutions are splines that are intimately related to the regularization operator. In the Tikhonov case, the solution is smooth and constrained to live in a fixed subspace that depends on the measurement operator. By contrast, the gTV regularization results in a sparse solution composed of only a few dictionary elements that are upper-bounded by the number of measurements and independent of the measurement operator. Our findings for the gTV regularization resonates with the minimization of the $l_1$ norm, which is its discrete counterpart and also produces sparse solutions. Finally, we find the experimental solutions for some measurement models in one dimension. We discuss the special case when the gTV regularization results in multiple solutions and devise an algorithm to find an extreme point of the solution set which is guaranteed to be sparse.
DP-GAN: Diversity-Promoting Generative Adversarial Network for Generating Informative and Diversified Text
Venue: arXiv cs.CL 2018
Year: 2018

Existing text generation methods tend to produce repeated and "boring" expressions. To tackle this problem, we propose a new text generation model, called Diversity-Promoting Generative Adversarial Network (DP-GAN). The proposed model assigns low reward for repeatedly generated text and high reward for "novel" and fluent text, encouraging the generator to produce diverse and informative text. Moreover, we propose a novel language-model based discriminator, which can better distinguish novel text from repeated text without the saturation problem compared with existing classifier-based discriminators. The experimental results on review generation and dialogue generation tasks demonstrate that our model can generate substantially more diverse and informative text than existing baselines. The code is available at https://github.com/lancopku/DPGAN
Randomness and isometries in echo state networks and compressed sensing
Venue: arXiv cs.IT 2018
Year: 2018

Although largely different concepts, echo state networks and compressed sensing models both rely on collections of random weights; as the reservoir dynamics for echo state networks, and the sensing coefficients in compressed sensing. Several methods for generating the random matrices and metrics to indicate desirable performance are well-studied in compressed sensing, but less so for echo state networks. This work explores any overlap in these compressed sensing methods and metrics for application to echo state networks. Several methods for generating the random reservoir weights are considered, and a new metric, inspired by the restricted isometry property for compressed sensing, is proposed for echo state networks. The methods and metrics are investigated theoretically and experimentally, with results suggesting that the same types of random matrices work well for both echo state network and compressed sensing scenarios, and that echo state network classification accuracy is improved when the proposed restricted isometry-like constants are close to 1.
SDN based Control and Management of WLANs in the 3GPP 5G Network
Venue: arXiv cs.NI 2018
Year: 2018

The exponential growth in mobile broadband usage [1] has catalyzed the need for high data rate communication systems. In this regard, activities for standardizing the next generation mobile broadband system, known as the Fifth Generation(5G) system are underway. The 5G system also enables the integration of Institute of Electrical and Electronic Engineers (IEEE) Wireless Local Area Networks (WLANs) for providing cost-effective broadband connectivity. It is therefore imperative to find solutions for control and management of WLANs, while providing seamless inter-working capabilities with the cellular network. In this paper, we propose a novel Software Defined Networking (SDN) based architecture for efficient control and management of IEEE WLANs while providing a mechanism for smooth integration of WLANs within the 5G system.
An efficient counting method for the colored triad census
Venue: arXiv cs.DS 2018
Year: 2018

The triad census is an important approach to understand local structure in network science, providing comprehensive assessments of the observed relational configurations between triples of actors in a network. However, researchers are often interested in combinations of relational and categorical nodal attributes. In this case, it is desirable to account for the label, or color, of the nodes in the triad census. In this paper, we describe an efficient algorithm for constructing the colored triad census, based, in part, on existing methods for the classic triad census. We evaluate the performance of the algorithm using empirical and simulated data for both undirected and directed graphs. The results of the simulation demonstrate that the proposed algorithm reduces computational time many-fold over the naive approach. We also apply the colored triad census to the Zachary karate club network dataset. We simultaneously show the efficiency of the algorithm, and a way to conduct a statistical test on the census by forming a null distribution from 1,000 realizations of a mixing-matrix conditioned graph and comparing the observed colored triad counts to the expected. From this, we demonstrate the method's utility in our discussion of results about homophily, heterophily, and bridging, simultaneously gained via the colored triad census. In sum, the proposed algorithm for the colored triad census brings novel utility to social network analysis in an efficient package.
Shoulder Physiotherapy Exercise Recognition: Machine Learning the Inertial Signals from a Smartwatch
Venue: arXiv cs.HC 2018
Year: 2018

Objective: Participation in a physical therapy program is considered one of the greatest predictors of successful conservative management of common shoulder disorders. However, adherence to these protocols is often poor and typically worse for unsupervised home exercise programs. Currently, there are limited tools available for objective measurement of adherence in the home setting. The goal of this study was to develop and evaluate the potential for performing home shoulder physiotherapy monitoring using a commercial smartwatch. Approach: Twenty healthy adult subjects with no prior shoulder disorders performed seven exercises from an evidence-based rotator cuff physiotherapy protocol, while 6-axis inertial sensor data was collected from the active extremity. Within an activity recognition chain (ARC) framework, four supervised learning algorithms were trained and optimized to classify the exercises: k-nearest neighbor (k-NN), random forest (RF), support vector machine classifier (SVC), and a convolutional recurrent neural network (CRNN). Algorithm performance was evaluated using 5-fold cross-validation stratified first temporally and then by subject. Main Results: Categorical classification accuracy was above 94% for all algorithms on the temporally stratified cross validation, with the best performance achieved by the CRNN algorithm (99.4%). The subject stratified cross validation, which evaluated classifier performance on unseen subjects, yielded lower accuracies scores again with CRNN performing best (88.9%). Significance: This proof of concept study demonstrates the technical feasibility of a smartwatch device and supervised machine learning approach to more easily monitor and assess the at-home adherence of shoulder physiotherapy exercise protocols.
Analysing the Degree of Meshing in Medium Voltage Target Grids - An Automated Technical and Economical Impact Assessment
Venue: arXiv cs.CE 2018
Year: 2018

There are different MV grid concepts with regard to mode of operation and protection system layout. The increasing installation of DG raises the question if the currently used concepts are still optimal for future power systems. We present a methodology that allows the automated calculation and comparison of target grids within different concepts. Specifically, we consider radial grids, closed ring grids and grids with switching stations. A target grid structure is optimized for each of those grid concepts based on geographical information. To model a realistic planning process, compliance with technical constraints for normal operation, contingency behaviour and reliability figures are ensured in all grid concepts. We present a multiphase approach to solve the optimization problem based on an iterated local search meta-heuristic. We then economically compare the grids with regards to CAPEX and OPEX for primary and secondary equipment, to analyse which concept leads to the most overall cost-efficient target grids. Since the methodology allows an automated evaluation of a large number of grids, it can be used to draw general conclusions about the cost-efficiency of specific concepts. The methodology is applied to 44 real MV grids spanning about 4800km of lines, for which the results show that a radial grid structure is overall cost efficient compared to grid topologies with switching stations or closed rings even in grid areas with a large DG penetration. The contribution of this paper is threefold: first, a comprehensive methodology to compile automated target grid plans under realistic premises is presented. Second, the practical applicability of the approach is demonstrated with a large scale case study with a high degree of automation. And third, the results of the case study allow to draw conclusions about the techno-economical differences of different MV grid concepts.
Guided Policy Exploration for Markov Decision Processes using an Uncertainty-Based Value-of-Information Criterion
Venue: arXiv cs.AI 2018
Year: 2018

Reinforcement learning in environments with many action-state pairs is challenging. At issue is the number of episodes needed to thoroughly search the policy space. Most conventional heuristics address this search problem in a stochastic manner. This can leave large portions of the policy space unvisited during the early training stages. In this paper, we propose an uncertainty-based, information-theoretic approach for performing guided stochastic searches that more effectively cover the policy space. Our approach is based on the value of information, a criterion that provides the optimal trade-off between expected costs and the granularity of the search process. The value of information yields a stochastic routine for choosing actions during learning that can explore the policy space in a coarse to fine manner. We augment this criterion with a state-transition uncertainty factor, which guides the search process into previously unexplored regions of the policy space.
Background subtraction using the factored 3-way restricted Boltzmann machines
Venue: arXiv cs.CV 2018
Year: 2018

In this paper, we proposed a method for reconstructing the 3D model based on continuous sensory input. The robot can draw on extremely large data from the real world using various sensors. However, the sensory inputs are usually too noisy and high-dimensional data. It is very difficult and time consuming for robot to process using such raw data when the robot tries to construct 3D model. Hence, there needs to be a method that can extract useful information from such sensory inputs. To address this problem our method utilizes the concept of Object Semantic Hierarchy (OSH). Different from the previous work that used this hierarchy framework, we extract the motion information using the Deep Belief Network technique instead of applying classical computer vision approaches. We have trained on two large sets of random dot images (10,000) which are translated and rotated, respectively, and have successfully extracted several bases that explain the translation and rotation motion. Based on this translation and rotation bases, background subtraction have become possible using Object Semantic Hierarchy.
Learning from Richer Human Guidance: Augmenting Comparison-Based Learning with Feature Queries
Venue: arXiv cs.AI 2018
Year: 2018

We focus on learning the desired objective function for a robot. Although trajectory demonstrations can be very informative of the desired objective, they can also be difficult for users to provide. Answers to comparison queries, asking which of two trajectories is preferable, are much easier for users, and have emerged as an effective alternative. Unfortunately, comparisons are far less informative. We propose that there is much richer information that users can easily provide and that robots ought to leverage. We focus on augmenting comparisons with feature queries, and introduce a unified formalism for treating all answers as observations about the true desired reward. We derive an active query selection algorithm, and test these queries in simulation and on real users. We find that richer, feature-augmented queries can extract more information faster, leading to robots that better match user preferences in their behavior.
Multiplex Influence Maximization in Online Social Networks with Heterogeneous Diffusion Models
Venue: arXiv cs.SI 2018
Year: 2018

Motivated by online social networks that are linked together through overlapping users, we study the influence maximization problem on a multiplex, with each layer endowed with its own model of influence diffusion. This problem is a novel version of the influence maximization problem that necessitates new analysis incorporating the type of propagation on each layer of the multiplex. We identify a new property, generalized deterministic submodular, which when satisfied by the propagation in each layer, ensures that the propagation on the multiplex overall is submodular -- for this case, we formulate ISF, the greedy algorithm with approximation ratio $(1 - 1/e)$. Since the size of a multiplex comprising multiple OSNs may encompass billions of users, we formulate an algorithm KSN that runs on each layer of the multiplex in parallel. KSN takes an $α$-approximation algorithm A for the influence maximization problem on a single-layer network as input, and has approximation ratio $\frac{(1-ε)α}{(o+1)k}$ for arbitrary $ε> 0$, $o$ is the number of overlapping users, and $k$ is the number of layers in the multiplex. Experiments on real and synthesized multiplexes validate the efficacy of the proposed algorithms for the problem of influence maximization in the heterogeneous multiplex. Implementations of ISF and KSN are available at http://www.alankuhnle.com/papers/mim/mim.html.
Formal Verification of Spacecraft Control Programs Using a Metalanguage for State Transformers
Venue: arXiv cs.PL 2018
Year: 2018

Verification of functional correctness of control programs is an essential task for the development of space electronics; it is difficult and time-consuming and typically outweighs design and programming tasks in terms of development hours. We present a verification approach designed to help spacecraft engineers reduce the effort required for formal verification of low-level control programs executed on custom hardware. The approach uses a metalanguage to describe the semantics of a program as a state transformer, which can be compiled to multiple targets for testing, formal verification, and code generation. The metalanguage itself is embedded in a strongly-typed host language (Haskell), providing a way to prove program properties at the type level, which can shorten the feedback loop and further increase the productivity of engineers. The verification approach is demonstrated on an industrial case study. We present REDFIN, a processing core used in space missions, and its formal semantics expressed using the proposed metalanguage, followed by a detailed example of verification of a simple control program.
Question-Answer Selection in User to User Marketplace Conversations
Venue: arXiv cs.CL 2018
Year: 2018

Sellers in user to user marketplaces can be inundated with questions from potential buyers. Answers are often already available in the product description. We collected a dataset of around 590K such questions and answers from conversations in an online marketplace. We propose a question answering system that selects a sentence from the product description using a neural-network ranking model. We explore multiple encoding strategies, with recurrent neural networks and feed-forward attention layers yielding good results. This paper presents a demo to interactively pose buyer questions and visualize the ranking scores of product description sentences from live online listings.