OpenRaiser/Intern-Atlas huggingface dataset:
Net-Zero Settlement in Distribution Markets
Venue: arXiv cs.SY 2017
Year: 2017

Introduction of market mechanisms in distribution systems is currently subject to extensive studies. One of the challenges facing Distribution Market Operators (DMOs) is to implement a fair and economically efficient pricing mechanism that can incentivize consumers to positively contribute to grid operations and to improve economic performance of the distribution system. This paper studies a penalty-based pricing mechanism in distribution markets and further investigates the interrelationship between the locational marginal prices (LMPs) at transmission and distribution levels. As a result, a closed-form relationship between these LMPs is derived. The possibility of zeroing out the settlement profit is further investigated under the proposed pricing mechanism.
Feature Generation for Robust Semantic Role Labeling
Venue: arXiv cs.CL 2017
Year: 2017

Hand-engineered feature sets are a well understood method for creating robust NLP models, but they require a lot of expertise and effort to create. In this work we describe how to automatically generate rich feature sets from simple units called featlets, requiring less engineering. Using information gain to guide the generation process, we train models which rival the state of the art on two standard Semantic Role Labeling datasets with almost no task or linguistic insight.
Multi-shell Sampling Scheme with Accurate and Efficient Transforms for Diffusion MRI
Venue: arXiv cs.DM 2017
Year: 2017

We propose a multi-shell sampling grid and develop corresponding transforms for the accurate reconstruction of the diffusion signal in diffusion MRI by expansion in the spherical polar Fourier (SPF) basis. The transform is exact in the radial direction and accurate, on the order of machine precision, in the angular direction. The sampling scheme uses an optimal number of samples equal to the degrees of freedom of the diffusion signal in the SPF domain.
Data-Driven Fuzzy Modeling Using Deep Learning
Venue: arXiv cs.SY 2017
Year: 2017

Fuzzy modeling has many advantages over the non-fuzzy methods, such as robustness against uncertainties and less sensitivity to the varying dynamics of nonlinear systems. Data-driven fuzzy modeling needs to extract fuzzy rules from the input/output data, and train the fuzzy parameters. This paper takes advantages from deep learning, probability theory, fuzzy modeling, and extreme learning machines. We use the restricted Boltzmann machine (RBM) and probability theory to overcome some common problems in data based modeling methods. The RBM is modified such that it can be trained with continuous values. A probability based clustering method is proposed to partition the hidden features from the RBM, and extract fuzzy rules with probability measurement. An extreme learning machine and an optimization method are applied to train the consequent part of the fuzzy rules and the probability parameters. The proposed method is validated with two benchmark problems.
Carina: Interactive Million-Node Graph Visualization using Web Browser Technologies
Venue: arXiv cs.HC 2017
Year: 2017

We are working on a scalable, interactive visualization system, called Carina, for people to explore million-node graphs. By using latest web browser technologies, Carina offers fast graph rendering via WebGL, and works across desktop (via Electron) and mobile platforms. Different from most existing graph visualization tools, Carina does not store the full graph in RAM, enabling it to work with graphs with up to 69M edges. We are working to improve and open-source Carina, to offer researchers and practitioners a new, scalable way to explore and visualize large graph datasets.
The Facets of the Bases Polytope of a Matroid and Two Consequences
Venue: arXiv cs.CC 2017
Year: 2017

Let $M$ to be a matroid defined on a finite set $E$ and $L\subset E$. $L$ is locked in $M$ if $M|L$ and $M^*|(E\backslash L)$ are 2-connected, and $min\{r(L), r^*(E\backslash L)\} \geq 2$. In this paper, we prove that the nontrivial facets of the bases polytope of $M$ are described by the locked subsets. We deduce that finding the maximum--weight basis of $M$ is a polynomial time problem for matroids with a polynomial number of locked subsets. This class of matroids is closed under 2-sums and contains the class of uniform matroids, the Vámos matroid and all the excluded minors of 2-sums of uniform matroids. We deduce also a matroid oracle for testing uniformity of matroids after one call of this oracle.
An architecture for non-invasive software measurement
Venue: arXiv cs.SE 2017
Year: 2017

