OpenRaiser/Intern-Atlas huggingface dataset:
Modeling the resilience of large and evolving systems
Venue: arXiv cs.PF 2012
Year: 2012

This paper summarizes the state of knowledge and ongoing research on methods and techniques for resilience evaluation, taking into account the resilience-scaling challenges and properties related to the ubiquitous computerized systems. We mainly focus on quantitative evaluation approaches and, in particular, on model-based evaluation techniques that are commonly used to evaluate and compare, from the dependability point of view, different architecture alternatives at the design stage. We outline some of the main modeling techniques aiming at mastering the largeness of analytical dependability models at the construction level. Actually, addressing the model largeness problem is important with respect to the investigation of the scalability of current techniques to meet the complexity challenges of ubiquitous systems. Finally we present two case studies in which some of the presented techniques are applied for modeling web services and General Packet Radio Service (GPRS) mobile telephone networks, as prominent examples of large and evolving systems.
DBR: A Simple, Fast and Efficient Dynamic Network Reconfiguration Mechanism Based on Deadlock Recovery Scheme
Venue: arXiv cs.DC 2012
Year: 2012

Dynamic network reconfiguration is described as the process of replacing one routing function with another while the network keeps running. The main challenge is avoiding deadlock anomalies while keeping limitations on message injection and forwarding minimal. Current approaches, whose complexity is so high that their practical applicability is limited, either require the existence of extra network resources like virtual channels, or they affect the performance of the network during the reconfiguration process. In this paper we present a simple, fast and efficient mechanism for dynamic network reconfiguration which is based on regressive deadlock recoveries instead of avoiding deadlocks. The mechanism which is referred to as DBR guarantees a deadlock-free reconfiguration based on wormhole switching (WS) and it does not require additional resources. In this approach, the need for a reliable message transmission has led to a modified WS mechanism which includes additional flits or control signals. DBR allows cycles to be formed and in such conditions when a deadlock occurs, the messages suffer from time-out. Then, this method releases the buffers and channels from the current node and thus the source retransmits the message after a random time gap. Evaluating results reveal that the mechanism shows substantial performance improvements over the other methods and it works efficiently in different topologies with various routing algorithms.
Inversion of Linear and Nonlinear Observable Systems with Series-defined Output Trajectories
Venue: arXiv cs.SY 2012
Year: 2012

The problem of inverting a system in presence of a series-defined output is analyzed. Inverse models are derived that consist of a set of algebraic equations. The inversion is performed explicitly for an output trajectory functional, which is a linear combination of some basis functions with arbitrarily free coefficients. The observer canonical form is exploited, and the input-output representation is solved using a series method. It is shown that the only required system characteristic is observability, which implies that there is no need for output redefinition. An exact inverse model is found for linear systems. For general nonlinear systems, a good approximation of the inverse model valid on a finite time interval is found.
Computationally Efficient Trajectory Optimization for Linear Control Systems with Input and State Constraints
Venue: arXiv cs.SY 2012
Year: 2012

This paper presents a trajectory generation method that optimizes a quadratic cost functional with respect to linear system dynamics and to linear input and state constraints. The method is based on continuous-time flatness-based trajectory generation, and the outputs are parameterized using a polynomial basis. A method to parameterize the constraints is introduced using a result on polynomial nonpositivity. The resulting parameterized problem remains linear-quadratic and can be solved using quadratic programming. The problem can be further simplified to a linear programming problem by linearization around the unconstrained optimum. The method promises to be computationally efficient for constrained systems with a high optimization horizon. As application, a predictive torque controller for a permanent magnet synchronous motor which is based on real-time optimization is presented.
Extending SPARQL to Support Entity Grouping and Path Queries
Venue: arXiv cs.DB 2012
Year: 2012

The ability to efficiently find relevant subgraphs and paths in a large graph to a given query is important in many applications including scientific data analysis, social networks, and business intelligence. Currently, there is little support and no efficient approaches for expressing and executing such queries. This paper proposes a data model and a query language to address this problem. The contributions include supporting the construction and selection of: (i) folder nodes, representing a set of related entities, and (ii) path nodes, representing a set of paths in which a path is the transitive relationship of two or more entities in the graph. Folders and paths can be stored and used for future queries. We introduce FPSPARQL which is an extension of the SPARQL supporting folder and path nodes. We have implemented a query engine that supports FPSPARQL and the evaluation results shows its viability and efficiency for querying large graph datasets.
Shadows and Headless Shadows: an Autobiographical Approach to Narrative Reasoning
Venue: arXiv cs.AI 2012
Year: 2012

