OpenRaiser/Intern-Atlas huggingface dataset:
Requirements, Formal Verification and Model transformations of an Agent-based System: A CASE STUDY
Venue: arXiv cs.SE 2015
Year: 2015

One of the most challenging tasks in software specifications engineering for a multi-agent system is to ensure correctness. As these systems have high concurrency, often have dynamic environments, the formal specification and verification of these systems along with step-wise refinement from abstract to concrete concepts play major role in system correctness. Our objectives are the formal specification, analysis with respect to functional as well as non-functional properties by step-wise refinement from abstract to concrete specifications and then formal verification of these specifications. A multi-agent system is concurrent system with processes working in parallel with synchronization between them. We have worked on Gaia multi-agent method along with finite state process based finite automata techniques and as a result we have defined the formal specifications of our system, checked the correctness and verified all possible flow of concurrent executions of these specifications. Our contribution consists in transforming requirement specifications based on organizational abstractions into executable formal verification specifications based on finite automata. We have considered a case study of our multi-agent system to exemplify formal specifications and verification.
Varieties of Languages in a Category
Venue: arXiv cs.FL 2015
Year: 2015

Eilenberg's variety theorem, a centerpiece of algebraic automata theory, establishes a bijective correspondence between varieties of languages and pseudovarieties of monoids. In the present paper this result is generalized to an abstract pair of algebraic categories: we introduce varieties of languages in a category C, and prove that they correspond to pseudovarieties of monoids in a closed monoidal category D, provided that C and D are dual on the level of finite objects. By suitable choices of these categories our result uniformly covers Eilenberg's theorem and three variants due to Pin, Polak and Reutenauer, respectively, and yields new Eilenberg-type correspondences.
A Graph Theoretic Approach for Object Shape Representation in Compositional Hierarchies Using a Hybrid Generative-Descriptive Model
Venue: arXiv cs.CV 2015
Year: 2015

A graph theoretic approach is proposed for object shape representation in a hierarchical compositional architecture called Compositional Hierarchy of Parts (CHOP). In the proposed approach, vocabulary learning is performed using a hybrid generative-descriptive model. First, statistical relationships between parts are learned using a Minimum Conditional Entropy Clustering algorithm. Then, selection of descriptive parts is defined as a frequent subgraph discovery problem, and solved using a Minimum Description Length (MDL) principle. Finally, part compositions are constructed by compressing the internal data representation with discovered substructures. Shape representation and computational complexity properties of the proposed approach and algorithms are examined using six benchmark two-dimensional shape image datasets. Experiments show that CHOP can employ part shareability and indexing mechanisms for fast inference of part compositions using learned shape vocabularies. Additionally, CHOP provides better shape retrieval performance than the state-of-the-art shape retrieval methods.
Distributed mining of large scale remote sensing image archives on public computing infrastructures
Venue: arXiv cs.DC 2015
Year: 2015

Earth Observation (EO) mining aims at supporting efficient access and exploration of petabyte-scale space- and airborne remote sensing archives that are currently expanding at rates of terabytes per day. A significant challenge is performing the analysis required by envisaged applications --- like for instance process mapping for environmental risk management --- in reasonable time. In this work, we address the problem of content-based image retrieval via example-based queries from EO data archives. In particular, we focus on the analysis of polarimetric SAR data, for which target decomposition theorems have proved fundamental in discovering patterns in data and characterize the ground scattering properties. To this end, we propose an interactive region-oriented content-based image mining system in which 1) unsupervised ingestion processes are distributed onto virtual machines in elastic, on-demand computing infrastructures 2) archive-scale content hierarchical indexing is implemented in terms of a "big data" analytics cluster-computing framework 3) query processing amounts to traversing the generated binary tree index, computing distances that correspond to descriptor-based similarity measures between image groups and a query image tile. We describe in depth both the strategies and the actual implementations for the ingestion and indexing components, and verify the approach by experiments carried out on the NASA/JPL UAVSAR full polarimetric data archive. We report the results of the tests performed on computer clusters by using a public Infrastructure-as-a-Service and evaluating the impact of cluster configuration on system performance. Results are promising for data mapping and information retrieval applications.
Semantics for Locking Specifications
Venue: arXiv cs.PL 2015
Year: 2015

To prevent concurrency errors, programmers need to obey a locking discipline. Annotations that specify that discipline, such as Java's @GuardedBy, are already widely used. Unfortunately, their semantics is expressed informally and is consequently ambiguous. This article highlights such ambiguities and formalizes the semantics of @GuardedBy in two alternative ways, building on an operational semantics for a small concurrent fragment of a Java-like language. It also identifies when such annotations are actual guarantees against data races. Our work aids in understanding the annotations and supports the development of sound formal tools that verify or infer such annotations.
Wireless Information and Power Transfer in Relay Systems with Multiple Antennas and Interference
Venue: arXiv cs.IT 2015
Year: 2015

