OpenRaiser/Intern-Atlas huggingface dataset:
Co-design of output feedback laws and event-triggering conditions for linear systems
Venue: arXiv cs.SY 2014
Year: 2014

We present a procedure to simultaneously design the output feedback law and the event-triggering condition to stabilize linear systems. The closed-loop system is shown to satisfy a global asymptotic stability property and the existence of a strictly positive minimum amount of time between two transmissions is guaranteed. The event-triggered controller is obtained by solving linear matrix inequalities (LMIs). We then exploit the flexibility of the method to maximize the guaranteed minimum amount of time between two transmissions. Finally, we provide a (heuristic) method to reduce the amount of transmissions, which is supported by numerical simulations.
The Power of Proofs: New Algorithms for Timed Automata Model Checking (with Appendix)
Venue: arXiv cs.FL 2014
Year: 2014

This paper presents the first model-checking algorithm for an expressive modal mu-calculus over timed automata, $L^{\mathit{rel}, \mathit{af}}_{ν,μ}$, and reports performance results for an implementation. This mu-calculus contains extended time-modality operators and can express all of TCTL. Our algorithmic approach uses an "on-the-fly" strategy based on proof search as a means of ensuring high performance for both positive and negative answers to model-checking questions. In particular, a set of proof rules for solving model-checking problems are given and proved sound and complete; we encode our algorithm in these proof rules and model-check a property by constructing a proof (or showing none exists) using these rules. One noteworthy aspect of our technique is that we show that verification performance can be improved with \emph{derived rules}, whose correctness can be inferred from the more primitive rules on which they are based. In this paper, we give the basic proof rules underlying our method, describe derived proof rules to improve performance, and compare our implementation of this model checker to the UPPAAL tool.
Cross-layer Theoretical Analysis of NC-aided Cooperative ARQ Protocols in Correlated Shadowed Environments (Extended Version)
Venue: arXiv cs.NI 2014
Year: 2014

In this paper, we propose a cross-layer analytical model for the study of Network Coding (NC)-based Automatic Repeat reQuest (ARQ) Medium Access Control (MAC) protocols in correlated slow faded (shadowed) environments, where two end nodes are assisted by a cluster of relays to exchange data packets. The goal of our work is threefold: i) to provide general Physical (PHY) layer theoretical expressions for estimating crucial network parameters (i.e., network outage probability and expected size of the active relay set), applicable in two-way communications, ii) to demonstrate how these expressions are incorporated in theoretical models of the upper layers (i.e., MAC), and iii) to study the performance of a recently proposed NC-aided Cooperative ARQ (NCCARQ) MAC protocol under correlated shadowing conditions. Extensive Monte Carlo experiments have been carried out to validate the efficiency of the developed analytical model and to investigate the realistic performance of NCCARQ. Our results indicate that the number of active relays is independent of the shadowing correlation in the wireless links and reveal intriguing trade-offs between throughput and energy efficiency, highlighting the importance of cross-layer approaches for the assessment of cooperative MAC protocols.
Design and Implementation of Parallel Debugger and Profiler for MPJ Express
Venue: arXiv cs.DC 2014
Year: 2014

MPJ Express is a messaging system that allows computational scientists to write and execute parallel Java applications on High Performance Computing (HPC) hardware. Despite its successful adoption in the Java HPC community, the MPJ Express software currently does not provide any support for debugging and profiling parallel applications and hence forces its users to rely on manual and tedious debugging/profiling methods. Support for such tools is essential to help application developers increase their overall productivity. To address this we have developed debugging and profiling tools for MPJ Express, which are the main topic of this paper. Key design goals for these tools include: 1) maintain compatibility with existing logging, debugging, and visualizing tools, 2) build these tools by extending existing debugging/profiling tools instead of reinventing the wheel. The first tool, named MPJDebug, builds on the open-source Eclipse Integrated Development Environment (IDE). It provides an Eclipse-based plugin developed using the Eclipse Plugin Development Environment (PDE). The default Eclipse debugger currently does not support debugging parallel applications running on a compute cluster. The second tool, named MPJProf, is a utility based on Tuning and Analysis Utility (TAU)-an open-source performance evaluation tool. Our goal here is to exploit TAU to profile Java applications parallelized using MPJ Express by generating profiles and traces, which can later be visualized using existing tools like paraprof and Jumpshot. Towards the end of the paper, we quantify the overhead of using MPJProf, which we found to be negligible in the profiling stage of parallel application development.
Modeling Non-Progressive Phenomena for Influence Propagation
Venue: arXiv cs.SI 2014
Year: 2014

