OpenRaiser/Intern-Atlas huggingface dataset:
Towards an Extension of the 2-tuple Linguistic Model to Deal With Unbalanced Linguistic Term sets
Venue: arXiv cs.AI 2013
Year: 2013

In the domain of Computing with words (CW), fuzzy linguistic approaches are known to be relevant in many decision-making problems. Indeed, they allow us to model the human reasoning in replacing words, assessments, preferences, choices, wishes... by ad hoc variables, such as fuzzy sets or more sophisticated variables. This paper focuses on a particular model: Herrera & Martinez' 2-tuple linguistic model and their approach to deal with unbalanced linguistic term sets. It is interesting since the computations are accomplished without loss of information while the results of the decision-making processes always refer to the initial linguistic term set. They propose a fuzzy partition which distributes data on the axis by using linguistic hierarchies to manage the non-uniformity. However, the required input (especially the density around the terms) taken by their fuzzy partition algorithm may be considered as too much demanding in a real-world application, since density is not always easy to determine. Moreover, in some limit cases (especially when two terms are very closed semantically to each other), the partition doesn't comply with the data themselves, it isn't close to the reality. Therefore we propose to modify the required input, in order to offer a simpler and more faithful partition. We have added an extension to the package jFuzzyLogic and to the corresponding script language FCL. This extension supports both 2-tuple models: Herrera & Martinez' and ours. In addition to the partition algorithm, we present two aggregation algorithms: the arithmetic means and the addition. We also discuss these kinds of 2-tuple models.
Security Policies for WFMS with Rich Business Logic - A Model Suitable for Analysis
Venue: arXiv cs.CR 2013
Year: 2013

This paper introduces a formal metamodel for the specification of security policies for workflows in online service systems designed to be suitable for the modeling and analysis of complex business-related rules as well as traditional access control. A translation of the model into a colored Petri net is shown and an example of policy for an online banking system is described. By writing predicates for querying the resulting state-space of the Petri net, a connection between the formalized model and a higher-level description of the security policy can be made, indicating the feasibility of the intended method for validating such descriptions. Thanks to the independent nature among tasks related to different business services, represented by restrictions in the information flow within the metamodel, the state-space may be fractioned for analysis, avoiding the state-space explosion problem. Related existing models are discussed, pointing the gain in expressiveness of business rules and the analysis of insecure state paths rather than simply insecure states in the proposed model. The successful representation and analysis of the policy from the example combined with reasonings for the general case attest the adequacy of the proposed approach for its intended application.
Low-Complexity Channel Estimation in Large-Scale MIMO using Polynomial Expansion
Venue: arXiv cs.IT 2013
Year: 2013

This paper considers pilot-based channel estimation in large-scale multiple-input multiple-output (MIMO) communication systems, also known as "massive MIMO". Unlike previous works on this topic, which mainly considered the impact of inter-cell disturbance due to pilot reuse (so-called pilot contamination), we are concerned with the computational complexity. The conventional minimum mean square error (MMSE) and minimum variance unbiased (MVU) channel estimators rely on inverting covariance matrices, which has cubic complexity in the multiplication of number of antennas at each side. Since this is extremely expensive when there are hundreds of antennas, we propose to approximate the inversion by an L-order matrix polynomial. A set of low-complexity Bayesian channel estimators, coined Polynomial ExpAnsion CHannel (PEACH) estimators, are introduced. The coefficients of the polynomials are optimized to yield small mean square error (MSE). We show numerically that near-optimal performance is achieved with low polynomial orders. In practice, the order L can be selected to balance between complexity and MSE. Interestingly, pilot contamination is beneficial to the PEACH estimators in the sense that smaller L can be used to achieve near-optimal MSEs.
Separating Hierarchical and General Hub Labelings
Venue: arXiv cs.DS 2013
Year: 2013

