OpenRaiser/Intern-Atlas huggingface dataset:
Controller synthesis for MDPs and Frequency LTL$\setminus$GU
Venue: arXiv cs.LO 2015
Year: 2015

Quantitative extensions of temporal logics have recently attracted significant attention. In this work, we study frequency LTL (fLTL), an extension of LTL which allows to speak about frequencies of events along an execution. Such an extension is particularly useful for probabilistic systems that often cannot fulfil strict qualitative guarantees on the behaviour. It has been recently shown that controller synthesis for Markov decision processes and fLTL is decidable when all the bounds on frequencies are 1. As a step towards a complete quantitative solution, we show that the problem is decidable for the fragment fLTL$\setminus$GU, where U does not occur in the scope of G (but still F can). Our solution is based on a novel translation of such quantitative formulae into equivalent deterministic automata.
DeltaImpactFinder: Assessing Semantic Merge Conflicts with Dependency Analysis
Venue: arXiv cs.SE 2015
Year: 2015

In software development, version control systems (VCS) provide branching and merging support tools. Such tools are popular among developers to concurrently change a code-base in separate lines and reconcile their changes automatically afterwards. However, two changes that are correct independently can introduce bugs when merged together. We call semantic merge conflicts this kind of bugs. Change impact analysis (CIA) aims at estimating the effects of a change in a codebase. In this paper, we propose to detect semantic merge conflicts using CIA. On a merge, DELTAIMPACTFINDER analyzes and compares the impact of a change in its origin and destination branches. We call the difference between these two impacts the delta-impact. If the delta-impact is empty, then there is no indicator of a semantic merge conflict and the merge can continue automatically. Otherwise, the delta-impact contains what are the sources of possible conflicts.
Wireless Throughput and Energy Efficiency with Random Arrivals and Statistical Queueing Constraints
Venue: arXiv cs.IT 2015
Year: 2015

Throughput and energy efficiency in fading channels are studied in the presence of randomly arriving data and statistical queueing constraints. In particular, Markovian arrival models including discrete-time Markov, Markov fluid, and Markov-modulated Poisson sources are considered. Employing the effective bandwidth of time-varying sources and effective capacity of time-varying wireless transmissions, maximum average arrival rates in the presence of statistical queueing constraints are characterized. For the two-state (ON/OFF) source models, throughput is determined in closed-form as a function of the source statistics, channel characteristics, and quality of service (QoS) constraints. Throughput is further studied in certain asymptotic regimes. Furthermore, energy efficiency is analyzed by determining the minimum energy per bit and wideband slope in the low signal-to-noise ratio (SNR) regime. Overall, the impact of source characteristics, QoS requirements, and channel fading correlations on the throughput and energy efficiency of wireless systems is identified.
Comment on "Asymptotic Achievability of the Cramér-Rao Bound for Noisy Compressive Sampling"
Venue: arXiv cs.IT 2015
Year: 2015

In [1], we proved the asymptotic achievability of the Cramér-Rao bound in the compressive sensing setting in the linear sparsity regime. In the proof, we used an erroneous closed-form expression of $ασ^2$ for the genie-aided Cramér-Rao bound $σ^2 \textrm{Tr} (\mathbf{A}^*_\mathcal{I} \mathbf{A}_\mathcal{I})^{-1}$ from Lemma 3.5, which appears in Eqs. (20) and (29). The proof, however, holds if one avoids replacing $σ^2 \textrm{Tr} (\mathbf{A}^*_\mathcal{I} \mathbf{A}_\mathcal{I})^{-1}$ by the expression of Lemma 3.5, and hence the claim of the Main Theorem stands true. In Chapter 2 of the Ph. D. dissertation by Behtash Babadi [2], this error was fixed and a more detailed proof in the non-asymptotic regime was presented. A draft of Chapter 2 of [2] is included in this note, verbatim. We would like to refer the interested reader to the full dissertation, which is electronically archived in the ProQuest database [2], and a draft of which can be accessed through the author's homepage under: http://ece.umd.edu/~behtash/babadi_thesis_2011.pdf.
Neuron detection in stack images: a persistent homology interpretation
Venue: arXiv cs.CV 2015
Year: 2015

Automation and reliability are the two main requirements when computers are applied in Life Sciences. In this paper we report on an application to neuron recognition, an important step in our long-term project of providing software systems to the study of neural morphology and functionality from biomedical images. Our algorithms have been implemented in an ImageJ plugin called NeuronPersistentJ, which has been validated experimentally. The soundness and reliability of our approach are based on the interpretation of our processing methods with respect to persistent homology, a well-known tool in computational mathematics.
Energy Harvesting for Physical-Layer Security in OFDMA Networks
Venue: arXiv cs.IT 2015
Year: 2015

