OpenRaiser/Intern-Atlas huggingface dataset:
A Comparison of Sequential and GPU Implementations of Iterative Methods to Compute Reachability Probabilities
Venue: arXiv cs.DC 2012
Year: 2012

We consider the problem of computing reachability probabilities: given a Markov chain, an initial state of the Markov chain, and a set of goal states of the Markov chain, what is the probability of reaching any of the goal states from the initial state? This problem can be reduced to solving a linear equation Ax = b for x, where A is a matrix and b is a vector. We consider two iterative methods to solve the linear equation: the Jacobi method and the biconjugate gradient stabilized (BiCGStab) method. For both methods, a sequential and a parallel version have been implemented. The parallel versions have been implemented on the compute unified device architecture (CUDA) so that they can be run on a NVIDIA graphics processing unit (GPU). From our experiments we conclude that as the size of the matrix increases, the CUDA implementations outperform the sequential implementations. Furthermore, the BiCGStab method performs better than the Jacobi method for dense matrices, whereas the Jacobi method does better for sparse ones. Since the reachability probabilities problem plays a key role in probabilistic model checking, we also compared the implementations for matrices obtained from a probabilistic model checker. Our experiments support the conjecture by Bosnacki et al. that the Jacobi method is superior to Krylov subspace methods, a class to which the BiCGStab method belongs, for probabilistic model checking.
Lex-Partitioning: A New Option for BDD Search
Venue: arXiv cs.AI 2012
Year: 2012

For the exploration of large state spaces, symbolic search using binary decision diagrams (BDDs) can save huge amounts of memory and computation time. State sets are represented and modified by accessing and manipulating their characteristic functions. BDD partitioning is used to compute the image as the disjunction of smaller subimages. In this paper, we propose a novel BDD partitioning option. The partitioning is lexicographical in the binary representation of the states contained in the set that is represented by a BDD and uniform with respect to the number of states represented. The motivation of controlling the state set sizes in the partitioning is to eventually bridge the gap between explicit and symbolic search. Let n be the size of the binary state vector. We propose an O(n) ranking and unranking scheme that supports negated edges and operates on top of precomputed satcount values. For the uniform split of a BDD, we then use unranking to provide paths along which we partition the BDDs. In a shared BDD representation the efforts are O(n). The algorithms are fully integrated in the CUDD library and evaluated in strongly solving general game playing benchmarks.
Topic-Level Opinion Influence Model(TOIM): An Investigation Using Tencent Micro-Blogging
Venue: arXiv cs.SI 2012
Year: 2012

Mining user opinion from Micro-Blogging has been extensively studied on the most popular social networking sites such as Twitter and Facebook in the U.S., but few studies have been done on Micro-Blogging websites in other countries (e.g. China). In this paper, we analyze the social opinion influence on Tencent, one of the largest Micro-Blogging websites in China, endeavoring to unveil the behavior patterns of Chinese Micro-Blogging users. This paper proposes a Topic-Level Opinion Influence Model (TOIM) that simultaneously incorporates topic factor and social direct influence in a unified probabilistic framework. Based on TOIM, two topic level opinion influence propagation and aggregation algorithms are developed to consider the indirect influence: CP (Conservative Propagation) and NCP (None Conservative Propagation). Users' historical social interaction records are leveraged by TOIM to construct their progressive opinions and neighbors' opinion influence through a statistical learning process, which can be further utilized to predict users' future opinions on some specific topics. To evaluate and test this proposed model, an experiment was designed and a sub-dataset from Tencent Micro-Blogging was used. The experimental results show that TOIM outperforms baseline methods on predicting users' opinion. The applications of CP and NCP have no significant differences and could significantly improve recall and F1-measure of TOIM.
Equitable Colorings of Corona Multiproducts of Graphs
Venue: arXiv cs.DM 2012
Year: 2012

A graph is equitably $k$-colorable if its vertices can be partitioned into $k$ independent sets in such a way that the number of vertices in any two sets differ by at most one. The smallest $k$ for which such a coloring exists is known as the equitable chromatic number of $G$ and denoted $χ_{=}(G)$. It is known that this problem is NP-hard in general case and remains so for corona graphs. In "Equitable colorings of Cartesian products of graphs" (2012) Lin and Chang studied equitable coloring of Cartesian products of graphs. In this paper we consider the same model of coloring in the case of corona products of graphs. In particular, we obtain some results regarding the equitable chromatic number for $l$-corona product $G \circ ^l H$, where $G$ is an equitably 3- or 4-colorable graph and $H$ is an $r$-partite graph, a path, a cycle or a complete graph. Our proofs are constructive in that they lead to polynomial algorithms for equitable coloring of such graph products provided that there is given an equitable coloring of $G$. Moreover, we confirm Equitable Coloring Conjecture for corona products of such graphs. This paper extends our results from \cite{hf}.
Reconciling complex organizations and data management: the Panopticon paradigm
Venue: arXiv cs.CY 2012
Year: 2012