The Xapagy architecture is a story-oriented cognitive system which relies exclusively on the autobiographical memory implemented as a raw collection of events. Reasoning is performed by shadowing current events with events from the autobiography. The shadows are then extrapolated into headless shadows (HLSs). In a story following mood, HLSs can be used to track the level of surprise of the agent, to infer hidden actions or relations between the participants, and to summarize ongoing events. In recall mood, the HLSs can be used to create new stories ranging from exact recall to free-form confabulation.
Shark: SQL and Rich Analytics at Scale
Venue: arXiv cs.DB 2012
Year: 2012

Shark is a new data analysis system that marries query processing with complex analytics on large clusters. It leverages a novel distributed memory abstraction to provide a unified engine that can run SQL queries and sophisticated analytics functions (e.g., iterative machine learning) at scale, and efficiently recovers from failures mid-query. This allows Shark to run SQL queries up to 100x faster than Apache Hive, and machine learning programs up to 100x faster than Hadoop. Unlike previous systems, Shark shows that it is possible to achieve these speedups while retaining a MapReduce-like execution engine, and the fine-grained fault tolerance properties that such engines provide. It extends such an engine in several ways, including column-oriented in-memory storage and dynamic mid-query replanning, to effectively execute SQL. The result is a system that matches the speedups reported for MPP analytic databases over MapReduce, while offering fault tolerance properties and complex analytics capabilities that they lack.
A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets
Venue: arXiv cs.LO 2012
Year: 2012

Timed-arc Petri nets (TAPN) are a well-known time extension of the Petri net model and several translations to networks of timed automata have been proposed for this model. We present a direct, DBM-based algorithm for forward reachability analysis of bounded TAPNs extended with transport arcs, inhibitor arcs and age invariants. We also give a complete proof of its correctness, including reduction techniques based on symmetries and extrapolation. Finally, we augment the algorithm with a novel state-space reduction technique introducing a monotonic ordering on markings and prove its soundness even in the presence of monotonicity-breaking features like age invariants and inhibitor arcs. We implement the algorithm within the model-checker TAPAAL and the experimental results document an encouraging performance compared to verification approaches that translate TAPN models to UPPAAL timed automata.
Time-Darts: A Data Structure for Verification of Closed Timed Automata
Venue: arXiv cs.DS 2012
Year: 2012

Symbolic data structures for model checking timed systems have been subject to a significant research, with Difference Bound Matrices (DBMs) still being the preferred data structure in several mature verification tools. In comparison, discretization offers an easy alternative, with all operations having linear-time complexity in the number of clocks, and yet valid for a large class of closed systems. Unfortunately, fine-grained discretization causes itself a state-space explosion. We introduce a new data structure called time-darts for the symbolic representation of state-spaces of timed automata. Compared with the complete discretization, a single time-dart allows to represent an arbitrary large set of states, yet the time complexity of operations on time-darts remain linear in the number of clocks. We prove the correctness of the suggested reachability algorithm and perform several experiments in order to compare the performance of time-darts and the complete discretization. The main conclusion is that in all our experiments the time-dart method outperforms the complete discretization and it scales significantly better for models with larger constants.
Verifying Probabilistic Correctness in Isabelle with pGCL
Venue: arXiv cs.LO 2012
Year: 2012

This paper presents a formalisation of pGCL in Isabelle/HOL. Using a shallow embedding, we demonstrate close integration with existing automation support. We demonstrate the facility with which the model can be extended to incorporate existing results, including those of the L4.verified project. We motivate the applicability of the formalism to the mechanical verification of probabilistic security properties, including the effectiveness of side-channel countermeasures in real systems.
Optimal Rate Irregular LDPC Codes in Binary Erasure Channel
Venue: arXiv cs.IT 2012
Year: 2012

In this paper, we design the optimal rate capacity approaching irregular Low-Density Parity-Check code ensemble over Binary Erasure Channel, by using practical Semi-Definite Programming approach. Our method does not use any relaxation or any approximate solution unlike previous works. Our simulation results include two parts; first, we present some codes and their degree distribution functions that their rates are close to the capacity. Second, the maximum achievable rate behavior of codes in our method is illustrated through some figures.
The Refined Calculus of Inductive Construction: Parametricity and Abstraction
Venue: arXiv cs.LO 2012
Year: 2012

We present a refinement of the Calculus of Inductive Constructions in which one can easily define a notion of relational parametricity. It provides a new way to automate proofs in an interactive theorem prover like Coq.
New Hoopoe Heuristic Optimization
Venue: arXiv cs.NE 2012
Year: 2012