Analysis of data related to software development helps to increase quality, control and predictability of software development processes and products.However, collecting such data for is a complex task. A non-invasive collection of software metrics is one of the most promising approaches to solve the task. In this paper we present an approach which consists of four parts: collect the data, store all collected data, unify the stored data and analyze the data to provide insights to the user about software product or process. We employ the approach to the development of an architecture for non-invasive software measurement system and explain its advantages and limitations.
Stability of Topic Modeling via Matrix Factorization
Venue: arXiv cs.IR 2017
Year: 2017

Topic models can provide us with an insight into the underlying latent structure of a large corpus of documents. A range of methods have been proposed in the literature, including probabilistic topic models and techniques based on matrix factorization. However, in both cases, standard implementations rely on stochastic elements in their initialization phase, which can potentially lead to different results being generated on the same corpus when using the same parameter values. This corresponds to the concept of "instability" which has previously been studied in the context of $k$-means clustering. In many applications of topic modeling, this problem of instability is not considered and topic models are treated as being definitive, even though the results may change considerably if the initialization process is altered. In this paper we demonstrate the inherent instability of popular topic modeling approaches, using a number of new measures to assess stability. To address this issue in the context of matrix factorization for topic modeling, we propose the use of ensemble learning strategies. Based on experiments performed on annotated text corpora, we show that a K-Fold ensemble strategy, combining both ensembles and structured initialization, can significantly reduce instability, while simultaneously yielding more accurate topic models.
First Experiences Optimizing Smith-Waterman on Intel's Knights Landing Processor
Venue: arXiv cs.DC 2017
Year: 2017

The well-known Smith-Waterman (SW) algorithm is the most commonly used method for local sequence alignments. However, SW is very computationally demanding for large protein databases. There exist several implementations that take advantage of computing parallelization on many-cores, FPGAs or GPUs, in order to increase the alignment throughtput. In this paper, we have explored SW acceleration on Intel KNL processor. The novelty of this architecture requires the revision of previous programming and optimization techniques on many-core architectures. To the best of authors knowledge, this is the first KNL architecture assessment for SW algorithm. Our evaluation, using the renowned Environmental NR database as benchmark, has shown that multi-threading and SIMD exploitation reports competitive performance (351 GCUPS) in comparison with other implementations.
On normalization of inconsistency indicators in pairwise comparisons
Venue: arXiv cs.DM 2017
Year: 2017

In this study, we provide mathematical and practice-driven justification for using $[0,1]$ normalization of inconsistency indicators in pairwise comparisons. The need for normalization, as well as problems with the lack of normalization, are presented. A new type of paradox of infinity is described.
$\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
Venue: arXiv cs.LO 2017
Year: 2017

We extend the constructive dependent type theory of the Logical Framework $\mathsf{LF}$ with monadic, dependent type constructors indexed with predicates over judgements, called Locks. These monads capture various possible proof attitudes in establishing the judgment of the object logic encoded by an $\mathsf{LF}$ type. Standard examples are factoring-out the verification of a constraint or delegating it to an external oracle, or supplying some non-apodictic epistemic evidence, or simply discarding the proof witness of a precondition deeming it irrelevant. This new framework, called Lax Logical Framework, $\mathsf{LLF}_{\cal P}$, is a conservative extension of $\mathsf{LF}$, and hence it is the appropriate metalanguage for dealing formally with side-conditions in rules or external evidence in logical systems. $\mathsf{LLF}_{\cal P}$ arises once the monadic nature of the lock type-constructor, ${\cal L}^{\cal P}_{M,σ}[\cdot]$, introduced by the authors in a series of papers, together with Marina Lenisa, is fully exploited. The nature of the lock monads permits to utilize the very Lock destructor, ${\cal U}^{\cal P}_{M,σ}[\cdot]$, in place of Moggi's monadic $let_T$, thus simplifying the equational theory. The rules for ${\cal U}^{\cal P}_{M,σ}[\cdot]$ permit also the removal of the monad once the constraint is satisfied. We derive the meta-theory of $\mathsf{LLF}_{\cal P}$ by a novel indirect method based on the encoding of $\mathsf{LLF}_{\cal P}$ in $\mathsf{LF}$. We discuss encodings in $\mathsf{LLF}_{\cal P}$ of call-by-value $λ$-calculi, Hoare's Logic, and Fitch-Prawitz Naive Set Theory.
GANDALF: A fine-grained hardware-software co-design for preventing memory attacks
Venue: arXiv cs.CR 2017
Year: 2017