In this paper, an energy harvesting dual-hop relaying system without/with the presence of co-channel interference (CCI) is investigated. Specifically, the energy constrained multi-antenna relay node is powered by either the information signal of the source or via the signal receiving from both the source and interferer. In particular, we first study the outage probability and ergodic capacity of an interference free system, and then extend the analysis to an interfering environment. To exploit the benefit of multiple antennas, three different linear processing schemes are investigated, namely, 1) Maximum ratio combining/maximal ratio transmission (MRC/MRT), 2) Zero-forcing/MRT (ZF/MRT) and 3) Minimum mean-square error/MRT (MMSE/MRT). For all schemes, both the systems outage probability and ergodic capacity are studied, and the achievable diversity order is also presented. In addition, the optimal power splitting ratio minimizing the outage probability is characterized. Our results show that the implementation of multiple antennas increases the energy harvesting capability, hence, significantly improves the systems performance. Moreover, it is demonstrated that the CCI could be potentially exploited to substantially boost the performance, while the choice of a linear processing scheme plays a critical role in determining how much gain could be extracted from the CCI.
A Task-Type-Based Algorithm for the Energy-Aware Profit Maximizing Scheduling Problem in Heterogeneous Computing Systems
Venue: arXiv cs.DC 2015
Year: 2015

In this paper, we design an efficient algorithm for the energy-aware profit maximizing scheduling problem, where the high performance computing system administrator is to maximize the profit per unit time. The running time of the proposed algorithm is depending on the number of task types, while the running time of the previous algorithm is depending on the number of tasks. Moreover, we prove that the worst-case performance ratio is close to 2, which maybe the best result. Simulation experiments show that the proposed algorithm is more accurate than the previous method.
Classification of Message Spreading in a Heterogeneous Social Network
Venue: arXiv cs.SI 2015
Year: 2015

Nowadays, social networks such as Twitter, Facebook and LinkedIn become increasingly popular. In fact, they introduced new habits, new ways of communication and they collect every day several information that have different sources. Most existing research works fo-cus on the analysis of homogeneous social networks, i.e. we have a single type of node and link in the network. However, in the real world, social networks offer several types of nodes and links. Hence, with a view to preserve as much information as possible, it is important to consider so-cial networks as heterogeneous and uncertain. The goal of our paper is to classify the social message based on its spreading in the network and the theory of belief functions. The proposed classifier interprets the spread of messages on the network, crossed paths and types of links. We tested our classifier on a real word network that we collected from Twitter, and our experiments show the performance of our belief classifier.
Linear Massive MIMO Precoders in the Presence of Phase Noise -- A Large-Scale Analysis
Venue: arXiv cs.IT 2015
Year: 2015

We study the impact of phase noise on the downlink performance of a multi-user multiple-input multiple-output system, where the base station (BS) employs a large number of transmit antennas $M$. We consider a setup where the BS employs $M_{\mathrm{osc}}$ free-running oscillators, and $M/M_{\mathrm{osc}}$ antennas are connected to each oscillator. For this configuration, we analyze the impact of phase noise on the performance of the regularized zero-forcing (RZF), when $M$ and the number of users $K$ are asymptotically large, while the ratio $M/K=β$ is fixed. We analytically show that the impact of phase noise on the signal-to-interference-plus-noise ratio (SINR) can be quantified as an effective reduction in the quality of the channel state information available at the BS when compared to a system without phase noise. As a consequence, we observe that as $M_{\mathrm{osc}}$ increases, the SINR performance of all considered precoders degrades. On the other hand, the variance of the random phase variations caused by the BS oscillators reduces with increasing $M_{\mathrm{osc}}$. Through Monte-Carlo simulations, we verify our analytical results, and compare the performance of the precoders for different phase noise and channel noise variances. For all considered precoders, we show that when $β$ is small, the performance of the setup where all BS antennas are connected to a single oscillator is superior to that of the setup where each BS antenna has its own oscillator. However, the opposite is true when $β$ is large and the signal-to-noise ratio at the users is low.
On Frequency LTL in Probabilistic Systems
Venue: arXiv cs.LO 2015
Year: 2015