In this paper, we study the simultaneous wireless information and power transfer (SWIPT) in downlink multiuser orthogonal frequency-division multiple access (OFDMA) systems, where each user applies power splitting scheme to coordinate the energy harvesting and secrecy information decoding processes. Assuming equal power allocation across subcarriers, we formulate the problem to maximize the aggregate harvested power of all users while satisfying secrecy rate requirement of individual user by joint subcarrier allocation and optimal power splitting ratio selection. Due to the NP-hardness of the problem, we propose two suboptimal algorithms to solve the problem in the dual domain. The first one is an iterative algorithm that optimizes subcarrier allocation and power splitting in an alternating way. The second algorithm is based on a two-step approach that solves the subcarrier allocation and power splitting sequentially. The numerical results show that the proposed methods outperform conventional methods. It is also shown that the iterative algorithm performs close to the upper bound and the step-wise algorithm provides good tradeoffs between performance and complexity.
Architecture and Behavior Modeling of Cyber-Physical Systems with MontiArcAutomaton
Venue: arXiv cs.SE 2015
Year: 2015

This book presents MontiArcAutomaton, a modeling language for architecture and be- havior modeling of Cyber-Physical Systems as interactive Component & Connector mod- els. MontiArcAutomaton extends the Architecture Description Language MontiArc with automata to describe component behavior. The modeling language MontiArcAutomaton provides syntactical elements for defin- ing automata with states, variables, and transitions inside MontiArc components. These syntactical elements and a basic set of well-formedness rules provide the syntax for a fam- ily of modeling languages for state-based behavior modeling in Component & Connector architectures. We present two concrete language profiles with additional well-formedness rules to model time-synchronous component behavior and untimed, event-driven behav- ior of components. This book gives an overview of the MontiArcAutomaton language including examples, a language reference, and a context-free grammar for MontiArcAutomaton models. It also provides syntax definition, well-formedness rules, and semantics for two language profiles. We summarize projects and case studies applying MontiArcAutomaton. MontiArcAutomaton is implemented using the DSL framework MontiCore. Available tools include a textual editor with syntax highlighting and code completion as well as a graphical editor and a powerful and extensible code generation framework for target languages including EMF, Java, Mona, and Python.
Decentralized gradient algorithm for solution of a linear equation
Venue: arXiv cs.SY 2015
Year: 2015

The paper develops a technique for solving a linear equation $Ax=b$ with a square and nonsingular matrix $A$, using a decentralized gradient algorithm. In the language of control theory, there are $n$ agents, each storing at time $t$ an $n$-vector, call it $x_i(t)$, and a graphical structure associating with each agent a vertex of a fixed, undirected and connected but otherwise arbitrary graph $\mathcal G$ with vertex set and edge set $\mathcal V$ and $\mathcal E$ respectively. We provide differential equation update laws for the $x_i$ with the property that each $x_i$ converges to the solution of the linear equation exponentially fast. The equation for $x_i$ includes additive terms weighting those $x_j$ for which vertices in $\mathcal G$ corresponding to the $i$-th and $j$-th agents are adjacent. The results are extended to the case where $A$ is not square but has full row rank, and bounds are given on the convergence rate.
Kernelized Deep Convolutional Neural Network for Describing Complex Images
Venue: arXiv cs.CV 2015
Year: 2015

With the impressive capability to capture visual content, deep convolutional neural networks (CNN) have demon- strated promising performance in various vision-based ap- plications, such as classification, recognition, and objec- t detection. However, due to the intrinsic structure design of CNN, for images with complex content, it achieves lim- ited capability on invariance to translation, rotation, and re-sizing changes, which is strongly emphasized in the s- cenario of content-based image retrieval. In this paper, to address this problem, we proposed a new kernelized deep convolutional neural network. We first discuss our motiva- tion by an experimental study to demonstrate the sensitivi- ty of the global CNN feature to the basic geometric trans- formations. Then, we propose to represent visual content with approximate invariance to the above geometric trans- formations from a kernelized perspective. We extract CNN features on the detected object-like patches and aggregate these patch-level CNN features to form a vectorial repre- sentation with the Fisher vector model. The effectiveness of our proposed algorithm is demonstrated on image search application with three benchmark datasets.
Medical Image Classification via SVM using LBP Features from Saliency-Based Folded Data
Venue: arXiv cs.CV 2015
Year: 2015