Reading or writing outside the bounds of a buffer is a serious security vulnerability that has been exploited in numerous occasions. These attacks can be prevented by ensuring that every buffer is only accessed within its specified bounds. In this paper we present Gandalf, a compiler-assisted hardware extension for the OpenRISC processor that thwarts all forms of memory based attacks including buffer overflows and over-reads.The feature associates lightweight base and bound capabilities to all pointer variables, which are checked at run time by the hardware. Gandalf is transparent to the user and does not require significant OS modifications. Moreover, it achieves locality, thus resulting in small performance penalties.
On the Properties of the Power Systems Nodal Admittance Matrix
Venue: arXiv cs.SY 2017
Year: 2017

This letter provides conditions determining the rank of the nodal admittance matrix, and arbitrary block partitions of it, for connected AC power networks with complex admittances. Furthermore, some implications of these properties concerning Kron Reduction and Hybrid Network Parameters are outlined.
Second order conservative languages with a Maltsev polymorphism also have a majority polymorphism
Venue: arXiv cs.DM 2017
Year: 2017

The paper proves that for any second order conservative constraint language with a Maltsev polymorphism there is a majority polymorphism. Moreover, the majority polymorphism can be defined by the Maltsev polymorphism.
Efficient Simulation of Temperature Evolution of Overhead Transmission Lines Based on Analytical Solution and NWP
Venue: arXiv cs.CE 2017
Year: 2017

Transmission lines are vital components in power systems. Tripping of transmission lines caused by over-temperature is a major threat to the security of system operations, so it is necessary to efficiently simulate line temperature under both normal operation conditions and foreseen fault conditions. Existing methods based on thermal-steady-state analyses cannot reflect transient temperature evolution, and thus cannot provide timing information needed for taking remedial actions. Moreover, conventional numerical method requires huge computational efforts and barricades system-wide analysis. In this regard, this paper derives an approximate analytical solution of transmission-line temperature evolution enabling efficient analysis on multiple operation states. Considering the uncertainties in environmental parameters, the region of over-temperature is constructed in the environmental parameter space to realize the over-temperature risk assessment in both the planning stage and real-time operations. A test on a typical conductor model verifies the accuracy of the approximate analytical solution. Based on the analytical solution and numerical weather prediction (NWP) data, an efficient simulation method for temperature evolution of transmission systems under multiple operation states is proposed. As demonstrated on an NPCC 140-bus system, it achieves over 1000 times of efficiency enhancement, verifying its potentials in online risk assessment and decision support.
Network Construction with Ordered Constraints
Venue: arXiv cs.DS 2017
Year: 2017

In this paper, we study the problem of constructing a network by observing ordered connectivity constraints, which we define herein. These ordered constraints are made to capture realistic properties of real-world problems that are not reflected in previous, more general models. We give hardness of approximation results and nearly-matching upper bounds for the offline problem, and we study the online problem in both general graphs and restricted sub-classes. In the online problem, for general graphs, we give exponentially better upper bounds than exist for algorithms for general connectivity problems. For the restricted classes of stars and paths we are able to find algorithms with optimal competitive ratios, the latter of which involve analysis using a potential function defined over pq-trees.
Delta-net: Real-time Network Verification Using Atoms
Venue: arXiv cs.NI 2017
Year: 2017

