OpenRaiser/Intern-Atlas huggingface dataset:
Computation of time-optimal control problem with variation evolution principle
Venue: arXiv cs.SY 2017
Year: 2017

An effective form of the Variation Evolving Method (VEM), which originates from the continuous-time dynamics stability theory, is developed for the classic time-optimal control problem with control constraint. Within the mathematic derivation, the Pontryagin's Minimum Principle (PMP) optimality conditions are used. Techniques including limited integrator and corner points are introduced to capture the right solution. The variation dynamic evolving equation may be reformulated as the Partial Differential Equation (PDE), and then discretized as finite-dimensional Initial-value Problem (IVP) to be solved with common Ordinary Differential Equation (ODE) integration methods. An illustrative example is solved to show the effectiveness of the method. In particular, the VEM is further developed to be more flexible in treating the boundary conditions of the Optimal Control Problem (OCP), by initializing the transformed IVP with arbitrary initial values of variables.
Recency-weighted Markovian inference
Venue: arXiv cs.LG 2017
Year: 2017

We describe a Markov latent state space (MLSS) model, where the latent state distribution is a decaying mixture over multiple past states. We present a simple sampling algorithm that allows to approximate such high-order MLSS with fixed time and memory costs.
Automata Minimization: a Functorial Approach
Venue: arXiv cs.FL 2017
Year: 2017

In this paper we regard languages and their acceptors -- such as deterministic or weighted automata, transducers, or monoids -- as functors from input categories that specify the type of the languages and of the machines to categories that specify the type of outputs. Our results are as follows: a) We provide sufficient conditions on the output category so that minimization of the corresponding automata is guaranteed. b) We show how to lift adjunctions between the categories for output values to adjunctions between categories of automata. c) We show how this framework can be applied to several phenomena in automata theory, starting with determinization and minimization (previously studied from a coalgebraic and duality theoretic perspective). We apply in particular these techniques to Choffrut's minimization algorithm for subsequential transducers and revisit Brzozowski's minimization algorithm.
A Grammar Compression Algorithm based on Induced Suffix Sorting
Venue: arXiv cs.DS 2017
Year: 2017

We introduce GCIS, a grammar compression algorithm based on the induced suffix sorting algorithm SAIS, introduced by Nong et al. in 2009. Our solution builds on the factorization performed by SAIS during suffix sorting. We construct a context-free grammar on the input string which can be further reduced into a shorter string by substituting each substring by its correspondent factor. The resulting grammar is encoded by exploring some redundancies, such as common prefixes between suffix rules, which are sorted according to SAIS framework. When compared to well-known compression tools such as Re-Pair and 7-zip, our algorithm is competitive and very effective at handling repetitive string regarding compression ratio, compression and decompression running time.
Analysis of the U.S. Patient Referral Network
Venue: arXiv cs.SI 2017
Year: 2017

In this paper we analyze the US Patient Referral Network (also called the Shared Patient Network) and various subnetworks for the years 2009--2015. In these networks two physicians are linked if a patient encounters both of them within a specified time-interval, according to the data made available by the Centers for Medicare and Medicaid Services. We find power law distributions on most state-level data as well as a core-periphery structure. On a national and state level, we discover a so-called small-world structure as well as a "gravity law" of the type found in some large-scale economic networks. Some physicians play the role of hubs for interstate referral. Strong correlations between certain network statistics with healthcare system statistics at both the state and national levels are discovered. The patterns in the referral network evinced using several statistical analyses involving key metrics derived from the network illustrate the potential for using network analysis to provide new insights into the healthcare system and opportunities or mechanisms for catalyzing improvements.
Go with the Flow: Compositional Abstractions for Concurrent Data Structures (Extended Version)
Venue: arXiv cs.LO 2017
Year: 2017

Concurrent separation logics have helped to significantly simplify correctness proofs for concurrent data structures. However, a recurring problem in such proofs is that data structure abstractions that work well in the sequential setting are much harder to reason about in a concurrent setting due to complex sharing and overlays. To solve this problem, we propose a novel approach to abstracting regions in the heap by encoding the data structure invariant into a local condition on each individual node. This condition may depend on a quantity associated with the node that is computed as a fixpoint over the entire heap graph. We refer to this quantity as a flow. Flows can encode both structural properties of the heap (e.g. the reachable nodes from the root form a tree) as well as data invariants (e.g. sortedness). We then introduce the notion of a flow interface, which expresses the relies and guarantees that a heap region imposes on its context to maintain the local flow invariant with respect to the global heap. Our main technical result is that this notion leads to a new semantic model of separation logic. In this model, flow interfaces provide a general abstraction mechanism for describing complex data structures. This abstraction mechanism admits proof rules that generalize over a wide variety of data structures. To demonstrate the versatility of our approach, we show how to extend the logic RGSep with flow interfaces. We have used this new logic to prove linearizability and memory safety of nontrivial concurrent data structures. In particular, we obtain parametric linearizability proofs for concurrent dictionary algorithms that abstract from the details of the underlying data structure representation. These proofs cannot be easily expressed using the abstraction mechanisms provided by existing separation logics.
Orchestrating Complex Application Architectures in Heterogeneous Clouds
Venue: arXiv cs.DC 2017
Year: 2017

