OpenRaiser/Intern-Atlas huggingface dataset:
Zielonka's Recursive Algorithm: dull, weak and solitaire games and tighter bounds
Venue: arXiv cs.LO 2013
Year: 2013

Dull, weak and nested solitaire games are important classes of parity games, capturing, among others, alternation-free mu-calculus and ECTL* model checking problems. These classes can be solved in polynomial time using dedicated algorithms. We investigate the complexity of Zielonka's Recursive algorithm for solving these special games, showing that the algorithm runs in O(d (n + m)) on weak games, and, somewhat surprisingly, that it requires exponential time to solve dull games and (nested) solitaire games. For the latter classes, we provide a family of games G, allowing us to establish a lower bound of 2^(n/3). We show that an optimisation of Zielonka's algorithm permits solving games from all three classes in polynomial time. Moreover, we show that there is a family of (non-special) games M that permits us to establish a lower bound of 2^(n/3), improving on the previous lower bound for the algorithm.
Deciding the Satisfiability of MITL Specifications
Venue: arXiv cs.LO 2013
Year: 2013

In this paper we present a satisfiability-preserving reduction from MITL interpreted over finitely-variable continuous behaviors to Constraint LTL over clocks, a variant of CLTL that is decidable, and for which an SMT-based bounded satisfiability checker is available. The result is a new complete and effective decision procedure for MITL. Although decision procedures for MITL already exist, the automata-based techniques they employ appear to be very difficult to realize in practice, and, to the best of our knowledge, no implementation currently exists for them. A prototype tool for MITL based on the encoding presented here has, instead, been implemented and is publicly available.
Improving HyLTL model checking of hybrid systems
Venue: arXiv cs.LO 2013
Year: 2013

The problem of model-checking hybrid systems is a long-time challenge in the scientific community. Most of the existing approaches and tools are either limited on the properties that they can verify, or restricted to simplified classes of systems. To overcome those limitations, a temporal logic called HyLTL has been recently proposed. The model checking problem for this logic has been solved by translating the formula into an equivalent hybrid automaton, that can be analized using existing tools. The original construction employs a declarative procedure that generates exponentially many states upfront, and can be very inefficient when complex formulas are involved. In this paper we solve a technical issue in the construction that was not considered in previous works, and propose a new algorithm to translate HyLTL into hybrid automata, that exploits optimized techniques coming from the discrete LTL community to build smaller automata.
Approximating the minimum cycle mean
Venue: arXiv cs.DS 2013
Year: 2013

We consider directed graphs where each edge is labeled with an integer weight and study the fundamental algorithmic question of computing the value of a cycle with minimum mean weight. Our contributions are twofold: (1) First we show that the algorithmic question is reducible in O(n^2) time to the problem of a logarithmic number of min-plus matrix multiplications of n-by-n matrices, where n is the number of vertices of the graph. (2) Second, when the weights are nonnegative, we present the first (1 + ε)-approximation algorithm for the problem and the running time of our algorithm is \tilde(O)(n^ωlog^3(nW/ε) / ε), where O(n^ω) is the time required for the classic n-by-n matrix multiplication and W is the maximum value of the weights.
Modularity and Openness in Modeling Multi-Agent Systems
Venue: arXiv cs.MA 2013
Year: 2013

We revisit the formalism of modular interpreted systems (MIS) which encourages modular and open modeling of synchronous multi-agent systems. The original formulation of MIS did not live entirely up to its promise. In this paper, we propose how to improve modularity and openness of MIS by changing the structure of interference functions. These relatively small changes allow for surprisingly high flexibility when modeling actual multi-agent systems. We demonstrate this on two well-known examples, namely the trains, tunnel and controller, and the dining cryptographers. Perhaps more importantly, we propose how the notions of multi-agency and openness, crucial for multi-agent systems, can be precisely defined based on their MIS representations.
Ranking with Diverse Intents and Correlated Contents
Venue: arXiv cs.DS 2013
Year: 2013

We consider the following document ranking problem: We have a collection of documents, each containing some topics (e.g. sports, politics, economics). We also have a set of users with diverse interests. Assume that user u is interested in a subset I_u of topics. Each user u is also associated with a positive integer K_u, which indicates that u can be satisfied by any K_u topics in I_u. Each document s contains information for a subset C_s of topics. The objective is to pick one document at a time such that the average satisfying time is minimized, where a user's satisfying time is the first time that at least K_u topics in I_u are covered in the documents selected so far. Our main result is an O(ρ)-approximation algorithm for the problem, where ρ is the algorithmic integrality gap of the linear programming relaxation of the set cover instance defined by the documents and topics. This result generalizes the constant approximations for generalized min-sum set cover and ranking with unrelated intents and the logarithmic approximation for the problem of ranking with submodular valuations (when the submodular function is the coverage function), and can be seen as an interpolation between these results. We further extend our model to the case when each user may interest in more than one sets of topics and when the user's valuation function is XOS, and obtain similar results for these models.
Bottleneck combinatorial optimization problems with uncertain costs and the OWA criterion
Venue: arXiv cs.DS 2013
Year: 2013