In the context of distance oracles, a labeling algorithm computes vertex labels during preprocessing. An $s,t$ query computes the corresponding distance from the labels of $s$ and $t$ only, without looking at the input graph. Hub labels is a class of labels that has been extensively studied. Performance of the hub label query depends on the label size. Hierarchical labels are a natural special kind of hub labels. These labels are related to other problems and can be computed more efficiently. This brings up a natural question of the quality of hierarchical labels. We show that there is a gap: optimal hierarchical labels can be polynomially bigger than the general hub labels. To prove this result, we give tight upper and lower bounds on the size of hierarchical and general labels for hypercubes.
Near-Optimal Stochastic Threshold Group Testing
Venue: arXiv cs.IT 2013
Year: 2013

We formulate and analyze a stochastic threshold group testing problem motivated by biological applications. Here a set of $n$ items contains a subset of $d \ll n$ defective items. Subsets (pools) of the $n$ items are tested -- the test outcomes are negative, positive, or stochastic (negative or positive with certain probabilities that might depend on the number of defectives being tested in the pool), depending on whether the number of defective items in the pool being tested are fewer than the {\it lower threshold} $l$, greater than the {\it upper threshold} $u$, or in between. The goal of a {\it stochastic threshold group testing} scheme is to identify the set of $d$ defective items via a "small" number of such tests. In the regime that $l = o(d)$ we present schemes that are computationally feasible to design and implement, and require near-optimal number of tests (significantly improving on existing schemes). Our schemes are robust to a variety of models for probabilistic threshold group testing.
Implementing hash-consed structures in Coq
Venue: arXiv cs.PL 2013
Year: 2013

We report on three different approaches to use hash-consing in programs certified with the Coq system, using binary decision diagrams (BDD) as running example. The use cases include execution inside Coq, or execution of the extracted OCaml code. There are different trade-offs between faithful use of pristine extracted code, and code that is fine-tuned to make use of OCaml programming constructs not available in Coq. We discuss the possible consequences in terms of performances and guarantees.
Invasive Computing - Common Terms and Granularity of Invasion
Venue: arXiv cs.OS 2013
Year: 2013

Future MPSoCs with 1000 or more processor cores on a chip require new means for resource-aware programming in order to deal with increasing imperfections such as process variation, fault rates, aging effects, and power as well as thermal problems. On the other hand, predictable program executions are threatened if not impossible if no proper means of resource isolation and exclusive use may be established on demand. In view of these problems and menaces, invasive computing enables an application programmer to claim for processing resources and spread computations to claimed processors dynamically at certain points of the program execution. Such decisions may be depending on the degree of application parallelism and the state of the underlying resources such as utilization, load, and temperature, but also with the goal to provide predictable program execution on MPSoCs by claiming processing resources exclusively as the default and thus eliminating interferences and creating the necessary isolation between multiple concurrently running applications. For achieving this goal, invasive computing introduces new programming constructs for resource-aware programming that meanwhile, for testing purpose, have been embedded into the parallel computing language X10 as developed by IBM using a library-based approach. This paper presents major ideas and common terms of invasive computing as investigated by the DFG Transregional Collaborative Research Centre TR89. Moreoever, a reflection is given on the granularity of resources that may be requested by invasive programs.
Automating the Dispute Resolution in Task Dependency Network
Venue: arXiv cs.AI 2013
Year: 2013

When perturbation or unexpected events do occur, agents need protocols for repairing or reforming the supply chain. Unfortunate contingency could increase too much the cost of performance, while breaching the current contract may be more efficient. In our framework the principles of contract law are applied to set penalties: expectation damages, opportunity cost, reliance damages, and party design remedies, and they are introduced in the task dependency model
Iterative Detection and Decoding for MIMO Systems with Knowledge-Aided Message Passing Algorithms
Venue: arXiv cs.IT 2013
Year: 2013