Recent work on modeling influence propagation focus on progressive models, i.e., once a node is influenced (active) the node stays in that state and cannot become inactive. However, this assumption is unrealistic in many settings where nodes can transition between active and inactive states. For instance, a user of a social network may stop using an app and become inactive, but again activate when instigated by a friend, or when the app adds a new feature or releases a new version. In this work, we study such non-progressive phenomena and propose an efficient model of influence propagation. Specifically, we model in influence propagation as a continuous-time Markov process with 2 states: active and inactive. Such a model is both highly scalable (we evaluated on graphs with over 2 million nodes), 17-20 times faster, and more accurate for estimating the spread of influence, as compared with state-of-the-art progressive models for several applications where nodes may switch states.
Sets, the Axiom of Choice, And All That: A Tutorial
Venue: arXiv cs.LO 2014
Year: 2014

This tutorial deal with the Axiom of Choice and some of its applications to topics related to Computer Science. We will see that the Axiom of Choice is equivalent to some well-known proof principles like Zorn's Lemma or Tuckey's Maximality Principle. We try to touch upon some topics, which appear to be important for developing mathematical structures within computer science.
Finding Maximum k-Cliques Faster using Lazy Global Domination
Venue: arXiv cs.DS 2014
Year: 2014

A clique in a graph is a set of vertices, each of which is adjacent to every other vertex in this set. A k-clique relaxes this requirement, requiring vertices to be within a distance k of each other, rather than directly adjacent. In theory, a maximum clique algorithm can easily be adapted to solve the maximum k-clique problem. We use a state of the art maximum clique algorithm to show that this is feasible in practice, and introduce a lazy global domination rule which sometimes vastly reduces the search space. We include experimental results for a range of real-world and benchmark graphs, and a detailed look at random graphs.
Turing degree spectra of minimal subshifts
Venue: arXiv cs.FL 2014
Year: 2014

Subshifts are shift invariant closed subsets of $Σ^{\mathbb{Z}^d}$ , minimal subshifts are subshifts in which all points contain the same patterns. It has been proved by Jeandel and Vanier that the Turing degree spectra of non-periodic minimal subshifts always contain the cone of Turing degrees above any of its degree. It was however not known whether each minimal subshift's spectrum was formed of exactly one cone or not. We construct inductively a minimal subshift whose spectrum consists of an uncountable number of cones with disjoint base.
Plane-Walking Automata
Venue: arXiv cs.FL 2014
Year: 2014

In this article, we study classes of multidimensional subshifts defined by multihead finite automata, in particular the hierarchy of classes of subshifts defined as the number of heads grows. The hierarchy collapses on the third level, where all co-recursively enumerable subshifts are obtained in every dimension. We also compare these classes to SFTs and sofic shifts. We are unable to separate the second and third level of the hierarchy in one and two dimensions, and suggest a related open problem for two-counter machines.
Non-Standard Words as Features for Text Categorization
Venue: arXiv cs.CL 2014
Year: 2014

