OpenRaiser/Intern-Atlas huggingface dataset:
Fault Localization in Multi-Threaded C Programs using Bounded Model Checking (extended version)
Venue: arXiv cs.LO 2015
Year: 2015

Software debugging is a very time-consuming process, which is even worse for multi-threaded programs, due to the non-deterministic behavior of thread-scheduling algorithms. However, the debugging time may be greatly reduced, if automatic methods are used for localizing faults. In this study, a new method for fault localization, in multi-threaded C programs, is proposed. It transforms a multi-threaded program into a corresponding sequential one and then uses a fault-diagnosis method suitable for this type of program, in order to localize faults. The code transformation is implemented with rules and context switch information from counterexamples, which are typically generated by bounded model checkers. Experimental results show that the proposed method is effective, in such a way that sequential fault-localization methods can be extended to multi-threaded programs.
Lattice Index Codes from Algebraic Number Fields
Venue: arXiv cs.IT 2015
Year: 2015

Broadcasting $K$ independent messages to multiple users where each user demands all the messages and has a subset of the messages as side information is studied. Recently, Natarajan, Hong, and Viterbo proposed a novel broadcasting strategy called lattice index coding which uses lattices constructed over some principal ideal domains (PIDs) for transmission and showed that this scheme provides uniform side information gains. In this paper, we generalize this strategy to general rings of algebraic integers of number fields which may not be PIDs. Upper and lower bounds on the side information gains for the proposed scheme constructed over some interesting classes of number fields are provided and are shown to coincide asymptotically in message rates. This generalization substantially enlarges the design space and partially includes the scheme by Natarajan, Hong, and Viterbo as a special case. Perhaps more importantly, in addition to side information gains, the proposed lattice index codes benefit from diversity gains inherent in constellations carved from number fields when used over Rayleigh fading channel. Some interesting examples are also provided for which the proposed scheme allows all the messages to be from the same field.
A Class of Deterministic Sensing Matrices and Their Application in Harmonic Detection
Venue: arXiv cs.IT 2015
Year: 2015

In this paper, a class of deterministic sensing matrices are constructed by selecting rows from Fourier matrices. These matrices have better performance in sparse recovery than random partial Fourier matrices. The coherence and restricted isometry property of these matrices are given to evaluate their capacity as compressive sensing matrices. In general, compressed sensing requires random sampling in data acquisition, which is difficult to implement in hardware. By using these sensing matrices in harmonic detection, a deterministic sampling method is provided. The frequencies and amplitudes of the harmonic components are estimated from under-sampled data. The simulations show that this under-sampled method is feasible and valid in noisy environments.
Modeling and visualizing networked multi-core embedded software energy consumption
Venue: arXiv cs.DC 2015
Year: 2015

In this report we present a network-level multi-core energy model and a software development process workflow that allows software developers to estimate the energy consumption of multi-core embedded programs. This work focuses on a high performance, cache-less and timing predictable embedded processor architecture, XS1. Prior modelling work is improved to increase accuracy, then extended to be parametric with respect to voltage and frequency scaling (VFS) and then integrated into a larger scale model of a network of interconnected cores. The modelling is supported by enhancements to an open source instruction set simulator to provide the first network timing aware simulations of the target architecture. Simulation based modelling techniques are combined with methods of results presentation to demonstrate how such work can be integrated into a software developer's workflow, enabling the developer to make informed, energy aware coding decisions. A set of single-, multi-threaded and multi-core benchmarks are used to exercise and evaluate the models and provide use case examples for how results can be presented and interpreted. The models all yield accuracy within an average +/-5 % error margin.
Approximating the Smallest Spanning Subgraph for 2-Edge-Connectivity in Directed Graphs
Venue: arXiv cs.DS 2015
Year: 2015