We study frequency linear-time temporal logic (fLTL) which extends the linear-time temporal logic (LTL) with a path operator $G^p$ expressing that on a path, certain formula holds with at least a given frequency p, thus relaxing the semantics of the usual G operator of LTL. Such logic is particularly useful in probabilistic systems, where some undesirable events such as random failures may occur and are acceptable if they are rare enough. Frequency-related extensions of LTL have been previously studied by several authors, where mostly the logic is equipped with an extended "until" and "globally" operator, leading to undecidability of most interesting problems. For the variant we study, we are able to establish fundamental decidability results. We show that for Markov chains, the problem of computing the probability with which a given fLTL formula holds has the same complexity as the analogous problem for LTL. We also show that for Markov decision processes the problem becomes more delicate, but when restricting the frequency bound $p$ to be 1 and negations not to be outside any $G^p$ operator, we can compute the maximum probability of satisfying the fLTL formula. This can be again performed with the same time complexity as for the ordinary LTL formulas.
Protograph-Based LDPC Code Design for Bit-Metric Decoding
Venue: arXiv cs.IT 2015
Year: 2015

A protograph-based low-density parity-check (LDPC) code design technique for bandwidth-efficient coded modulation is presented. The approach jointly optimizes the LDPC code node degrees and the mapping of the coded bits to the bit-interleaved coded modulation (BICM) bit-channels. For BICM with uniform input and for BICM with probabilistic shaping, binary-input symmetric-output surrogate channels are constructed and used for code design. The constructed codes perform as good as multi-edge type codes of Zhang and Kschischang (2013). For 64-ASK with probabilistic shaping, a blocklength 64800 code is constructed that operates within 0.69 dB of 0.5log(1+SNR) at a spectral efficiency of 4.2 bits/channel use and a frame error rate of 1e-3.
Second-Order Belief Hidden Markov Models
Venue: arXiv cs.AI 2015
Year: 2015

Hidden Markov Models (HMMs) are learning methods for pattern recognition. The probabilistic HMMs have been one of the most used techniques based on the Bayesian model. First-order probabilistic HMMs were adapted to the theory of belief functions such that Bayesian probabilities were replaced with mass functions. In this paper, we present a second-order Hidden Markov Model using belief functions. Previous works in belief HMMs have been focused on the first-order HMMs. We extend them to the second-order model.
Identification of a Hybrid Spring Mass Damper via Harmonic Transfer Functions as a Step Towards Data-Driven Models for Legged Locomotion
Venue: arXiv cs.RO 2015
Year: 2015

There are limitations on the extent to which manually constructed mathematical models can capture relevant aspects of legged locomotion. Even simple models for basic behaviors such as running involve non-integrable dynamics, requiring the use of possibly inaccurate approximations in the design of model-based controllers. In this study, we show how data-driven frequency domain system identification methods can be used to obtain input--output characteristics for a class of dynamical systems around their limit cycles, with hybrid structural properties similar to those observed in legged locomotion systems. Under certain assumptions, we can approximate hybrid dynamics of such systems around their limit cycle as a piecewise smooth linear time periodic system (LTP), further approximated as a time-periodic, piecewise LTI system to reduce parametric degrees of freedom in the identification process. In this paper, we use a simple one-dimensional hybrid model in which a limit-cycle is induced through the actions of a linear actuator to illustrate the details of our method. We first derive theoretical harmonic transfer functions of our example model. We then excite the model with small chirp signals to introduce perturbations around its limit-cycle and present systematic identification results to estimate the harmonic transfer functions for this model. Comparison between the data-driven HTF model and its theoretical prediction illustrates the potential effectiveness of such empirical identification methods in legged locomotion.
Safe Neighborhood Computation for Hybrid System Verification
Venue: arXiv cs.SY 2015
Year: 2015

For the design and implementation of engineering systems, performing model-based analysis can disclose potential safety issues at an early stage. The analysis of hybrid system models is in general difficult due to the intrinsic complexity of hybrid dynamics. In this paper, a simulation-based approach to formal verification of hybrid systems is presented.
A Reconfigurations Analogue of Brooks' Theorem and its Consequences
Venue: arXiv cs.CC 2015
Year: 2015

Let $G$ be a simple undirected graph on $n$ vertices with maximum degree~$Δ$. Brooks' Theorem states that $G$ has a $Δ$-colouring unless~$G$ is a complete graph, or a cycle with an odd number of vertices. To recolour $G$ is to obtain a new proper colouring by changing the colour of one vertex. We show an analogue of Brooks' Theorem by proving that from any $k$-colouring, $k>Δ$, a $Δ$-colouring of $G$ can be obtained by a sequence of $O(n^2)$ recolourings using only the original $k$ colours unless $G$ is a complete graph or a cycle with an odd number of vertices, or $k=Δ+1$, $G$ is $Δ$-regular and, for each vertex $v$ in $G$, no two neighbours of $v$ are coloured alike. We use this result to study the reconfiguration graph $R_k(G)$ of the $k$-colourings of $G$. The vertex set of $R_k(G)$ is the set of all possible $k$-colourings of $G$ and two colourings are adjacent if they differ on exactly one vertex. We prove that for $Δ\geq 3$, $R_{Δ+1}(G)$ consists of isolated vertices and at most one further component which has diameter $O(n^2)$. This result enables us to complete both a structural classification and an algorithmic classification for reconfigurations of colourings of graphs of bounded maximum degree.
Wise Computing: Towards Endowing System Development with True Wisdom
Venue: arXiv cs.SE 2015
Year: 2015