Good results on image classification and retrieval using support vector machines (SVM) with local binary patterns (LBPs) as features have been extensively reported in the literature where an entire image is retrieved or classified. In contrast, in medical imaging, not all parts of the image may be equally significant or relevant to the image retrieval application at hand. For instance, in lung x-ray image, the lung region may contain a tumour, hence being highly significant whereas the surrounding area does not contain significant information from medical diagnosis perspective. In this paper, we propose to detect salient regions of images during training and fold the data to reduce the effect of irrelevant regions. As a result, smaller image areas will be used for LBP features calculation and consequently classification by SVM. We use IRMA 2009 dataset with 14,410 x-ray images to verify the performance of the proposed approach. The results demonstrate the benefits of saliency-based folding approach that delivers comparable classification accuracies with state-of-the-art but exhibits lower computational cost and storage requirements, factors highly important for big data analytics.
Controller Synthesis with Inductive Proofs for Piecewise Linear Systems: an SMT-based Algorithm
Venue: arXiv cs.SY 2015
Year: 2015

We present a controller synthesis algorithm for reach-avoid problems for piecewise linear discrete-time systems. Our algorithm relies on SMT solvers and in this paper we focus on piecewise constant control strategies. Our algorithm generates feedback control laws together with inductive proofs of unbounded time safety and progress properties with respect to the reach-avoid sets. Under a reasonable robustness assump- tion, the algorithm is shown to be complete. That is, it either generates a controller of the above type along with a proof of correctness, or it establishes the impossibility of the existence of such controllers. To achieve this, the algorithm iteratively attempts to solve a weakened and strengthened versions of the SMT encoding of the reach-avoid problem. We present preliminary experimental results on applying this algorithm based on a prototype implementation.
Impact of Transceiver Impairments on the Capacity of Dual-Hop Relay Massive MIMO Systems
Venue: arXiv cs.IT 2015
Year: 2015

Despite the deleterious effect of hardware impairments on communication systems, most prior works have not investigated their impact on widely used relay systems. Most importantly, the application of inexpensive transceivers, being prone to hardware impairments, is the most cost-efficient way for the implementation of massive multiple-input multiple-output (MIMO) systems. Consequently, the direction of this paper is towards the investigation of the impact of hardware impairments on MIMO relay networks with large number of antennas. Specifically, we obtain the general expression for the ergodic capacity of dual-hop (DH) amplify-and-forward (AF) relay systems. Next, given the advantages of the free probability (FP) theory with comparison to other known techniques in the area of large random matrix theory, we pursue a large limit analysis in terms of number of antennas and users by shedding light to the behavior of relay systems inflicted by hardware impairments.
Direct high-order edge-preserving regularization for tomographic image reconstruction
Venue: arXiv cs.CV 2015
Year: 2015

In this paper we present a new two-level iterative algorithm for tomographic image reconstruction. The algorithm uses a regularization technique, which we call edge-preserving Laplacian, that preserves sharp edges between objects while damping spurious oscillations in the areas where the reconstructed image is smooth. Our numerical simulations demonstrate that the proposed method outperforms total variation (TV) regularization and it is competitive with the combined TV-L2 penalty. Obtained reconstructed images show increased signal-to-noise ratio and visually appealing structural features. Computer implementation and parameter control of the proposed technique is straightforward, which increases the feasibility of it across many tomographic applications. In this paper, we applied our method to the under-sampled computed tomography (CT) projection data and also considered a case of reconstruction in emission tomography The MATLAB code is provided to support obtained results.
Free-body Gesture Tracking and Augmented Reality Improvisation for Floor and Aerial Dance
Venue: arXiv cs.MM 2015
Year: 2015

This paper describes an updated interactive performance system for floor and Aerial Dance that controls visual and sonic aspects of the presentation via a depth sensing camera (MS Kinect). In order to detect, measure and track free movement in space, 3 degree of freedom (3-DOF) tracking in space (on the ground and in the air) is performed using IR markers with a method for multi target tracking capabilities added and described in detail. An improved gesture tracking and recognition system, called Action Graph (AG), is described in the paper. Action Graph uses an efficient incremental construction from a single long sequence of movement features and automatically captures repeated sub-segments in the movement from start to finish with no manual interaction needed with other advanced capabilities discussed as well. By using the new model for the gesture we can unify an entire choreography piece by dynamically tracking and recognizing gestures and sub-portions of the piece. This gives the performer the freedom to improvise based on a set of recorded gestures/portions of the choreography and have the system dynamically respond in relation to the performer within a set of related rehearsed actions, an ability that has not been seen in any other system to date.
amLite: Amharic Transliteration Using Key Map Dictionary
Venue: arXiv cs.CL 2015
Year: 2015

amLite is a framework developed to map ASCII transliterated Amharic texts back to the original Amharic letter texts. The aim of such a framework is to make existing Amharic linguistic data consistent and interoperable among researchers. For achieving the objective, a key map dictionary is constructed using the possible ASCII combinations actively in use for transliterating Amharic letters; and a mapping of the combinations to the corresponding Amharic letters is done. The mapping is then used to replace the Amharic linguistic text back to form the original Amharic letters text. The framework indicated 97.7, 99.7 and 98.4 percentage accuracy on converting the three sample random test data. It is; however, possible to improve the accuracy of the framework by adding an exception to the implementation of the algorithm, or by preprocessing the input text prior to conversion. This paper outlined the rationales behind the need for developing the framework and the processes undertaken in the development.
Melodic Contour and Mid-Level Global Features Applied to the Analysis of Flamenco Cantes
Venue: arXiv cs.SD 2015
Year: 2015