Let $G$ be a strongly connected directed graph. We consider the following three problems, where we wish to compute the smallest strongly connected spanning subgraph of $G$ that maintains respectively: the $2$-edge-connected blocks of $G$ (\textsf{2EC-B}); the $2$-edge-connected components of $G$ (\textsf{2EC-C}); both the $2$-edge-connected blocks and the $2$-edge-connected components of $G$ (\textsf{2EC-B-C}). All three problems are NP-hard, and thus we are interested in efficient approximation algorithms. For \textsf{2EC-C} we can obtain a $3/2$-approximation by combining previously known results. For \textsf{2EC-B} and \textsf{2EC-B-C}, we present new $4$-approximation algorithms that run in linear time. We also propose various heuristics to improve the size of the computed subgraphs in practice, and conduct a thorough experimental study to assess their merits in practical scenarios.
Provably Correct Systems: Community, connections, and citations
Venue: arXiv cs.DL 2015
Year: 2015

The original European ESPRIT ProCoS I and II projects on Provably Correct Systems} took place around a quarter of a century ago. Since then the legacy of the initiative has spawned many researchers with careers in formal methods. One of the leaders on the ProCoS projects was Ernst-Rüdiger Olderog. This paper charts the influence of the ProCoS projects and the subsequent ProCoS-WG Working Group, using Prof. Dr Olderog as an example. The community of researchers surrounding an initiative such as ProCoS is considered in the context of the social science concept of a Community of Practice (CoP) and the collaborations undertaken through coauthorship of and citations to publications. Consideration of citation metrics is also included.
The robustness of multiplex networks under layer node-based attack
Venue: arXiv cs.SI 2015
Year: 2015

From transportation networks to complex infrastructures, and to social and economic networks, a large variety of systems can be described in terms of multiplex networks formed by a set of nodes interacting through different network layers. Network robustness, as one of the most successful application areas of complex networks, has also attracted great interest in both theoretical and empirical researches. However, the vast majority of existing researches mainly focus on the robustness of single-layer networks an interdependent networks, how multiplex networks respond to potential attack is still short of further exploration. Here we study the robustness of multiplex networks under two attack strategies: layer node-based random attack and layer node-based targeted attack. A theoretical analysis framework is proposed to calculate the critical threshold and the size of giant component of multiplex networks when a fraction of layer nodes are removed randomly or intentionally. Via numerous simulations, it is unveiled that the theoretical method can accurately predict the threshold and the size of giant component, irrespective of attack strategies. Moreover, we also compare the robustness of multiplex networks under multiplex node-based attack and layer node-based attack, and find that layer node-based attack makes multiplex networks more vulnerable, regardless of average degree and underlying topology. Our finding may shed new light on the protection of multiplex networks.
Compatible Value Gradients for Reinforcement Learning of Continuous Deep Policies
Venue: arXiv cs.LG 2015
Year: 2015

This paper proposes GProp, a deep reinforcement learning algorithm for continuous policies with compatible function approximation. The algorithm is based on two innovations. Firstly, we present a temporal-difference based method for learning the gradient of the value-function. Secondly, we present the deviator-actor-critic (DAC) model, which comprises three neural networks that estimate the value function, its gradient, and determine the actor's policy respectively. We evaluate GProp on two challenging tasks: a contextual bandit problem constructed from nonparametric regression datasets that is designed to probe the ability of reinforcement learning algorithms to accurately estimate gradients; and the octopus arm, a challenging reinforcement learning benchmark. GProp is competitive with fully supervised methods on the bandit task and achieves the best performance to date on the octopus arm.
Self-Correlation and Maximum Independence in Finite Relations
Venue: arXiv cs.DM 2015
Year: 2015