Encouraged by significant advances in algorithms and tools for verification and analysis, high level modeling and programming techniques, natural language programming, etc., we feel it is time for a major change in the way complex software and systems are developed. We present a vision that will shift the power balance between human engineers and the development and runtime environments. The idea is to endow the computer with human-like wisdom - not general wisdom, and not AI in the standard sense of the term - but wisdom geared towards classical system-building, which will be manifested, throughout development, in creativity and proactivity, and deep insights into the system's own structure and behavior, its overarching goals and rationale. Ideally, the computer will join the development team as an equal partner - knowledgeable, concerned, and responsibly active. We present a running demo of our initial efforts on the topic, illustrating on a small example what we feel is the feasibility of the ideas.
Multiple-Symbol Interleaved RS Codes and Two-Pass Decoding Algorithm
Venue: arXiv cs.IT 2015
Year: 2015

For communication systems with heavy burst noise, an optimal Forward Error Correction (FEC) scheme is expected to have a large burst error correction capacity while simultaneously owning moderate random error correction capability. This letter presents a new FEC scheme based on multiple-symbol interleaved Reed-Solomon codes and an associated two-pass decoding algorithm. It is shown that the proposed multi-symbol interleaved coding scheme can achieve nearly twice as much as the burst error correction capability of conventional symbol-interleaved Reed-Solomon codes with the same code length and code rate.
A new efficient Matching method for web services substitution
Venue: arXiv cs.IR 2015
Year: 2015

The internet is considered as the most extensive market in the world. To keep its gradual reputation, it must confront real problems that result from its distribution and from the diversity of the protocols used to insure communications. The Web service technology has diminished significantly the effects of distribution and heterogeneity, but there are several problems that weaken their performance (unavailability, load increase of use, high cost of CPU time...). Faced with this situation, we are forced to move in the direction of the substitution of web services. In this context, we propose an effective technique of substitution based on a new method of matching that allows detecting and expressing the matching between the web services pairwise by considering that each of them is ontology. Also, our method performs a discovery of the most similar web service to that to be replaced by using an efficient method of similarity measurement.
Cyber Attacks and Public Embarrassment: A Survey of Some Notable Hacks
Venue: arXiv cs.CY 2015
Year: 2015

We hear it all too often in the media: an organization is attacked, its data, often containing personally identifying information, is made public, and a hacking group emerges to claim credit. In this excerpt, we discuss how such groups operate and describe the details of a few major cyber-attacks of this sort in the wider context of how they occurred. We feel that understanding how such groups have operated in the past will give organizations ideas of how to defend against them in the future.
Input Synthesis for Sampled Data Systems by Program Logic
Venue: arXiv cs.SY 2015
Year: 2015

Inspired by a concrete industry problem we consider the input synthesis problem for hybrid systems: given a hybrid system that is subject to input from outside (also called disturbance or noise), find an input sequence that steers the system to the desired postcondition. In this paper we focus on sampled data systems--systems in which a digital controller interrupts a physical plant in a periodic manner, a class commonly known in control theory--and furthermore assume that a controller is given in the form of an imperative program. We develop a structural approach to input synthesis that features forward and backward reasoning in program logic for the purpose of reducing a search space. Although the examples we cover are limited both in size and in structure, experiments with a prototype implementation suggest potential of our program logic based approach.
Quantifying Potential Energy Efficiency Gain in Green Cellular Wireless Networks
Venue: arXiv cs.NI 2015
Year: 2015

Conventional cellular wireless networks were designed with the purpose of providing high throughput for the user and high capacity for the service provider, without any provisions of energy efficiency. As a result, these networks have an enormous Carbon footprint. In this paper, we describe the sources of the inefficiencies in such networks. First we present results of the studies on how much Carbon footprint such networks generate. We also discuss how much more mobile traffic is expected to increase so that this Carbon footprint will even increase tremendously more. We then discuss specific sources of inefficiency and potential sources of improvement at the physical layer as well as at higher layers of the communication protocol hierarchy. In particular, considering that most of the energy inefficiency in cellular wireless networks is at the base stations, we discuss multi-tier networks and point to the potential of exploiting mobility patterns in order to use base station energy judiciously. We then investigate potential methods to reduce this inefficiency and quantify their individual contributions. By a consideration of the combination of all potential gains, we conclude that an improvement in energy consumption in cellular wireless networks by two orders of magnitude, or even more, is possible.