This paper presents categorization of Croatian texts using Non-Standard Words (NSW) as features. Non-Standard Words are: numbers, dates, acronyms, abbreviations, currency, etc. NSWs in Croatian language are determined according to Croatian NSW taxonomy. For the purpose of this research, 390 text documents were collected and formed the SKIPEZ collection with 6 classes: official, literary, informative, popular, educational and scientific. Text categorization experiment was conducted on three different representations of the SKIPEZ collection: in the first representation, the frequencies of NSWs are used as features; in the second representation, the statistic measures of NSWs (variance, coefficient of variation, standard deviation, etc.) are used as features; while the third representation combines the first two feature sets. Naive Bayes, CN2, C4.5, kNN, Classification Trees and Random Forest algorithms were used in text categorization experiments. The best categorization results are achieved using the first feature set (NSW frequencies) with the categorization accuracy of 87%. This suggests that the NSWs should be considered as features in highly inflectional languages, such as Croatian. NSW based features reduce the dimensionality of the feature space without standard lemmatization procedures, and therefore the bag-of-NSWs should be considered for further Croatian texts categorization experiments.
Bug Hunting By Computing Range Reduction
Venue: arXiv cs.LO 2014
Year: 2014

We describe a method of model checking called Computing Range Reduction (CRR). The CRR method is based on derivation of clauses that reduce the set of traces of reachable states in such a way that at least one counterexample remains (if any). These clauses are derived by a technique called Partial Quantifier Elimination (PQE). Given a number n, the CRR method finds a counterexample of length less or equal to n or proves that such a counterexample does not exist. We show experimentally that a PQE-solver we developed earlier can be efficiently applied to derivation of constraining clauses for transition relations of realistic benchmarks. One of the most appealing features of the CRR method is that it can potentially find long counterexamples. This is the area where it can beat model checkers computing reachable states (or their approximations as in IC3) or SAT-based methods of bounded model checking. PQE cannot be efficiently simulated by a SAT-solver. This is important because the current research in model checking is dominated by SAT-based algorithms. The CRR method is a reminder that one should not put all eggs in one basket.
Usability Engineering of Games: A Comparative Analysis of Measuring Excitement Using Sensors, Direct Observations and Self-Reported Data
Venue: arXiv cs.HC 2014
Year: 2014

Usability engineering and usability testing are concepts that continue to evolve. Interesting research studies and new ideas come up every now and then. This paper tests the hypothesis of using an EDA based physiological measurements as a usability testing tool by considering three measures which are observers opinions, self reported data and EDA based physiological sensor data. These data were analyzed comparatively and statistically. It concludes by discussing the findings that has been obtained from those subjective and objective measures, which partially supports the hypothesis.
A Variant of the Maximum Weight Independent Set Problem
Venue: arXiv cs.DS 2014
Year: 2014

We study a natural extension of the Maximum Weight Independent Set Problem (MWIS), one of the most studied optimization problems in Graph algorithms. We are given a graph $G=(V,E)$, a weight function $w: V \rightarrow \mathbb{R^+}$, a budget function $b: V \rightarrow \mathbb{Z^+}$, and a positive integer $B$. The weight (resp. budget) of a subset of vertices is the sum of weights (resp. budgets) of the vertices in the subset. A $k$-budgeted independent set in $G$ is a subset of vertices, such that no pair of vertices in that subset are adjacent, and the budget of the subset is at most $k$. The goal is to find a $B$-budgeted independent set in $G$ such that its weight is maximum among all the $B$-budgeted independent sets in $G$. We refer to this problem as MWBIS. Being a generalization of MWIS, MWBIS also has several applications in Scheduling, Wireless networks and so on. Due to the hardness results implied from MWIS, we study the MWBIS problem in several special classes of graphs. We design exact algorithms for trees, forests, cycle graphs, and interval graphs. In unweighted case we design an approximation algorithm for $d+1$-claw free graphs whose approximation ratio ($d$) is competitive with the approximation ratio ($\frac{d}{2}$) of MWIS (unweighted). Furthermore, we extend Baker's technique \cite{Baker83} to get a PTAS for MWBIS in planar graphs.
Ad Hoc Microphone Array Calibration: Euclidean Distance Matrix Completion Algorithm and Theoretical Guarantees
Venue: arXiv cs.SD 2014
Year: 2014