Private cloud infrastructures are now widely deployed and adopted across technology industries and research institutions. Although cloud computing has emerged as a reality, it is now known that a single cloud provider cannot fully satisfy complex user requirements. This has resulted in a growing interest in developing hybrid cloud solutions that bind together distinct and heterogeneous cloud infrastructures. In this paper we describe the orchestration approach for heterogeneous clouds that has been implemented and used within the INDIGO-DataCloud project. This orchestration model uses existing open-source software like OpenStack and leverages the OASIS Topology and Specification for Cloud Applications (TOSCA) open standard as the modeling language. Our approach uses virtual machines and Docker containers in an homogeneous and transparent way providing consistent application deployment for the users. This approach is illustrated by means of two different use cases in different scientific communities, implemented using the INDIGO-DataCloud solutions.
One-pass Person Re-identification by Sketch Online Discriminant Analysis
Venue: arXiv cs.CV 2017
Year: 2017

Person re-identification (re-id) is to match people across disjoint camera views in a multi-camera system, and re-id has been an important technology applied in smart city in recent years. However, the majority of existing person re-id methods are not designed for processing sequential data in an online way. This ignores the real-world scenario that person images detected from multi-cameras system are coming sequentially. While there is a few work on discussing online re-id, most of them require considerable storage of all passed data samples that have been ever observed, and this could be unrealistic for processing data from a large camera network. In this work, we present an onepass person re-id model that adapts the re-id model based on each newly observed data and no passed data are directly used for each update. More specifically, we develop an Sketch online Discriminant Analysis (SoDA) by embedding sketch processing into Fisher discriminant analysis (FDA). SoDA can efficiently keep the main data variations of all passed samples in a low rank matrix when processing sequential data samples, and estimate the approximate within-class variance (i.e. within-class covariance matrix) from the sketch data information. We provide theoretical analysis on the effect of the estimated approximate within-class covariance matrix. In particular, we derive upper and lower bounds on the Fisher discriminant score (i.e. the quotient between between-class variation and within-class variation after feature transformation) in order to investigate how the optimal feature transformation learned by SoDA sequentially approximates the offline FDA that is learned on all observed data. Extensive experimental results have shown the effectiveness of our SoDA and empirically support our theoretical analysis.
Data Fusion and Machine Learning Integration for Transformer Loss of Life Estimation
Venue: arXiv cs.SY 2017
Year: 2017

Rapid growth of machine learning methodologies and their applications offer new opportunity for improved transformer asset management. Accordingly, power system operators are currently looking for data-driven methods to make better-informed decisions in terms of network management. In this paper, machine learning and data fusion techniques are integrated to estimate transformer loss of life. Using IEEE Std. C57.91-2011, a data synthesis process is proposed based on hourly transformer loading and ambient temperature values. This synthesized data is employed to estimate transformer loss of life by using Adaptive Network-Based Fuzzy Inference System (ANFIS) and Radial Basis Function (RBF) network, which are further fused together with the objective of improving the estimation accuracy. Among various data fusion techniques, Ordered Weighted Averaging (OWA) and sequential Kalman filter are selected to fuse the output results of the estimated ANFIS and RBF. Simulation results demonstrate the merit and the effectiveness of the proposed method.
Higher-order Cons-free Interpreters
Venue: arXiv cs.LO 2017
Year: 2017

Constructor rewriting systems are said to be cons-free if any constructor term occurring in the rhs of a rule must be a subterm of the lhs of the rule. Roughly, such systems cannot build new data structures during their evaluation. In earlier work by several authors, (typed) cons-free systems have been used to characterise complexity classes such as polynomial or exponential time or space by varying the type orders, and the recursion forms allowed. This paper concerns the construction of interpreters for cons-free term rewriting. Due to their connection with proofs by diagonalisation, interpreters may be of use when studying separation results between complexity classes in implicit computational complexity theory. We are interested in interpreters of type order $k > 1$ that can interpret any term of strictly lower type order; while this gives us a well-known separation result E$^k$TIME $\subseteq$ E$^{k+1}$TIME, the hope is that more refined interpreters with syntactically limited constraints can be used to obtain a notion of faux diagonalisation and be used to attack open problems in complexity theory.
Open-World Knowledge Graph Completion
Venue: arXiv cs.AI 2017
Year: 2017