This work focuses on the topic of melodic characterization and similarity in a specific musical repertoire: a cappella flamenco singing, more specifically in debla and martinete styles. We propose the combination of manual and automatic description. First, we use a state-of-the-art automatic transcription method to account for general melodic similarity from music recordings. Second, we define a specific set of representative mid-level melodic features, which are manually labeled by flamenco experts. Both approaches are then contrasted and combined into a global similarity measure. This similarity measure is assessed by inspecting the clusters obtained through phylogenetic algorithms algorithms and by relating similarity to categorization in terms of style. Finally, we discuss the advantage of combining automatic and expert annotations as well as the need to include repertoire-specific descriptions for meaningful melodic characterization in traditional music collections.
A new model for multi-commodity macroscopic modeling of complex traffic networks
Venue: arXiv cs.SY 2015
Year: 2015

We propose a macroscopic modeling framework for a network of roads and multi-commodity traffic. The proposed framework is based on the Lighthill-Whitham-Richards kinematic wave theory; more precisely, on its discretization, the Cell Transmission Model (CTM), adapted for networks and multi-commodity traffic. The resulting model is called the Link-Node CTM (LNCTM). In the LNCTM, we use the fundamental diagram of an "inverse lambda" shape that allows modeling of the capacity drop and the hysteresis behavior of the traffic state in a link that goes from free flow to congestion and back. A model of the node with multiple input and multiple output links accepting multi-commodity traffic is a cornerstone of the LNCTM. We present the multi-input-multi-output (MIMO) node model for multi-commodity traffic that supersedes previously developed node models. The analysis and comparison with previous node models are provided. Sometimes, certain traffic commodities may choose between multiple output links in a node based on the current traffic state of the node's input and output links. For such situations, we propose a local traffic assignment algorithm that computes how incoming traffic of a certain commodity should be distributed between output links, if this information is not known a priori.
Processing Analytical Workloads Incrementally
Venue: arXiv cs.DB 2015
Year: 2015

Analysis of large data collections using popular machine learning and statistical algorithms has been a topic of increasing research interest. A typical analysis workload consists of applying an algorithm to build a model on a data collection and subsequently refining it based on the results. In this paper we introduce model materialization and incremental model reuse as first class citizens in the execution of analysis workloads. We materialize built models instead of discarding them in a way that can be reused in subsequent computations. At the same time we consider manipulating an existing model (adding or deleting data from it) in order to build a new one. We discuss our approach in the context of popular machine learning models. We specify the details of how to incrementally maintain models as well as outline the suitable optimizations required to optimally use models and their incremental adjustments to build new ones. We detail our techniques for linear regression, naive bayes and logistic regression and present the suitable algorithms and optimizations to handle these models in our framework. We present the results of a detailed performance evaluation, using real and synthetic data sets. Our experiments analyze the various trade offs inherent in our approach and demonstrate vast performance benefits.
On Tree Representations of Relations and Graphs: Symbolic Ultrametrics and Cograph Edge Decompositions
Venue: arXiv cs.DM 2015
Year: 2015

Tree representations of (sets of) symmetric binary relations, or equivalently edge-colored undirected graphs, are of central interest, e.g.\ in phylogenomics. In this context symbolic ultrametrics play a crucial role. Symbolic ultrametrics define an edge-colored complete graph that allows to represent the topology of this graph as a vertex-colored tree. Here, we are interested in the structure and the complexity of certain combinatorial problems resulting from considerations based on symbolic ultrametrics, and on algorithms to solve them. This includes, the characterization of symbolic ultrametrics that additionally distinguishes between edges and non-edges of \emph{arbitrary} edge-colored graphs $G$ and thus, yielding a tree representation of $G$, by means of so-called cographs. Moreover, we address the problem of finding "closest" symbolic ultrametrics and show the NP-completeness of the three problems: symbolic ultrametric editing, completion and deletion. Finally, as not all graphs are cographs, and hence, don't have a tree representation, we ask, furthermore, what is the minimum number of cotrees needed to represent the topology of an arbitrary non-cograph $G$. This is equivalent to find an optimal cograph edge $k$-decomposition $\{E_1,\dots,E_k\}$ of $E$ so that each subgraph $(V,E_i)$ of $G$ is a cograph. We investigate this problem in full detail, resulting in several new open problems, and NP-hardness results. For all optimization problems proven to be NP-hard we will provide integer linear program (ILP) formulations to efficiently solve them.