We consider relations with no order on their attributes as in Database Theory. An independent partition of the set of attributes S of a finite relation R is any partition X of S such that the join of the projections of R over the elements of X yields R. Identifying independent partitions has many applications and corresponds conceptually to revealing orthogonality between sets of dimensions in multidimensional point spaces. A subset of S is termed self-correlated if there is a value of each of its attributes such that no tuple of R contains all those values. This paper uncovers a connection between independence and self-correlation, showing that the maximum independent partition is the least fixed point of a certain inflationary transformer alpha that operates on the finite lattice of partitions of S. alpha is defined via the minimal self-correlated subsets of S. We use some additional properties of alpha to show the said fixed point is still the limit of the standard approximation sequence, just as in Kleene's well-known fixed point theorem for continuous functions.
The Arity Hierarchy in the Polyadic $μ$-Calculus
Venue: arXiv cs.LO 2015
Year: 2015

The polyadic mu-calculus is a modal fixpoint logic whose formulas define relations of nodes rather than just sets in labelled transition systems. It can express exactly the polynomial-time computable and bisimulation-invariant queries on finite graphs. In this paper we show a hierarchy result with respect to expressive power inside the polyadic mu-calculus: for every level of fixpoint alternation, greater arity of relations gives rise to higher expressive power. The proof uses a diagonalisation argument.
ptp++: A Precision Time Protocol Simulation Model for OMNeT++ / INET
Venue: arXiv cs.NI 2015
Year: 2015

Precise time synchronization is expected to play a key role in emerging distributed and real-time applications such as the smart grid and Internet of Things (IoT) based applications. The Precision Time Protocol (PTP) is currently viewed as one of the main synchronization solutions over a packet-switched network, which supports microsecond synchronization accuracy. In this paper, we present a PTP simulation model for OMNeT++ INET, which allows to investigate the synchronization accuracy under different network configurations and conditions. To show some illustrative simulation results using the developed module, we investigate on the network load fluctuations and their impacts on the PTP performance by considering a network with class-based quality-of-service (QoS) support. The simulation results show that the network load significantly affects the network delay symmetry, and investigate a new technique called class probing to improve the PTP accuracy and mitigate the load fluctuation effects.
Agent enabled Mining of Distributed Protein Data Banks
Venue: arXiv cs.CE 2015
Year: 2015

Mining biological data is an emergent area at the intersection between bioinformatics and data mining (DM). The intelligent agent based model is a popular approach in constructing Distributed Data Mining (DDM) systems to address scalable mining over large scale distributed data. The nature of associations between different amino acids in proteins has also been a subject of great anxiety. There is a strong need to develop new models and exploit and analyze the available distributed biological data sources. In this study, we have designed and implemented a multi-agent system (MAS) called Agent enriched Quantitative Association Rules Mining for Amino Acids in distributed Protein Data Banks (AeQARM-AAPDB). Such globally strong association rules enhance understanding of protein composition and are desirable for synthesis of artificial proteins. A real protein data bank is used to validate the system.
Online Buy-at-Bulk Network Design
Venue: arXiv cs.DS 2015
Year: 2015

We present the first non-trivial online algorithms for the non-uniform, multicommodity buy-at-bulk (MC-BB) network design problem in undirected and directed graphs. Our competitive ratios qualitatively match the best known approximation factors for the corresponding offline problems. The main engine for our results is an online reduction theorem of MC-BB problems to their single-sink (SS-BB) counterparts. We use the concept of junction-tree solutions (Chekuri et al., FOCS 2006) that play an important role in solving the offline versions of the problem via a greedy subroutine -- an inherently offline procedure. Our main technical contribution is in designing an online algorithm using only the existence of good junction-trees to reduce an MC-BB instance to multiple SS-BB sub-instances. Along the way, we also give the first non-trivial online node-weighted/directed single-sink buy-at-bulk algorithms. In addition to the new results, our generic reduction also yields new proofs of recent results for the online node-weighted Steiner forest and online group Steiner forest problems.
Simple, Flexible, and Interoperable SCADA System Based on Agent Technology
Venue: arXiv cs.SY 2015
Year: 2015