Knowledge Graphs (KGs) have been applied to many tasks including Web search, link prediction, recommendation, natural language processing, and entity linking. However, most KGs are far from complete and are growing at a rapid pace. To address these problems, Knowledge Graph Completion (KGC) has been proposed to improve KGs by filling in its missing connections. Unlike existing methods which hold a closed-world assumption, i.e., where KGs are fixed and new entities cannot be easily added, in the present work we relax this assumption and propose a new open-world KGC task. As a first attempt to solve this task we introduce an open-world KGC model called ConMask. This model learns embeddings of the entity's name and parts of its text-description to connect unseen entities to the KG. To mitigate the presence of noisy text descriptions, ConMask uses a relationship-dependent content masking to extract relevant snippets and then trains a fully convolutional neural network to fuse the extracted snippets with entities in the KG. Experiments on large data sets, both old and new, show that ConMask performs well in the open-world KGC task and even outperforms existing KGC models on the standard closed-world KGC task.
Fast Meta-Learning for Adaptive Hierarchical Classifier Design
Venue: arXiv cs.LG 2017
Year: 2017

We propose a new splitting criterion for a meta-learning approach to multiclass classifier design that adaptively merges the classes into a tree-structured hierarchy of increasingly difficult binary classification problems. The classification tree is constructed from empirical estimates of the Henze-Penrose bounds on the pairwise Bayes misclassification rates that rank the binary subproblems in terms of difficulty of classification. The proposed empirical estimates of the Bayes error rate are computed from the minimal spanning tree (MST) of the samples from each pair of classes. Moreover, a meta-learning technique is presented for quantifying the one-vs-rest Bayes error rate for each individual class from a single MST on the entire dataset. Extensive simulations on benchmark datasets show that the proposed hierarchical method can often be learned much faster than competing methods, while achieving competitive accuracy.
Language Modeling for Code-Switched Data: Challenges and Approaches
Venue: arXiv cs.CL 2017
Year: 2017

Lately, the problem of code-switching has gained a lot of attention and has emerged as an active area of research. In bilingual communities, the speakers commonly embed the words and phrases of a non-native language into the syntax of a native language in their day-to-day communications. The code-switching is a global phenomenon among multilingual communities, still very limited acoustic and linguistic resources are available as yet. For developing effective speech based applications, the ability of the existing language technologies to deal with the code-switched data can not be over emphasized. The code-switching is broadly classified into two modes: inter-sentential and intra-sentential code-switching. In this work, we have studied the intra-sentential problem in the context of code-switching language modeling task. The salient contributions of this paper includes: (i) the creation of Hindi-English code-switching text corpus by crawling a few blogging sites educating about the usage of the Internet (ii) the exploration of the parts-of-speech features towards more effective modeling of Hindi-English code-switched data by the monolingual language model (LM) trained on native (Hindi) language data, and (iii) the proposal of a novel textual factor referred to as the code-switch factor (CS-factor), which allows the LM to predict the code-switching instances. In the context of recognition of the code-switching data, the substantial reduction in the PPL is achieved with the use of POS factors and also the proposed CS-factor provides independent as well as additive gain in the PPL.
On Colorful Bin Packing Games
Venue: arXiv cs.GT 2017
Year: 2017

We consider colorful bin packing games in which selfish players control a set of items which are to be packed into a minimum number of unit capacity bins. Each item has one of $m\geq 2$ colors and cannot be packed next to an item of the same color. All bins have the same unitary cost which is shared among the items it contains, so that players are interested in selecting a bin of minimum shared cost. We adopt two standard cost sharing functions: the egalitarian cost function which equally shares the cost of a bin among the items it contains, and the proportional cost function which shares the cost of a bin among the items it contains proportionally to their sizes. Although, under both cost functions, colorful bin packing games do not converge in general to a (pure) Nash equilibrium, we show that Nash equilibria are guaranteed to exist and we design an algorithm for computing a Nash equilibrium whose running time is polynomial under the egalitarian cost function and pseudo-polynomial for a constant number of colors under the proportional one. We also provide a complete characterization of the efficiency of Nash equilibria under both cost functions for general games, by showing that the prices of anarchy and stability are unbounded when $m\geq 3$ while they are equal to 3 for black and white games, where $m=2$. We finally focus on games with uniform sizes (i.e., all items have the same size) for which the two cost functions coincide. We show again a tight characterization of the efficiency of Nash equilibria and design an algorithm which returns Nash equilibria with best achievable performance.
A New Proof Rule for Almost-Sure Termination
Venue: arXiv cs.PL 2017
Year: 2017