These last years, main IT companies have build software solutions and change management plans promoting data quality management within organizations concerned by the enhancement of their business intelligence system. These offers are closely similar data governance schemes based on a common paradigm called Master Data Management. These schemes appear generally inappropriate to the context of complex extended organizations. On the other hand, the community-based data governance schemes have shown their own efficiency to contribute to the reliability of data in digital social networks, as well as their ability to meet user expectations. After a brief analysis of the very specific constraints weighting on extended organization s data governance, and of peculiarities of monitoring and regulatory processes associated to management control and IT within these, we propose a new scheme inspired by Foucaldian analysis on governmentality: the Panopticon data governance paradigm.
Formally Checking Large Data Sets in the Railways
Venue: arXiv cs.SE 2012
Year: 2012

This article presents industrial experience of validating large data sets against specification written using the B / Event-B mathematical language and the ProB model checker.
The Geometry of Types (Long Version)
Venue: arXiv cs.LO 2012
Year: 2012

We show that time complexity analysis of higher-order functional programs can be effectively reduced to an arguably simpler (although computationally equivalent) verification problem, namely checking first-order inequalities for validity. This is done by giving an efficient inference algorithm for linear dependent types which, given a PCF term, produces in output both a linear dependent type and a cost expression for the term, together with a set of proof obligations. Actually, the output type judgement is derivable iff all proof obligations are valid. This, coupled with the already known relative completeness of linear dependent types, ensures that no information is lost, i.e., that there are no false positives or negatives. Moreover, the procedure reflects the difficulty of the original problem: simple PCF terms give rise to sets of proof obligations which are easy to solve. The latter can then be put in a format suitable for automatic or semi-automatic verification by external solvers. Ongoing experimental evaluation has produced encouraging results, which are briefly presented in the paper.
Towards Refinement Strategy Planning for Event-B
Venue: arXiv cs.SE 2012
Year: 2012

Event-B is a formal approach oriented to system modeling and analysis. It supports refinement mechanism that enables stepwise modeling and verification of a system. By using refinement, the complexity of verification can be spread and mitigated. In common development using Event-B, a specification written in a natural language is examined before modeling in order to plan the modeling and refinement strategy. After that, starting from a simple abstract model, concrete models in several different abstraction levels are constructed by gradually introducing complex structures and concepts. Although users of Event-B have to plan how to abstract the specification for the construction of each model, guidelines for such a planning have not been suggested. Specifically, some elements in a model often require that other elements are included in the model because of semantics constraints of Event-B. As such requirements introduces many elements at once, non-experts of Event-B often make refinement rough though rough refinement does not mitigate the complexity of verification well. In response to the problem, a method is proposed to plan what models are constructed in each abstraction level. The method calculates plans that mitigate the complexity well considering the semantics constraints of Event-B and the relationships between elements in a system.
On Numbers of Pseudo-Triangulations
Venue: arXiv cs.CG 2012
Year: 2012

We study the maximum numbers of pseudo-triangulations and pointed pseudo-triangulations that can be embedded over a specific set of points in the plane or contained in a specific triangulation. We derive the bounds $O(5.45^N)$ and $Ω(2.41^N)$ for the maximum number of pointed pseudo-triangulations that can be contained in a specific triangulation over a set of $N$ points. For the number of all pseudo-triangulations contained in a triangulation we derive the bounds $O^*(6.54^N)$ and $Ω(3.30^N)$. We also prove that $O^*(89.1^N)$ pointed pseudo-triangulations can be embedded over any specific set of $N$ points in the plane, and at most $120^N$ general pseudo-triangulations.
Synthesis of sup-interpretations: a survey
Venue: arXiv cs.CC 2012
Year: 2012

In this paper, we survey the complexity of distinct methods that allow the programmer to synthesize a sup-interpretation, a function providing an upper- bound on the size of the output values computed by a program. It consists in a static space analysis tool without consideration of the time consumption. Although clearly related, sup-interpretation is independent from termination since it only provides an upper bound on the terminating computations. First, we study some undecidable properties of sup-interpretations from a theoretical point of view. Next, we fix term rewriting systems as our computational model and we show that a sup-interpretation can be obtained through the use of a well-known termination technique, the polynomial interpretations. The drawback is that such a method only applies to total functions (strongly normalizing programs). To overcome this problem we also study sup-interpretations through the notion of quasi-interpretation. Quasi-interpretations also suffer from a drawback that lies in the subterm property. This property drastically restricts the shape of the considered functions. Again we overcome this problem by introducing a new notion of interpretations mainly based on the dependency pairs method. We study the decidability and complexity of the sup-interpretation synthesis problem for all these three tools over sets of polynomials. Finally, we take benefit of some previous works on termination and runtime complexity to infer sup-interpretations.
Abstract Data Types in Event-B - An Application of Generic Instantiation
Venue: arXiv cs.SE 2012
Year: 2012