In this paper a class of bottleneck combinatorial optimization problems with uncertain costs is discussed. The uncertainty is modeled by specifying a discrete scenario set containing a finite number of cost vectors, called scenarios. In order to choose a solution the Ordered Weighted Averaging aggregation operator (shortly OWA) is applied. The OWA operator generalizes traditional criteria in decision making under uncertainty such as the maximum, minimum, average, median, or Hurwicz criterion. New complexity and approximation results in this area are provided. These results are general and remain valid for many problems, in particular for a wide class of network problems.
Xing-Ling Codes, Duals of their Subcodes, and Good Asymmetric Quantum Codes
Venue: arXiv cs.IT 2013
Year: 2013

A class of powerful $q$-ary linear polynomial codes originally proposed by Xing and Ling is deployed to construct good asymmetric quantum codes via the standard CSS construction. Our quantum codes are $q$-ary block codes that encode $k$ qudits of quantum information into $n$ qudits and correct up to $\flr{(d_{x}-1)/2}$ bit-flip errors and up to $\flr{(d_{z}-1)/2}$ phase-flip errors.. In many cases where the length $(q^{2}-q)/2 \leq n \leq (q^{2}+q)/2$ and the field size $q$ are fixed and for chosen values of $d_{x} \in \{2,3,4,5\}$ and $d_{z} \ge δ$, where $δ$ is the designed distance of the Xing-Ling (XL) codes, the derived pure $q$-ary asymmetric quantum CSS codes possess the best possible size given the current state of the art knowledge on the best classical linear block codes.
Pushdown Systems for Monotone Frameworks
Venue: arXiv cs.PL 2013
Year: 2013

Monotone frameworks is one of the most successful frameworks for intraprocedural data flow analysis extending the traditional class of bitvector frameworks (like live variables and available expressions). Weighted pushdown systems is similarly one of the most general frameworks for interprocedural analysis of programs. However, it makes use of idempotent semirings to represent the sets of properties and unfortunately they do not admit analyses whose transfer functions are not strict (e.g., classical bitvector frameworks). This motivates the development of algorithms for backward and forward reachability of pushdown systems using sets of properties forming so-called flow algebras that weaken some of the assumptions of idempotent semirings. In particular they do admit the bitvector frameworks, monotone frameworks, as well as idempotent semirings. We show that the algorithms are sound under mild assumptions on the flow algebras, mainly that the set of properties constitutes a join semi-lattice, and complete provided that the transfer functions are suitably distributive (but not necessarily strict).
A Prolog Specification of Giant Number Arithmetic
Venue: arXiv cs.PL 2013
Year: 2013

The tree based representation described in this paper, hereditarily binary numbers, applies recursively a run-length compression mechanism that enables computations limited by the structural complexity of their operands rather than by their bitsizes. While within constant factors from their traditional counterparts for their worst case behavior, our arithmetic operations open the doors for interesting numerical computations, impossible with traditional number representations. We provide a complete specification of our algorithms in the form of a purely declarative Prolog program.
Relation lifting, with an application to the many-valued cover modality
Venue: arXiv cs.LO 2013
Year: 2013

We introduce basic notions and results about relation liftings on categories enriched in a commutative quantale. We derive two necessary and sufficient conditions for a 2-functor T to admit a functorial relation lifting: one is the existence of a distributive law of T over the "powerset monad" on categories, one is the preservation by T of "exactness" of certain squares. Both characterisations are generalisations of the "classical" results known for set functors: the first characterisation generalises the existence of a distributive law over the genuine powerset monad, the second generalises preservation of weak pullbacks. The results presented in this paper enable us to compute predicate liftings of endofunctors of, for example, generalised (ultra)metric spaces. We illustrate this by studying the coalgebraic cover modality in this setting.
Lorentzian Iterative Hard Thresholding: Robust Compressed Sensing with Prior Information
Venue: arXiv cs.IT 2013
Year: 2013