SCADA (Supervisory Control and Data Acquisition) is concerned with gathering process information from industrial control processes found in utilities such as power grids, water networks, transportation, manufacturing, etc., to provide the human operators with the required real-time access to industrial processes to be monitored and controlled either locally (on-site)or remotely (i.e., through Internet). Conventional solutions such as custom SCADA packages, custom communication protocols, and centralized architectures are no longer appropriate for engineering this type of systems because of their highly distribution and their uncertain continuously changing working environments. Multi-agent systems (MAS) appeared as a new architectural style for engineering complex and highly dynamic applications such as SCADA systems. In this paper, we propose an approach for simply developing flexible and interoperable SCADA systems based on the integration of MAS and OPC process protocol. The proposed SCADA system has the following advantages: 1) simple (easier to be implemented); 2) flexible (able to adapt to its environment dynamic changes); and 3) interoperable (relative to the underlying control systems, which belongs to diverse of vendors). The applicability of the proposed approach is demonstrated by a real case study example carried out in a paper mill.
Gibbs Sampling Strategies for Semantic Perception of Streaming Video Data
Venue: arXiv cs.RO 2015
Year: 2015

Topic modeling of streaming sensor data can be used for high level perception of the environment by a mobile robot. In this paper we compare various Gibbs sampling strategies for topic modeling of streaming spatiotemporal data, such as video captured by a mobile robot. Compared to previous work on online topic modeling, such as o-LDA and incremental LDA, we show that the proposed technique results in lower online and final perplexity, given the realtime constraints.
An Epsilon Hierarchical Fuzzy Twin Support Vector Regression
Venue: arXiv cs.AI 2015
Year: 2015

The research presents epsilon hierarchical fuzzy twin support vector regression based on epsilon fuzzy twin support vector regression and epsilon twin support vector regression. Epsilon FTSVR is achieved by incorporating trapezoidal fuzzy numbers to epsilon TSVR which takes care of uncertainty existing in forecasting problems. Epsilon FTSVR determines a pair of epsilon insensitive proximal functions by solving two related quadratic programming problems. The structural risk minimization principle is implemented by introducing regularization term in primal problems of epsilon FTSVR. This yields dual stable positive definite problems which improves regression performance. Epsilon FTSVR is then reformulated as epsilon HFTSVR consisting of a set of hierarchical layers each containing epsilon FTSVR. Experimental results on both synthetic and real datasets reveal that epsilon HFTSVR has remarkable generalization performance with minimum training time.
A Survey on Operational State Complexity
Venue: arXiv cs.FL 2015
Year: 2015

Descriptional complexity is the study of the conciseness of the various models representing formal languages. The state complexity of a regular language is the size, measured by the number of states of the smallest, either deterministic or nondeterministic, finite automaton that recognises it. Operational state complexity is the study of the state complexity of operations over languages. In this survey, we review the state complexities of individual regularity preserving language operations on regular and some subregular languages. Then we revisit the state complexities of the combination of individual operations. We also review methods of estimation and approximation of state complexity of more complex combined operations.
A New Method For Digital Watermarking Based on Combination of DCT and PCA
Venue: arXiv cs.MM 2015
Year: 2015

In the digital watermarking with DCT method,the watermark is located within a range of DCT coefficients of the cover image. In this paper to use the low-frequency band, a new method is proposed by using a combination of the DCT and PCA transform. The proposed method is compared to other DCT methods, our method is robust and keeps the quality of cover image, also increases capacity of the watermarking.
Fixed-time cluster synchronization for complex networks via pinning control
Venue: arXiv cs.SY 2015
Year: 2015

In this paper, the fixed-time cluster synchronization problem for complex networks via pinning control is discussed. Fixed-time synchronization has been a hot topic in recent years, which means that the network can achieve synchronization in finite-time and the settling time is bounded by a constant for any initial values. To realize the fixed-time cluster synchronization, a simple distributed protocol by pinning control technique is designed, whose validity is rigorously proved, and some sufficient criteria for fixed-time cluster synchronization are also obtained. Especially, when the cluster number is one, the cluster synchronization becomes the complete synchronization problem; when the intrinsic dynamics for each node is missed, the fixed-time cluster synchronization becomes the fixed-time cluster (or complete) consensus problem; when the network has only one node, the coupling term between nodes will disappear, and the synchronization problem becomes the simplest master-slave case, which also includes the stability problem for nonlinear systems like neural networks. All these cases are also discussed. Finally, numerical simulations are presented to demonstrate the correctness of obtained theoretical results.
OCR accuracy improvement on document images through a novel pre-processing approach
Venue: arXiv cs.CV 2015
Year: 2015