In this paper, we consider the problem of iterative detection and decoding (IDD) for multi-antenna systems using low-density parity-check (LDPC) codes. The proposed IDD system consists of a soft-input soft-output parallel interference (PIC) cancellation scheme with linear minimum mean-square error (MMSE) receive filters and two novel belief propagation (BP) decoding algorithms. The proposed BP algorithms exploit the knowledge of short cycles in the graph structure and the reweighting factors derived from the hypergraph's expansion. Simulation results show that when used to perform IDD for multi-antenna systems both proposed BP decoding algorithms can consistently outperform existing BP techniques with a small number of decoding iterations.
Adaptive Iterative Decision Feedback Detection Algorithms for Multi-User MIMO Systems
Venue: arXiv cs.IT 2013
Year: 2013

An adaptive iterative decision multi-feedback detection algorithm with constellation constraints is proposed for multiuser multi-antenna systems. An enhanced detection and interference cancellation is performed by introducing multiple constellation points as decision candidates. A complexity reduction strategy is developed to avoid redundant processing with reliable decisions along with an adaptive recursive least squares algorithm for time-varying channels. An iterative detection and decoding scheme is also considered with the proposed detection algorithm. Simulations show that the proposed technique has a complexity as low as the conventional decision feedback detector while it obtains a performance close to the maximum likelihood detector.
On the parameterized complexity of cutting a few vertices from a graph
Venue: arXiv cs.DS 2013
Year: 2013

We study the parameterized complexity of separating a small set of vertices from a graph by a small vertex-separator. That is, given a graph $G$ and integers $k$, $t$, the task is to find a vertex set $X$ with $|X| \le k$ and $|N(X)| \le t$. We show that - the problem is fixed-parameter tractable (FPT) when parameterized by $t$ but W[1]-hard when parameterized by $k$, and - a terminal variant of the problem, where $X$ must contain a given vertex $s$, is W[1]-hard when parameterized either by $k$ or by $t$ alone, but is FPT when parameterized by $k + t$. We also show that if we consider edge cuts instead of vertex cuts, the terminal variant is NP-hard.
Maximizing Barrier Coverage Lifetime with Mobile Sensors
Venue: arXiv cs.DS 2013
Year: 2013

Sensor networks are ubiquitously used for detection and tracking and as a result covering is one of the main tasks of such networks. We study the problem of maximizing the coverage lifetime of a barrier by mobile sensors with limited battery powers, where the coverage lifetime is the time until there is a breakdown in coverage due to the death of a sensor. Sensors are first deployed and then coverage commences. Energy is consumed in proportion to the distance traveled for mobility, while for coverage, energy is consumed in direct proportion to the radius of the sensor raised to a constant exponent. We study two variants which are distinguished by whether the sensing radii are given as part of the input or can be optimized, the fixed radii problem and the variable radii problem. We design parametric search algorithms for both problems for the case where the final order of the sensors is predetermined and for the case where sensors are initially located at barrier endpoints. In contrast, we show that the variable radii problem is strongly NP-hard and provide hardness of approximation results for fixed radii for the case where all the sensors are initially co-located at an internal point of the barrier.
Efficient Algorithms for Approximate Triangle Counting
Venue: arXiv cs.DS 2013
Year: 2013

Counting the number of triangles in a graph has many important applications in network analysis. Several frequently computed metrics like the clustering coefficient and the transitivity ratio need to count the number of triangles in the network. Furthermore, triangles are one of the most important graph classes considered in network mining. In this paper, we present a new randomized algorithm for approximate triangle counting. The algorithm can be adopted with different sampling methods and give effective triangle counting methods. In particular, we present two sampling methods, called the \textit{$q$-optimal sampling} and the \textit{edge sampling}, which respectively give $O(sm)$ and $O(sn)$ time algorithms with nice error bounds ($m$ and $n$ are respectively the number of edges and vertices in the graph and $s$ is the number of samples). Among others, we show, for example, that if an upper bound $\widetilde{Δ^e}$ is known for the number of triangles incident to every edge, the proposed method provides an $1\pm ε$ approximation which runs in $O( \frac{\widetilde{Δ^e} n \log n}{\widehat{Δ^e} ε^2} )$ time, where $\widehat{Δ^e}$ is the average number of triangles incident to an edge. Finally we show that the algorithm can be adopted with streams. Then it, for example, will perform 2 passes over the data (if the size of the graph is known, otherwise it needs 3 passes) and will use $O(sn)$ space.
Verification of Inconsistency-Aware Knowledge and Action Bases (Extended Version)
Venue: arXiv cs.AI 2013
Year: 2013