An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates "almost surely". Proving that can be hard, and this paper presents a new method for doing so; it is expressed in a program logic, and so applies directly to source code. The programs may contain both probabilistic- and demonic choice, and the probabilistic choices may depend on the current state. As do other researchers, we use variant functions (a.k.a. "super-martingales") that are real-valued and probabilistically might decrease on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (non-demonic) Markov chains.
Approaches to Stochastic Modeling of Wind Turbines
Venue: arXiv cs.CE 2017
Year: 2017

Background. This paper study statistical data gathered from wind turbines located on the territory of the Republic of Poland. The research is aimed to construct the stochastic model that predicts the change of wind speed with time. Purpose. The purpose of this work is to find the optimal distribution for the approximation of available statistical data on wind speed. Methods. We consider four distributions of a random variable: Log-Normal, Weibull, Gamma and Beta. In order to evaluate the parameters of distributions we use method of maximum likelihood. To assess the the results of approximation we use a quantile-quantile plot. Results. All the considered distributions properly approximate the available data. The Weibull distribution shows the best results for the extreme values of the wind speed. Conclusions. The results of the analysis are consistent with the common practice of using the Weibull distribution for wind speed modeling. In the future we plan to compare the results obtained with a much larger data set as well as to build a stochastic model of the evolution of the wind speed depending on time.
Traffic Models of Periodic Event-Triggered Control Systems
Venue: arXiv cs.SY 2017
Year: 2017

Periodic event-triggered control (PETC) is a version of event-triggered control (ETC) that only requires to measure the plant output periodically instead of continuously. In this work, we present a construction of timing models for these PETC implementations to capture the dynamics of the traffic they generate. In the construction, we employ a two-step approach. We first partition the state space into a finite number of regions. Then in each region, the event-triggering behavior is analyzed with the help of LMIs. The state transitions among different regions result from computing the reachable state set starting from each region within the computed event time intervals.
Distribution market as a ramping aggregator for grid flexibility support
Venue: arXiv cs.SY 2017
Year: 2017

The growing proliferation of microgrids and distributed energy resources in distribution networks has resulted in the development of Distribution Market Operator (DMO). This new entity will facilitate the management of the distributed resources and their interactions with upstream network and the wholesale market. At the same time, DMOs can tap into the flexibility potential of these distributed resources to address many of the challenges that system operators are facing. This paper investigates this opportunity and develops a distribution market scheduling model based on upstream network ramping flexibility requirements. That is, the distribution network will play the role of a flexibility resource in the system, with a relatively large size and potential, to help bulk system operators to address emerging ramping concerns. Numerical simulations demonstrate the effectiveness of the proposed model on when tested on a distribution system with several microgrids.
Object Referring in Visual Scene with Spoken Language
Venue: arXiv cs.CV 2017
Year: 2017

Object referring has important applications, especially for human-machine interaction. While having received great attention, the task is mainly attacked with written language (text) as input rather than spoken language (speech), which is more natural. This paper investigates Object Referring with Spoken Language (ORSpoken) by presenting two datasets and one novel approach. Objects are annotated with their locations in images, text descriptions and speech descriptions. This makes the datasets ideal for multi-modality learning. The approach is developed by carefully taking down ORSpoken problem into three sub-problems and introducing task-specific vision-language interactions at the corresponding levels. Experiments show that our method outperforms competing methods consistently and significantly. The approach is also evaluated in the presence of audio noise, showing the efficacy of the proposed vision-language interaction methods in counteracting background noise.
Refinement Reflection: Complete Verification with SMT
Venue: arXiv cs.PL 2017
Year: 2017

We introduce Refinement Reflection, a new framework for building SMT-based deductive verifiers. The key idea is to reflect the code implementing a user-defined function into the function's (output) refinement type. As a consequence, at uses of the function, the function definition is instantiated in the SMT logic in a precise fashion that permits decidable verification. Reflection allows the user to write equational proofs of programs just by writing other programs using pattern-matching and recursion to perform case-splitting and induction. Thus, via the propositions-as-types principle, we show that reflection permits the specification of arbitrary functional correctness properties. Finally, we introduce a proof-search algorithm called Proof by Logical Evaluation that uses techniques from model checking and abstract interpretation, to completely automate equational reasoning. We have implemented reflection in Liquid Haskell and used it to verify that the widely used instances of the Monoid, Applicative, Functor, and Monad typeclasses actually satisfy key algebraic laws required to make the clients safe, and have used reflection to build the first library that actually verifies assumptions about associativity and ordering that are crucial for safe deterministic parallelism.