Integrating formal methods into industrial practice is a challenging task. Often, different kinds of expertise are required within the same development. On the one hand, there are domain engineers who have specific knowledge of the system under development. On the other hand, there are formal methods experts who have experience in rigorously specifying and reasoning about formal systems. Coordination between these groups is important for taking advantage of their expertise. In this paper, we describe our approach of using generic instantiation to facilitate this coordination. In particular, generic instantiation enables a separation of concerns between the different parties involved in developing formal systems.
Edge-colouring seven-regular planar graphs
Venue: arXiv cs.DM 2012
Year: 2012

A conjecture due to the fourth author states that every $d$-regular planar multigraph can be $d$-edge-coloured, provided that for every odd set $X$ of vertices, there are at least $d$ edges between $X$ and its complement. For $d = 3$ this is the four-colour theorem, and the conjecture has been proved for all $d\le 8$, by various authors. In particular, two of us proved it when $d=7$; and then three of us proved it when $d=8$. The methods used for the latter give a proof in the $d=7$ case that is simpler than the original, and we present it here.
Optimizing Infrastructures for Testing Using Virtualization
Venue: arXiv cs.DC 2012
Year: 2012

Virtualization technology and cloud computing have brought a paradigm shift in the way we utilize, deploy and manage computer resources. They allow fast deployment of multiple operating system as containers on physical ma- chines which can be either discarded after use or check- pointed for later re-deployment. At European Organization for Nuclear Research (CERN), we have been using virtualization technology to quickly setup virtual machines for our developers with preconfigured software to enable them to quickly test/deploy a new version of a software patch for a given application. This paper reports both on the techniques that have been used to setup a private cloud on a commodity hardware and also presents the optimization techniques we used to remove deployment specific performance bottlenecks.
One-Step Quantized Network Coding for Near Sparse Gaussian Messages
Venue: arXiv cs.IT 2012
Year: 2012

In this paper, mathematical bases for non-adaptive joint source network coding of correlated messages in a Bayesian scenario are studied. Specifically, we introduce one-step Quantized Network Coding (QNC), which is a hybrid combination of network coding and packet forwarding for transmission. Motivated by the work on Bayesian compressed sensing, we derive theoretical guarantees on robust recovery in a one-step QNC scenario. Our mathematical derivations for Gaussian messages express the opportunity of distributed compression by using one-step QNC, as a simplified version of QNC scenario. Our simulation results show an improvement in terms of quality-delay performance over routing based packet forwarding.
Modified Stage-Gate: A Conceptual Model of Virtual Product Development Process
Venue: arXiv cs.OH 2012
Year: 2012

In today s dynamic marketplace, manufacturing companies are under strong pressure to introduce new products for long-term survival with their competitors. Nevertheless, every company cannot cope up progressively or immediately with the market requirements due to knowledge dynamics being experienced in the competitive milieu. Increased competition and reduced product life cycles put force upon companies to develop new products faster. In response to these pressing needs, there should be some new approach compatible in flexible circumstances. This paper presents a solution based on the popular Stage-Gate system, which is closely linked with virtual team approach. Virtual teams can provide a platform to advance the knowledge-base in a company and thus to reduce time-to-market. This article introduces conceptual product development architecture under a virtual team umbrella. The paper describes all the major aspects of new product development (NPD), NPD process and its relationship with virtual teams, Stage-Gate system finally presents a modified Stage-Gate system to cope up with the changing needs. It also provides the guidelines for the successful implementation of virtual teams in new product development.
Virtual Collaborative R&D Teams in Malaysia Manufacturing SMEs
Venue: arXiv cs.OH 2012
Year: 2012

This paper presents the results of empirical research conducted during March to September 2009. The study focused on the influence of virtual research and development teams within Malaysian manufacturing small and medium sized enterprises (SMEs). The specific objective of the study is better understanding of the application of collaborative technologies in business, to find the effective factors to assist SMEs to remain competitive in the future. The paper stresses to find an answer for a question Is there any relationship between company size, Internet connection facility and virtuality?. The survey data shows SMEs are now technologically capable of performing the virtual collaborative team, but the infrastructure usage is less. SMEs now have the necessary technology to begin the implementation process of collaboration tools to reduce research and development time, costs and increase productivity. So, the manager of R and D should take the potentials of virtual teams into account.
Algorithm Selection for Combinatorial Search Problems: A Survey
Venue: arXiv cs.AI 2012
Year: 2012