Description Logic Knowledge and Action Bases (KABs) have been recently introduced as a mechanism that provides a semantically rich representation of the information on the domain of interest in terms of a DL KB and a set of actions to change such information over time, possibly introducing new objects. In this setting, decidability of verification of sophisticated temporal properties over KABs, expressed in a variant of first-order mu-calculus, has been shown. However, the established framework treats inconsistency in a simplistic way, by rejecting inconsistent states produced through action execution. We address this problem by showing how inconsistency handling based on the notion of repairs can be integrated into KABs, resorting to inconsistency-tolerant semantics. In this setting, we establish decidability and complexity of verification.
A Theoretical Analysis of NDCG Type Ranking Measures
Venue: arXiv cs.LG 2013
Year: 2013

A central problem in ranking is to design a ranking measure for evaluation of ranking functions. In this paper we study, from a theoretical perspective, the widely used Normalized Discounted Cumulative Gain (NDCG)-type ranking measures. Although there are extensive empirical studies of NDCG, little is known about its theoretical properties. We first show that, whatever the ranking function is, the standard NDCG which adopts a logarithmic discount, converges to 1 as the number of items to rank goes to infinity. On the first sight, this result is very surprising. It seems to imply that NDCG cannot differentiate good and bad ranking functions, contradicting to the empirical success of NDCG in many applications. In order to have a deeper understanding of ranking measures in general, we propose a notion referred to as consistent distinguishability. This notion captures the intuition that a ranking measure should have such a property: For every pair of substantially different ranking functions, the ranking measure can decide which one is better in a consistent manner on almost all datasets. We show that NDCG with logarithmic discount has consistent distinguishability although it converges to the same limit for all ranking functions. We next characterize the set of all feasible discount functions for NDCG according to the concept of consistent distinguishability. Specifically we show that whether NDCG has consistent distinguishability depends on how fast the discount decays, and 1/r is a critical point. We then turn to the cut-off version of NDCG, i.e., NDCG@k. We analyze the distinguishability of NDCG@k for various choices of k and the discount functions. Experimental results on real Web search datasets agree well with the theory.
Virtual Machine Trading in a Federation of Clouds: Individual Profit and Social Welfare Maximization
Venue: arXiv cs.NI 2013
Year: 2013

By sharing resources among different cloud providers, the paradigm of federated clouds exploits temporal availability of resources and geographical diversity of operational costs for efficient job service. While interoperability issues across different cloud platforms in a cloud federation have been extensively studied, fundamental questions on cloud economics remain: When and how should a cloud trade resources (e.g., virtual machines) with others, such that its net profit is maximized over the long run, while a close-to-optimal social welfare in the entire federation can also be guaranteed? To answer this question, a number of important, inter-related decisions, including job scheduling, server provisioning and resource pricing, should be dynamically and jointly made, while the long-term profit optimality is pursued. In this work, we design efficient algorithms for inter-cloud virtual machine (VM) trading and scheduling in a cloud federation. For VM transactions among clouds, we design a double-auction based mechanism that is strategyproof, individual rational, ex-post budget balanced, and efficient to execute over time. Closely combined with the auction mechanism is a dynamic VM trading and scheduling algorithm, which carefully decides the true valuations of VMs in the auction, optimally schedules stochastic job arrivals with different SLAs onto the VMs, and judiciously turns on and off servers based on the current electricity prices. Through rigorous analysis, we show that each individual cloud, by carrying out the dynamic algorithm in the online double auction, can achieve a time-averaged profit arbitrarily close to the offline optimum. Asymptotic optimality in social welfare is also achieved under homogeneous cloud settings. We carry out trace-driven simulations to examine the effectiveness of our algorithms and the achievable social welfare under heterogeneous cloud settings.
Partitions of Frobenius Rings Induced by the Homogeneous Weight
Venue: arXiv cs.IT 2013
Year: 2013