Real-time network verification promises to automatically detect violations of network-wide reachability invariants on the data plane. To be useful in practice, these violations need to be detected in the order of milliseconds, without raising false alarms. To date, most real-time data plane checkers address this problem by exploiting at least one of the following two observations: (i) only small parts of the network tend to be affected by typical changes to the data plane, and (ii) many different packets tend to share the same forwarding behaviour in the entire network. This paper shows how to effectively exploit a third characteristic of the problem, namely: similarity among forwarding behaviour of packets through parts of the network, rather than its entirety. We propose the first provably amortized quasi-linear algorithm to do so. We implement our algorithm in a new real-time data plane checker, Delta-net. Our experiments with SDN-IP, a globally deployed ONOS software-defined networking application, and several hundred million IP prefix rules generated using topologies and BGP updates from real-world deployed networks, show that Delta-net checks a rule insertion or removal in approximately 40 microseconds on average, a more than 10X improvement over the state-of-the-art. We also show that Delta-net eliminates an inherent bottleneck in the state-of-the-art that restricts its use in answering Datalog-style "what if" queries.
Glimmers: Resolving the Privacy/Trust Quagmire
Venue: arXiv cs.CR 2017
Year: 2017

Many successful services rely on trustworthy contributions from users. To establish that trust, such services often require access to privacy-sensitive information from users, thus creating a conflict between privacy and trust. Although it is likely impractical to expect both absolute privacy and trustworthiness at the same time, we argue that the current state of things, where individual privacy is usually sacrificed at the altar of trustworthy services, can be improved with a pragmatic $Glimmer$ $of$ $Trust$, which allows services to validate user contributions in a trustworthy way without forfeiting user privacy. We describe how trustworthy hardware such as Intel's SGX can be used client-side -- in contrast to much recent work exploring SGX in cloud services -- to realize the Glimmer architecture, and demonstrate how this realization is able to resolve the tension between privacy and trust in a variety of cases.
On Relation between Constraint Answer Set Programming and Satisfiability Modulo Theories
Venue: arXiv cs.LO 2017
Year: 2017

Constraint answer set programming is a promising research direction that integrates answer set programming with constraint processing. It is often informally related to the field of satisfiability modulo theories. Yet, the exact formal link is obscured as the terminology and concepts used in these two research areas differ. In this paper, we connect these two research areas by uncovering the precise formal relation between them. We believe that this work will booster the cross-fertilization of the theoretical foundations and the existing solving methods in both areas. As a step in this direction we provide a translation from constraint answer set programs with integer linear constraints to satisfiability modulo linear integer arithmetic that paves the way to utilizing modern satisfiability modulo theories solvers for computing answer sets of constraint answer set programs.
Exact Synthesis of Reversible Logic Circuits using Model Checking
Venue: arXiv cs.ET 2017
Year: 2017

Synthesis of reversible logic circuits has gained great atten- tion during the last decade. Various synthesis techniques have been pro- posed, some generate optimal solutions (in gate count) and are termed as exact, while others are scalable in the sense that they can handle larger functions but generate sub-optimal solutions. Although scalable synthe- sis is very much essential for circuit design, exact synthesis is also of great importance as it helps in building design library for the synthesis of larger functions. In this paper, we propose an exact synthesis technique for re- versible circuits using model checking. We frame the synthesis problem as a model checking instance and propose an iterative bounded model checking calls for an optimal synthesis. Experiments on reversible logic benchmarks shows successful synthesis of optimal circuits. We also illus- trate optimal synthesis of random functions with as many as 10 variables and up to 10 gates.
Dirichlet-vMF Mixture Model
Venue: arXiv cs.CL 2017
Year: 2017

This document is about the multi-document Von-Mises-Fisher mixture model with a Dirichlet prior, referred to as VMFMix. VMFMix is analogous to Latent Dirichlet Allocation (LDA) in that they can capture the co-occurrence patterns acorss multiple documents. The difference is that in VMFMix, the topic-word distribution is defined on a continuous n-dimensional hypersphere. Hence VMFMix is used to derive topic embeddings, i.e., representative vectors, from multiple sets of embedding vectors. An efficient Variational Expectation-Maximization inference algorithm is derived. The performance of VMFMix on two document classification tasks is reported, with some preliminary analysis.
Yet Another Pseudorandom Number Generator
Venue: arXiv cs.CR 2017
Year: 2017