The Algorithm Selection Problem is concerned with selecting the best algorithm to solve a given problem on a case-by-case basis. It has become especially relevant in the last decade, as researchers are increasingly investigating how to identify the most suitable existing algorithm for solving a problem instead of developing new algorithms. This survey presents an overview of this work focusing on the contributions made in the area of combinatorial search problems, where Algorithm Selection techniques have achieved significant performance improvements. We unify and organise the vast literature according to criteria that determine Algorithm Selection systems in practice. The comprehensive classification of approaches identifies and analyses the different directions from which Algorithm Selection has been approached. This paper contrasts and compares different methods for solving the problem as well as ways of using these solutions. It closes by identifying directions of current and future research.
Beltrami Representation and its applications to texture map and video compression
Venue: arXiv cs.MM 2012
Year: 2012

Surface parameterizations and registrations are important in computer graphics and imaging, where 1-1 correspondences between meshes are computed. In practice, surface maps are usually represented and stored as 3D coordinates each vertex is mapped to, which often requires lots of storage memory. This causes inconvenience in data transmission and data storage. To tackle this problem, we propose an effective algorithm for compressing surface homeomorphisms using Fourier approximation of the Beltrami representation. The Beltrami representation is a complex-valued function defined on triangular faces of the surface mesh with supreme norm strictly less than 1. Under suitable normalization, there is a 1-1 correspondence between the set of surface homeomorphisms and the set of Beltrami representations. Hence, every bijective surface map is associated with a unique Beltrami representation. Conversely, given a Beltrami representation, the corresponding bijective surface map can be exactly reconstructed using the Linear Beltrami Solver introduced in this paper. Using the Beltrami representation, the surface homeomorphism can be easily compressed by Fourier approximation, without distorting the bijectivity of the map. The storage memory can be effectively reduced, which is useful for many practical problems in computer graphics and imaging. In this paper, we proposed to apply the algorithm to texture map compression and video compression. With our proposed algorithm, the storage requirement for the texture properties of a textured surface can be significantly reduced. Our algorithm can further be applied to compressing motion vector fields for video compression, which effectively improve the compression ratio.
Strict localization of eigenvectors and eigenvalues
Venue: arXiv cs.NA 2012
Year: 2012

In this article we show and implement a simple and effcient method to strictly locate eigenvectors and eigenvalues of a given matrix, based on the modified cone condition. As a consequence we can also effectively localize zeros of complex polynomials.
Compact Support Biorthogonal Wavelet Filterbanks for Arbitrary Undirected Graphs
Venue: arXiv cs.IT 2012
Year: 2012

In our recent work, we proposed the design of perfect reconstruction orthogonal wavelet filterbanks, called graph- QMF, for arbitrary undirected weighted graphs. In that formulation we first designed "one-dimensional" two-channel filterbanks on bipartite graphs, and then extended them to "multi-dimensional" separable two-channel filterbanks for arbitrary graphs via a bipartite subgraph decomposition. We specifically designed wavelet filters based on the spectral decomposition of the graph, and stated necessary and sufficient conditions for a two-channel graph filter-bank on bipartite graphs to provide aliasing-cancellation, perfect reconstruction and orthogonal set of basis (orthogonality). While, the exact graph-QMF designs satisfy all the above conditions, they are not exactly k-hop localized on the graph. In this paper, we relax the condition of orthogonality to design a biorthogonal pair of graph-wavelets that can have compact spatial spread and still satisfy the perfect reconstruction conditions. The design is analogous to the standard Cohen-Daubechies-Feauveau's (CDF) construction of factorizing a maximally-flat Daubechies half-band filter. Preliminary results demonstrate that the proposed filterbanks can be useful for both standard signal processing applications as well as for signals defined on arbitrary graphs. Note: Code examples from this paper are available at http://biron.usc.edu/wiki/index.php/Graph Filterbanks
A stopping criterion for Markov chains when generating independent random graphs
Venue: arXiv cs.SI 2012
Year: 2012

Markov chains are convenient means of generating realizations of networks with a given (joint or otherwise) degree distribution, since they simply require a procedure for rewiring edges. The major challenge is to find the right number of steps to run such a chain, so that we generate truly independent samples. Theoretical bounds for mixing times of these Markov chains are too large to be practically useful. Practitioners have no useful guide for choosing the length, and tend to pick numbers fairly arbitrarily. We give a principled mathematical argument showing that it suffices for the length to be proportional to the number of desired number of edges. We also prescribe a method for choosing this proportionality constant. We run a series of experiments showing that the distributions of common graph properties converge in this time, providing empirical evidence for our claims.
Performance Indicator for MIMO MMSE Receivers in the Presence of Channel Estimation Error
Venue: arXiv cs.PF 2012
Year: 2012

We present the derivation of post-processing SNR for Minimum-Mean-Squared-Error (MMSE) receivers with imperfect channel estimates, and show that it is an accurate indicator of the error rate performance of MIMO systems in the presence of channel estimation error. Simulation results show the tightness of the analysis.