Most optimization problems in real life applications are often highly nonlinear. Local optimization algorithms do not give the desired performance. So, only global optimization algorithms should be used to obtain optimal solutions. This paper introduces a new nature-inspired metaheuristic optimization algorithm, called Hoopoe Heuristic (HH). In this paper, we will study HH and validate it against some test functions. Investigations show that it is very promising and could be seen as an optimization of the powerful algorithm of cuckoo search. Finally, we discuss the features of Hoopoe Heuristic and propose topics for further studies.
Optimization of measurement configurations for geometrical calibration of industrial robot
Venue: arXiv cs.RO 2012
Year: 2012

The paper is devoted to the geometrical calibration of industrial robots employed in precise manufacturing. To identify geometric parameters, an advanced calibration technique is proposed that is based on the non-linear experiment design theory, which is adopted for this particular application. In contrast to previous works, the calibration experiment quality is evaluated using a concept of the user-defined test-pose. In the frame of this concept, the related optimization problem is formulated and numerical routines are developed, which allow user to generate optimal set of manipulator configurations for a given number of calibration experiments. The efficiency of the developed technique is illustrated by several examples.
Sum-Rate Optimal Multi-Code CDMA Systems: An Equivalence Result
Venue: arXiv cs.IT 2012
Year: 2012

In this paper, the sum rate of a multi-code CDMA system with asymmetric-power users is maximized, given a processing gain and a power profile of users. Unlike the sum-rate maximization for a single-code CDMA system, the optimization requires the joint optimal distribution of each user's power to its multiple data streams as well as the optimal design of signature sequences. The crucial step is to establish an equivalence of the multi-code CDMA system to restricted FDMA and TDMA systems. The CDMA system has upper limits on the numbers of multi-codes of users, while the FDMA and the TDMA systems have upper limits on the bandwidths and the duty cycles of users, respectively, in addition to total bandwidth constraint. The equivalence facilitates the complete characterization of the maximum sum rate of the multi-code CDMA system and also provides new insights into the single- and the multi-code CDMA systems in terms of the parameters of the equivalent FDMA and TDMA systems.
Subexponential and FPT-time Inapproximability of Independent Set and Related Problems
Venue: arXiv cs.CC 2012
Year: 2012

Fixed-parameter algorithms, approximation algorithms and moderately exponential algorithms are three major approaches to algorithms design. While each of them being very active in its own, there is an increasing attention to the connection between different approaches. In particular, whether Maximum Independent Set would be better approximable once endowed with subexponential-time or FPT-time is a central question. In this paper, we present a strong link between the linear PCP conjecture and the inapproximability, thus partially answering this question.
On the Concrete Categories of Graphs
Venue: arXiv cs.DM 2012
Year: 2012

In the standard Category of Graphs, the graphs allow only one edge to be incident to any two vertices, not necessarily distinct, and the graph morphisms must map edges to edges and vertices to vertices while preserving incidence. We refer to these graph morphisms as Strict Morphisms. We relax the condition on the graphs allowing any number of edges to be incident to any two vertices, as well as relaxing the condition on graph morphisms by allowing edges to be mapped to vertices, provided that incidence is still preserved. We call this broader graph category The Category of Conceptual Graphs, and define four other graph categories created by combinations of restrictions of the graph morphisms as well as restrictions on the allowed graphs. We investigate which Lawvere axioms for the category of Sets and Functions apply to each of these Categories of Graphs, as well as the other categorial constructions of free objects, projective objects, generators, and their categorial duals.
Context Visualization for Social Bookmark Management
Venue: arXiv cs.HC 2012
Year: 2012

We present the design of a new social bookmark manager, named GalViz, as part of the interface of the GiveA-Link system. Unlike the interfaces of traditional social tagging tools, which usually display information in a list view, GalViz visualizes tags, resources, social links, and social context in an interactive network, combined with the tag cloud. Evaluations through a scenario case study and log analysis provide evidence of the effectiveness of our design.
Aspects of Polar-Coded Modulation
Venue: arXiv cs.IT 2012
Year: 2012

We consider the joint design of polar coding and higher-order modulation schemes for ever increased spectral efficiency. The close connection between the polar code construction and the multi-level coding approach is described in detail. Relations between different modulation schemes such as bit-interleaved coded modulation (BICM) and multi-level coding (MLC) in case of polar-coded modulation as well as the influence of the applied labeling rule and the selection of frozen channels are demonstrated.
Secure and Reliable Transmission with Cooperative Relays in Two-Hop Wireless Networks
Venue: arXiv cs.NI 2012
Year: 2012