The values of the homogeneous weight are determined for finite Frobenius rings that are a direct product of local Frobenius rings. This is used to investigate the partition induced by this weight and its dual partition under character-theoretic dualization. A characterization is given of those rings for which the induced partition is reflexive or even self-dual.
Lp-Regularized Least Squares (0<p<1) and Critical Path
Venue: arXiv cs.IT 2013
Year: 2013

The least squares problem is formulated in terms of Lp quasi-norm regularization (0<p<1). Two formulations are considered: (i) an Lp-constrained optimization and (ii) an Lp-penalized (unconstrained) optimization. Due to the nonconvexity of the Lp quasi-norm, the solution paths of the regularized least squares problem are not ensured to be continuous. A critical path, which is a maximal continuous curve consisting of critical points, is therefore considered separately. The critical paths are piecewise smooth, as can be seen from the viewpoint of the variational method, and generally contain non-optimal points such as saddle points and local maxima as well as global/local minima. Along each critical path, the correspondence between the regularization parameters (which govern the 'strength' of regularization in the two formulations) is non-monotonic and, more specifically, it has multiplicity. Two paths of critical points connecting the origin and an ordinary least squares (OLS) solution are highlighted. One is a main path starting at an OLS solution, and the other is a greedy path starting at the origin. Part of the greedy path can be constructed with a generalized Minkowskian gradient. The breakpoints of the greedy path coincide with the step-by-step solutions generated by using orthogonal matching pursuit (OMP), thereby establishing a direct link between OMP and Lp-regularized least squares.
PIDE as front-end technology for Coq
Venue: arXiv cs.HC 2013
Year: 2013

Isabelle/PIDE is the current Prover IDE technology for Isabelle. It has been developed in ML and Scala in the past 4-5 years for this particular proof assistant, but with an open mind towards other systems. PIDE is based on an asynchronous document model, where the prover receives edits continuously and updates its internal state accordingly. The interpretation of edits and the policies for proof document processing are determined by the prover. The editor front-end merely takes care of visual rendering of formal document content. Here we report on an experiment to connect Coq to the PIDE infrastructure of Isabelle. This requires to re-implement the core PIDE protocol layer of Isabelle/ML in OCaml. The payload for semantic processing of proof document content is restricted to lexical analysis in the sense of existing CoqIde functionality. This is sufficient as proof-of-concept for PIDE connectivity. Actual proof processing is then a matter of improving Coq towards timeless and stateless proof processing, independently of PIDE technicalities. The implementation worked out smoothly and required minimal changes to the refined PIDE architecture of Isabelle2013. This experiment substantiates PIDE as general approach to prover interaction. It illustrates how other provers of the greater ITP family can participate by following similar reforms of the classic TTY loop as was done for Isabelle in the past few years.
Algebraic Algorithms for b-Matching, Shortest Undirected Paths, and f-Factors
Venue: arXiv cs.DS 2013
Year: 2013

Let G=(V,E) be a graph with f:V\to Z_+ a function assigning degree bounds to vertices. We present the first efficient algebraic algorithm to find an f-factor. The time is \tilde{O}(f(V)^ω). More generally for graphs with integral edge weights of maximum absolute value W we find a maximum weight f-factor in time \tilde{O}(Wf(V)^ω). (The algorithms are randomized, correct with high probability and Las Vegas; the time bound is worst-case.) We also present three specializations of these algorithms: For maximum weight perfect f-matching the algorithm is considerably simpler (and almost identical to its special case of ordinary weighted matching). For the single-source shortest-path problem in undirected graphs with conservative edge weights, we present a generalization of the shortest-path tree, and we compute it in \tilde{O(Wn^ω) time. For bipartite graphs, we improve the known complexity bounds for vertex capacitated max-flow and min-cost max-flow on a subclass of graphs.