Commonly employed reconstruction algorithms in compressed sensing (CS) use the $L_2$ norm as the metric for the residual error. However, it is well-known that least squares (LS) based estimators are highly sensitive to outliers present in the measurement vector leading to a poor performance when the noise no longer follows the Gaussian assumption but, instead, is better characterized by heavier-than-Gaussian tailed distributions. In this paper, we propose a robust iterative hard Thresholding (IHT) algorithm for reconstructing sparse signals in the presence of impulsive noise. To address this problem, we use a Lorentzian cost function instead of the $L_2$ cost function employed by the traditional IHT algorithm. We also modify the algorithm to incorporate prior signal information in the recovery process. Specifically, we study the case of CS with partially known support. The proposed algorithm is a fast method with computational load comparable to the LS based IHT, whilst having the advantage of robustness against heavy-tailed impulsive noise. Sufficient conditions for stability are studied and a reconstruction error bound is derived. We also derive sufficient conditions for stable sparse signal recovery with partially known support. Theoretical analysis shows that including prior support information relaxes the conditions for successful reconstruction. Simulation results demonstrate that the Lorentzian-based IHT algorithm significantly outperform commonly employed sparse reconstruction techniques in impulsive environments, while providing comparable performance in less demanding, light-tailed environments. Numerical results also demonstrate that the partially known support inclusion improves the performance of the proposed algorithm, thereby requiring fewer samples to yield an approximate reconstruction.
Cloud Template, a Big Data Solution
Venue: arXiv cs.DC 2013
Year: 2013

Today cloud computing has become as a new concept for hosting and delivering different services over the Internet for big data solutions. Cloud computing is attractive to different business owners of both small and enterprise as it eliminates the requirement for users to plan ahead for provisioning, and allows enterprises to start from the small and increase resources only when there is a rise in service demand. Despite the fact that cloud computing offers huge opportunities to the IT industry, the development of cloud computing technology is currently has several issues. This study presents an idea for introducing cloud templates which will be used for analyzing, designing, developing and implementing cloud computing systems. We will present a template based design for cloud computing systems, highlighting its key concepts, architectural principles and state of the art implementation, as well as research challenges and future work requirements. The aim of this idea is to provide a better understanding of the design challenges of cloud computing and identify important research directions in this big data increasingly important area. We will describe a series of studies by which we and other researchers have assessed the effectiveness of these techniques in practical situations. Finally, in this study we will show how this idea could be implemented in a practical and useful way in industry.
Content Based Image Retrieval System using Feature Classification with Modified KNN Algorithm
Venue: arXiv cs.CV 2013
Year: 2013

Feature means countenance, remote sensing scene objects with similar characteristics, associated to interesting scene elements in the image formation process. They are classified into three types in image processing, that is low, middle and high. Low level features are color, texture and middle level feature is shape and high level feature is semantic gap of objects. An image retrieval system is a computer system for browsing, searching and retrieving images from a large image database. Content Based Image Retrieval is a technique which uses visual features of image such as color, shape, texture to search user required image from large image database according to user requests in the form of a query. MKNN is an enhancing method of KNN. The proposed KNN classification is called MKNN. MKNN contains two parts for processing, they are validity of the train samples and applying weighted KNN. The validity of each point is computed according to its neighbors. In our proposal, Modified K-Nearest Neighbor can be considered a kind of weighted KNN so that the query label is approximated by weighting the neighbors of the query.
Performance Limits of a Cloud Radio
Venue: arXiv cs.IT 2013
Year: 2013

Cooperation in a cellular network is seen as a key technique in managing other cell interference to observe a gain in achievable rate. In this paper, we present the achievable rate regions for a cloud radio network using a sub-optimal zero forcing equalizer with dirty paper precoding. We show that when complete channel state information is available at the cloud, rates close to those achievable with total interference cancellation can be achieved. With mean capacity gains, of up to 2 fold over the conventional cellular network in both uplink and downlink, this precoding scheme shows great promise for implementation in a cloud radio network. To simplify the analysis, we use a stochastic geometric framework based of Poisson point processes instead of the traditional grid based cellular network model. We also study the impact of limiting the channel state information and geographical clustering to limit the cloud size on the achievable rate. We have observed that using this zero forcing-dirty paper coding technique, the adverse effect of inter-cluster interference can be minimized thereby transforming an interference limited network into a noise limited network as experienced by an average user in the network for low operating signal-to-noise-ratios. However, for higher signal-to-noise-ratios, both the average achievable rate and cell-edge achievable rate saturate as observed in literature. As the implementation of dirty paper coding is practically not feasible, we present a practical design of a cloud radio network using cloud a minimum mean square equalizer for processing the uplink streams and use Tomlinson-Harashima precoder as a sub-optimal substitute for a dirty paper precoder in downlink.
Time-Frequency Foundations of Communications
Venue: arXiv cs.IT 2013
Year: 2013

In the tradition of Gabor's 1946 landmark paper [1], we advocate a time-frequency (TF) approach to communications. TF methods for communications have been proposed very early (see the box History). While several tutorial papers and book chapters on the topic are available (see, e.g., [2]-[4] and references therein), the goal of this paper is to present the fundamental aspects in a coherent and easily accessible manner. Specifically, we establish the role of TF methods in communications across a range of subject areas including TF dispersive channels, orthogonal frequency division multiplexing (OFDM), information-theoretic limits, and system identification and channel estimation. Furthermore, we present fundamental results that are stated in the literature for the continuous-time case in simple linear algebra terms.
Estimating 3D Signals with Kalman Filter
Venue: arXiv cs.IT 2013
Year: 2013