This paper addresses the problem of ad hoc microphone array calibration where only partial information about the distances between microphones is available. We construct a matrix consisting of the pairwise distances and propose to estimate the missing entries based on a novel Euclidean distance matrix completion algorithm by alternative low-rank matrix completion and projection onto the Euclidean distance space. This approach confines the recovered matrix to the EDM cone at each iteration of the matrix completion algorithm. The theoretical guarantees of the calibration performance are obtained considering the random and locally structured missing entries as well as the measurement noise on the known distances. This study elucidates the links between the calibration error and the number of microphones along with the noise level and the ratio of missing distances. Thorough experiments on real data recordings and simulated setups are conducted to demonstrate these theoretical insights. A significant improvement is achieved by the proposed Euclidean distance matrix completion algorithm over the state-of-the-art techniques for ad hoc microphone array calibration.
Online networks destroy social trust
Venue: arXiv cs.CY 2014
Year: 2014

Studies in the social capital literature have documented two stylised facts: first, a decline in measures of social participation has occurred in many OECD countries. Second, and more recently, the success of social networking sites (SNSs) has resulted in a steep rise in online social participation. Our study adds to this body of research by conducting the first empirical assessment of how online networking affects two economically relevant aspects of social capital, i.e. trust and sociability. We address endogeneity in online networking by exploiting technological characteristics of the pre-existing voice telecommunication infrastructures that exogenously determined the availability of broadband for high-speed Internet. We find that participation in SNSs such as Facebook and Twitter has a positive effect on face-to-face interactions. However, social trust decreases with online interactions. We argue that the rising practice of hate speech may play a crucial role in the destruction of trust.
Searching for a Unique Style in Soccer
Venue: arXiv cs.SI 2014
Year: 2014

Is it possible to have a unique, recognizable style in soccer nowadays? We address this question by proposing a method to quantify the motif characteristics of soccer teams based on their pass networks. We introduce the the concept of "flow motifs" to characterize the statistically significant pass sequence patterns. It extends the idea of the network motifs, highly significant subgraphs that usually consists of three or four nodes. The analysis of the motifs in the pass networks allows us to compare and differentiate the styles of different teams. Although most teams tend to apply homogenous style, surprisingly, a unique strategy of soccer exists. Specifically, FC Barcelona's famous tiki-taka does not consist of uncountable random passes but rather has a precise, finely constructed structure.
Visualization of Co-Readership Patterns from an Online Reference Management System
Venue: arXiv cs.DL 2014
Year: 2014

In this paper, we analyze the adequacy and applicability of readership statistics recorded in social reference management systems for creating knowledge domain visualizations. First, we investigate the distribution of subject areas in user libraries of educational technology researchers on Mendeley. The results show that around 69% of the publications in an average user library can be attributed to a single subject area. Then, we use co-readership patterns to map the field of educational technology. The resulting visualization prototype, based on the most read publications in this field on Mendeley, reveals 13 topic areas of educational technology research. The visualization is a recent representation of the field: 80% of the publications included were published within ten years of data collection. The characteristics of the readers, however, introduce certain biases to the visualization. Knowledge domain visualizations based on readership statistics are therefore multifaceted and timely, but it is important that the characteristics of the underlying sample are made transparent.
"Share and Enjoy": Publishing Useful and Usable Scientific Models
Venue: arXiv cs.CE 2014
Year: 2014