Digital camera and mobile document image acquisition are new trends arising in the world of Optical Character Recognition and text detection. In some cases, such process integrates many distortions and produces poorly scanned text or text-photo images and natural images, leading to an unreliable OCR digitization. In this paper, we present a novel nonparametric and unsupervised method to compensate for undesirable document image distortions aiming to optimally improve OCR accuracy. Our approach relies on a very efficient stack of document image enhancing techniques to recover deformation of the entire document image. First, we propose a local brightness and contrast adjustment method to effectively handle lighting variations and the irregular distribution of image illumination. Second, we use an optimized greyscale conversion algorithm to transform our document image to greyscale level. Third, we sharpen the useful information in the resulting greyscale image using Un-sharp Masking method. Finally, an optimal global binarization approach is used to prepare the final document image to OCR recognition. The proposed approach can significantly improve text detection rate and optical character recognition accuracy. To demonstrate the efficiency of our approach, an exhaustive experimentation on a standard dataset is presented.
MiXiM, PAWiS, and STEAM-Sim Integration - Combining Channel Models, Energy Awareness, and Real-life Application Code
Venue: arXiv cs.NI 2015
Year: 2015

After a decade of research in the field of wireless sensor networks (WSNs) there are still open issues. WSNs impose several severe requirements regarding energy consumption, processing capabilities, mobility, and robustness of wireless transmissions. Simulation has shown to be the most cost-efficient approach for evaluation of WSNs, thus a number of simulators are available. Unfortunately, these simulation environments typically consider WSNs from a special point of view. In this work we present the integration of three such specialized frameworks, namely MiXiM, PAWiS, and STEAM-Sim. This integration combines the strengths of the single frameworks such as realistic channel models, mobility patterns, accurate energy models, and inclusion of real-life application code. The result is a new simulation environment which enables a more general consideration of WSNs. We implemented and verified our proposed concept by means of static and mobile scenarios. As the presented results show, the combined framework gives the same results regarding the functionality and energy consumption as our "golden model". Therefore the system integration was successful and the framework is ready to be used by the community.
Implementation of PFC and RCM for RoCEv2 Simulation in OMNeT++
Venue: arXiv cs.NI 2015
Year: 2015

As traffic patterns and network topologies become more and more complicated in current enterprise data centers and TOP500 supercomputers, the probability of network congestion increases. If no countermeasures are taken, network congestion causes long communication delays and degrades network performance. A congestion control mechanism is often provided to reduce the consequences of congestion. However, it is usually difficult to configure and activate a congestion control mechanism in production clusters and supercomputers due to concerns that it may negatively impact jobs if the mechanism is not appropriately configured. Therefore, simulations for these situations are necessary to identify congestion points and sources, and more importantly, to determine optimal settings that can be utilized to reduce congestion in those complicated networks. In this paper, we use OMNeT++ to implement the IEEE 802.1Qbb Priority-based Flow Control (PFC) and RoCEv2 Congestion Management (RCM) in order to simulate clusters with RoCEv2 interconnects.
Key Exchange Protocol in the Trusted Data Servers Context
Venue: arXiv cs.CR 2015
Year: 2015

The aim of this technical report is to complement the work in [To et al. 2014] by proposing a Group Key Exchange protocol so that the Querier and TDSs (and TDSs themselves) can securely create and exchange the shared key. Then, the security of this protocol is formally proved using the game-based model. Finally, we perform the comparison between this protocol and other related works.