In this paper, the standard Kalman filter was implemented to denoise the three dimensional signals affected by additive white Gaussian noise (AWGN), we used fast algorithm based on Laplacian operator to measure the noise variance and a fast median filter to predict the state variable. The Kalman algorithm is modeled by adjusting its parameters for better performance in both filtering and in reducing the computational load while conserving the information contained in the signal
Linear Precoder Design for MIMO Interference Channels with Finite-Alphabet Signaling
Venue: arXiv cs.IT 2013
Year: 2013

This paper investigates the linear precoder design for $K$-user interference channels of multiple-input multiple-output (MIMO) transceivers under finite alphabet inputs. We first obtain general explicit expressions of the achievable rate for users in the MIMO interference channel systems. We study optimal transmission strategies in both low and high signal-to-noise ratio (SNR) regions. Given finite alphabet inputs, we show that a simple power allocation design achieves optimal performance at high SNR whereas the well-known interference alignment technique for Gaussian inputs only utilizes a partial interference-free signal space for transmission and leads to a constant rate loss when applied naively to finite-alphabet inputs. Moreover, we establish necessary conditions for the linear precoder design to achieve weighted sum-rate maximization. We also present an efficient iterative algorithm for determining precoding matrices of all the users. Our numerical results demonstrate that the proposed iterative algorithm achieves considerably higher sum-rate under practical QAM inputs than other known methods.
Approximate Nash Equilibria via Sampling
Venue: arXiv cs.GT 2013
Year: 2013

We prove that in a normal form n-player game with m actions for each player, there exists an approximate Nash equilibrium where each player randomizes uniformly among a set of O(log(m) + log(n)) pure strategies. This result induces an $N^{\log \log N}$ algorithm for computing an approximate Nash equilibrium in games where the number of actions is polynomial in the number of players (m=poly(n)), where $N=nm^n$ is the size of the game (the input size). In addition, we establish an inverse connection between the entropy of Nash equilibria in the game, and the time it takes to find such an approximate Nash equilibrium using the random sampling algorithm.
The Pin-Bang Theory: Discovering The Pinterest World
Venue: arXiv cs.SI 2013
Year: 2013

Pinterest is an image-based online social network, which was launched in the year 2010 and has gained a lot of traction, ever since. Within 3 years, Pinterest has attained 48.7 million unique users. This stupendous growth makes it interesting to study Pinterest, and gives rise to multiple questions about it's users, and content. We characterized Pinterest on the basis of large scale crawls of 3.3 million user profiles, and 58.8 million pins. In particular, we explored various attributes of users, pins, boards, pin sources, and user locations, in detail and performed topical analysis of user generated textual content. The characterization revealed most prominent topics among users and pins, top image sources, and geographical distribution of users on Pinterest. We then investigated this social network from a privacy and security standpoint, and found traces of malware in the form of pin sources. Instances of Personally Identifiable Information (PII) leakage were also discovered in the form of phone numbers, BBM (Blackberry Messenger) pins, and email addresses. Further, our analysis demonstrated how Pinterest is a potential venue for copyright infringement, by showing that almost half of the images shared on Pinterest go uncredited. To the best of our knowledge, this is the first attempt to characterize Pinterest at such a large scale.
Performance Analysis of Optimum Zero-Forcing Beamforming with Greedy User Selection
Venue: arXiv cs.IT 2013
Year: 2013

In this letter, an exact performance analysis is presented on the sum rate of zero-forcing beamforming with a greedy user scheduling algorithm in a downlink system. Adopting water-filling power allocation, we derive a compact form for the joint probability density function of the scheduled users' squared subchannel gains when a transmitter with multiple antennas sends information to at most two scheduled users with each having a single antenna. The analysis is verified by numerical results.
Navigation Assistance and Web Accessibility Helper
Venue: arXiv cs.HC 2013
Year: 2013

Web accessibility is actually the most important aspect for providing access to information and interaction for people with disabilities. However, it seems that the ability of users with disabilities to navigate over the Web is not dependent on the graphical complexity, but on the markup used to create the structure of the website. Consequently, it is necessary to design some software assistants to help all users to mark themselves in space during a navigation session. In this paper, we propose an assistant for browsing on the Internet to allow user to get one s bearings within Web navigation. We describe our approach which puts at the disposal of the user a visited site map, thus giving an explicit representation of virtual space. Different levels of visualization are implemented in order to make the map more visible and less overloaded.