The reproduction and replication of reported scientific results is a hot topic within the academic community. The retraction of numerous studies from a wide range of disciplines, from climate science to bioscience, has drawn the focus of many commentators, but there exists a wider socio-cultural problem that pervades the scientific community. Sharing code, data and models often requires extra effort; this is currently seen as a significant overhead that may not be worth the time investment. Automated systems, which allow easy reproduction of results, offer the potential to incentivise a culture change and drive the adoption of new techniques to improve the efficiency of scientific exploration. In this paper, we discuss the value of improved access and sharing of the two key types of results arising from work done in the computational sciences: models and algorithms. We propose the development of an integrated cloud-based system underpinning computational science, linking together software and data repositories, toolchains, workflows and outputs, providing a seamless automated infrastructure for the verification and validation of scientific models and in particular, performance benchmarks.
Modeling Cyber-Physical Systems: Model-Driven Specification of Energy Efficient Buildings
Venue: arXiv cs.SE 2014
Year: 2014

A lot of current buildings are operated energy inefficient and offer a great potential to reduce the overall energy consumption and CO2 emission. Detecting these inefficiencies is a complicated task and needs domain experts that are able to identify them. Most approaches try to support detection by focussing on monitoring the building's operation and visualizing data. Instead our approach focuses on using techniques taken from the cyber-physical systems' modeling domain. We create a model of the building and show how we constrain the model by OCL-like rules to support a sound specification which can be matched against monitoring results afterwards. The paper presents our domain-specific language for modeling buildings and technical facilities that is implemented in a software-based tool used by domain experts and thus hopefully providing a suitable contribution to modeling the cyber-physical world.
On Decoding of DVR-Based Linear Network Codes
Venue: arXiv cs.IT 2014
Year: 2014

The conventional theory of linear network coding (LNC) is only over acyclic networks. Convolutional network coding (CNC) applies to all networks. It is also a form of LNC, but the linearity is w.r.t. the ring of rational power series rather than the field of data symbols. CNC has been generalized to LNC w.r.t. any discrete valuation ring (DVR) in order for flexibility in applications. For a causal DVR-based code, all possible source-generated messages form a free module, while incoming coding vectors to a receiver span the \emph{received submodule}. An existing \emph{time-invariant decoding} algorithm is at a delay equal to the largest valuation among all invariant factors of the received submodule. This intrinsic algebraic attribute is herein proved to be the optimal decoding delay. Meanwhile, \emph{time-variant decoding} is formulated. The meaning of time-invariant decoding delay gets a new interpretation through being a special case of the time-variant counterpart. The optimal delay turns out to be the same for time-variant decoding, but the decoding algorithm is more flexible in terms of decodability check and decoding matrix design. All results apply, in particular, to CNC.
An LSH Index for Computing Kendall's Tau over Top-k Lists
Venue: arXiv cs.DB 2014
Year: 2014

We consider the problem of similarity search within a set of top-k lists under the Kendall's Tau distance function. This distance describes how related two rankings are in terms of concordantly and discordantly ordered items. As top-k lists are usually very short compared to the global domain of possible items to be ranked, creating an inverted index to look up overlapping lists is possible but does not capture tight enough the similarity measure. In this work, we investigate locality sensitive hashing schemes for the Kendall's Tau distance and evaluate the proposed methods using two real-world datasets.
An Approach for Assessing Clustering of Households by Electricity Usage
Venue: arXiv cs.CE 2014
Year: 2014

How a household varies their regular usage of electricity is useful information for organisations to allow accurate targeting of behaviour modification initiatives with the aim of improving the overall efficiency of the electricity network. The variability of regular activities in a household is one possible indication of that household's willingness to accept incentives to change their behaviour. An approach is presented for identifying a way of representing the variability of a household's behaviour and developing an efficient way of clustering the households, using these measures of variability, into a few, usable groupings. To evaluate the effectiveness of the variability measures, a number of cluster validity indexes are explored with regard to how the indexes vary with the number of clusters, the number of attributes, and the quality of the attributes. The Cluster Dispersion Indicator (CDI) and the Davies-Boulden Indicator (DBI) are selected for future work developing various indicators of household behaviour variability. The approach is tested using data from 180 UK households monitored for over a year at a sampling interval of 5 minutes. Data is taken from the evening peak electricity usage period of 4pm to 8pm.