This work considers the secure and reliable information transmission in two-hop relay wireless networks without the information of both eavesdropper channels and locations. While the previous work on this problem mainly studied infinite networks and their asymptotic behavior and scaling law results, this papers focuses on a more practical network with finite number of system nodes and explores the corresponding exact results on the number of eavesdroppers the network can tolerant to ensure a desired secrecy and reliability. For achieving secure and reliable information transmission in a finite network, two transmission protocols are considered in this paper, one adopts an optimal but complex relay selection process with less load balance capacity while the other adopts a random but simple relay selection process with good load balance capacity. Theoretical analysis is further provided to determine the exact and maximum number of independent and also uniformly distributed eavesdroppers one network can tolerate to satisfy a specified requirement in terms of the maximum secrecy outage probability and maximum transmission outage probability allowed.
Governance of Spreadsheets through Spreadsheet Change Reviews
Venue: arXiv cs.SE 2012
Year: 2012

We present a pragmatic method for management of risks that arise due to spreadsheet use in large organizations. We combine peer-review, tool-assisted evaluation and other pre-existing approaches into a single organization-wide approach that reduces spreadsheet risk without overly restricting spreadsheet use. The method was developed in the course of several spreadsheet evaluation assignments for a corporate customer. Our method addresses a number of issues pertinent to spreadsheet risks that were raised by the Sarbanes-Oxley act.
SVD Based Image Processing Applications: State of The Art, Contributions and Research Challenges
Venue: arXiv cs.CV 2012
Year: 2012

Singular Value Decomposition (SVD) has recently emerged as a new paradigm for processing different types of images. SVD is an attractive algebraic transform for image processing applications. The paper proposes an experimental survey for the SVD as an efficient transform in image processing applications. Despite the well-known fact that SVD offers attractive properties in imaging, the exploring of using its properties in various image applications is currently at its infancy. Since the SVD has many attractive properties have not been utilized, this paper contributes in using these generous properties in newly image applications and gives a highly recommendation for more research challenges. In this paper, the SVD properties for images are experimentally presented to be utilized in developing new SVD-based image processing applications. The paper offers survey on the developed SVD based image applications. The paper also proposes some new contributions that were originated from SVD properties analysis in different image processing. The aim of this paper is to provide a better understanding of the SVD in image processing and identify important various applications and open research directions in this increasingly important area; SVD based image processing in the future research.
Unshuffling a Square is NP-Hard
Venue: arXiv cs.CC 2012
Year: 2012

A shuffle of two strings is formed by interleaving the characters into a new string, keeping the characters of each string in order. A string is a square if it is a shuffle of two identical strings. There is a known polynomial time dynamic programming algorithm to determine if a given string z is the shuffle of two given strings x,y; however, it has been an open question whether there is a polynomial time algorithm to determine if a given string z is a square. We resolve this by proving that this problem is NP-complete via a many-one reduction from 3- Partition.
A Routine for Measuring Synergy in University-Industry-Government Relations: Mutual Information as a Triple-Helix and Quadruple-Helix Indicator
Venue: arXiv cs.CY 2012
Year: 2012

Mutual information in three (or more) dimensions can be considered as a Triple-Helix indicator of synergy in university-industry-government relations. An open-source routine th4.exe makes the computation of this indicator interactively available at the Internet, and thus applicable to large sets of data. Th4.exe computes all probabilistic entropies and mutual information in two, three, and, if available in the data, four dimensions among, for example, classes such as geographical addresses (cities, regions), technological codes (e.g., OECD's NACE codes), and size categories; or, alternatively, among institutional addresses (academic, industrial, public sector) in document sets. The relations between the Triple-Helix indicator -- as an indicator of synergy -- and the Triple-Helix model that specifies the possibility of feedback by an overlay of communications, are also discussed.
Distributed Optimization via Adaptive Regularization for Large Problems with Separable Constraints
Venue: arXiv cs.DC 2012
Year: 2012

Many practical applications require solving an optimization over large and high-dimensional data sets, which makes these problems hard to solve and prohibitively time consuming. In this paper, we propose a parallel distributed algorithm that uses an adaptive regularizer (PDAR) to solve a joint optimization problem with separable constraints. The regularizer is adaptive and depends on the step size between iterations and the iteration number. We show theoretical converge of our algorithm to an optimal solution, and use a multi-agent three-bin resource allocation example to illustrate the effectiveness of the proposed algorithm. Numerical simulations show that our algorithm converges to the same optimal solution as other distributed methods, with significantly reduced computational time.