We propose a novel pseudorandom number generator based on Rössler attractor and bent Boolean function. We estimated the output bits properties by number of statistical tests. The results of the cryptanalysis show that the new pseudorandom number generation scheme provides a high level of data security.
Medical Image Retrieval Based On the Parallelization of the Cluster Sampling Algorithm
Venue: arXiv cs.DC 2017
Year: 2017

In this paper we develop parallel cluster sampling algorithms and show that a multi-chain version is embarrassingly parallel and can be used efficiently for medical image retrieval among other applications.
Event-Triggered Consensus for Linear Continuous-time Multi-agent Systems Based on a Predictor
Venue: arXiv cs.SY 2017
Year: 2017

In this paper, the problem of event-triggered consensus for linear continuous-time multi-agent systems is investigated. A new event-triggered consensus protocol based on a predictor is proposed to achieve consensus without continuous communication among agents. In the proposed consensus protocol, each agent only needs to monitor its states to determine its event-triggered instants. When an event is triggered, the agent will update its consensus protocol and sent its state information to its neighbors. In addition, the agent will also update its consensus protocol and the predictor when it receives the state information from its neighbors. A necessary and sufficient condition that the consensus problem can be solved is derived. Moreover, it is proved that Zeno behavior does not exist. Finally, a numerical example is given to illustrate that the protocol proposed in this paper can make the multi-agent systems achieve consensus through much fewer event-triggered times.
How hard is it to cross the room? -- Training (Recurrent) Neural Networks to steer a UAV
Venue: arXiv cs.CV 2017
Year: 2017

This work explores the feasibility of steering a drone with a (recurrent) neural network, based on input from a forward looking camera, in the context of a high-level navigation task. We set up a generic framework for training a network to perform navigation tasks based on imitation learning. It can be applied to both aerial and land vehicles. As a proof of concept we apply it to a UAV (Unmanned Aerial Vehicle) in a simulated environment, learning to cross a room containing a number of obstacles. So far only feedforward neural networks (FNNs) have been used to train UAV control. To cope with more complex tasks, we propose the use of recurrent neural networks (RNN) instead and successfully train an LSTM (Long-Short Term Memory) network for controlling UAVs. Vision based control is a sequential prediction problem, known for its highly correlated input data. The correlation makes training a network hard, especially an RNN. To overcome this issue, we investigate an alternative sampling method during training, namely window-wise truncated backpropagation through time (WW-TBPTT). Further, end-to-end training requires a lot of data which often is not available. Therefore, we compare the performance of retraining only the Fully Connected (FC) and LSTM control layers with networks which are trained end-to-end. Performing the relatively simple task of crossing a room already reveals important guidelines and good practices for training neural control networks. Different visualizations help to explain the behavior learned.
Path Planning for Multiple Heterogeneous Unmanned Vehicles with Uncertain Service Times
Venue: arXiv cs.RO 2017
Year: 2017

This article presents a framework and develops a formulation to solve a path planning problem for multiple heterogeneous Unmanned Vehicles (UVs) with uncertain service times for each vehicle--target pair. The vehicles incur a penalty proportional to the duration of their total service time in excess of a preset constant. The vehicles differ in their motion constraints and are located at distinct depots at the start of the mission. The vehicles may also be equipped with disparate sensors. The objective is to find a tour for each vehicle that starts and ends at its respective depot such that every target is visited and serviced by some vehicle while minimizing the sum of the total travel distance and the expected penalty incurred by all the vehicles. We formulate the problem as a two-stage stochastic program with recourse, present the theoretical properties of the formulation and advantages of using such a formulation, as opposed to a deterministic expected value formulation, to solve the problem. Extensive numerical simulations also corroborate the effectiveness of the proposed approach.