OpenRaiser/Intern-Atlas huggingface dataset:
Efficient Symmetry Reduction and the Use of State Symmetries for Symbolic Model Checking
Venue: arXiv cs.LO 2010
Year: 2010

One technique to reduce the state-space explosion problem in temporal logic model checking is symmetry reduction. The combination of symmetry reduction and symbolic model checking by using BDDs suffered a long time from the prohibitively large BDD for the orbit relation. Dynamic symmetry reduction calculates representatives of equivalence classes of states dynamically and thus avoids the construction of the orbit relation. In this paper, we present a new efficient model checking algorithm based on dynamic symmetry reduction. Our experiments show that the algorithm is very fast and allows the verification of larger systems. We additionally implemented the use of state symmetries for symbolic symmetry reduction. To our knowledge we are the first who investigated state symmetries in combination with BDD based symbolic model checking.
Causality and the Semantics of Provenance
Venue: arXiv cs.LO 2010
Year: 2010

Provenance, or information about the sources, derivation, custody or history of data, has been studied recently in a number of contexts, including databases, scientific workflows and the Semantic Web. Many provenance mechanisms have been developed, motivated by informal notions such as influence, dependence, explanation and causality. However, there has been little study of whether these mechanisms formally satisfy appropriate policies or even how to formalize relevant motivating concepts such as causality. We contend that mathematical models of these concepts are needed to justify and compare provenance techniques. In this paper we review a theory of causality based on structural models that has been developed in artificial intelligence, and describe work in progress on using causality to give a semantics to provenance graphs.
Algebraic characterisation of one-way patterns
Venue: arXiv cs.DS 2010
Year: 2010

We give a complete structural characterisation of the map the positive branch of a one-way pattern implements. We start with the representation of the positive branch in terms of the phase map decomposition, which is then further analysed to obtain the primary structure of the matrix M, representing the phase map decomposition in the computational basis. Using this approach we obtain some preliminary results on the connection between the columns structure of a given unitary and the angles of measurements in a pattern that implements it. We believe this work is a step forward towards a full characterisation of those unitaries with an efficient one-way model implementation.
Semantics of a Typed Algebraic Lambda-Calculus
Venue: arXiv cs.LO 2010
Year: 2010

Algebraic lambda-calculi have been studied in various ways, but their semantics remain mostly untouched. In this paper we propose a semantic analysis of a general simply-typed lambda-calculus endowed with a structure of vector space. We sketch the relation with two established vectorial lambda-calculi. Then we study the problems arising from the addition of a fixed point combinator and how to modify the equational theory to solve them. We sketch an algebraic vectorial PCF and its possible denotational interpretations.
Computing by Means of Physics-Based Optical Neural Networks
Venue: arXiv cs.NE 2010
Year: 2010

We report recent research on computing with biology-based neural network models by means of physics-based opto-electronic hardware. New technology provides opportunities for very-high-speed computation and uncovers problems obstructing the wide-spread use of this new capability. The Computation Modeling community may be able to offer solutions to these cross-boundary research problems.
On Secure Workflow Decentralisation on the Internet
Venue: arXiv cs.CR 2010
Year: 2010

Decentralised workflow management systems are a new research area, where most work to-date has focused on the system's overall architecture. As little attention has been given to the security aspects in such systems, we follow a security driven approach, and consider, from the perspective of available security building blocks, how security can be implemented and what new opportunities are presented when empowering the decentralised environment with modern distributed security protocols. Our research is motivated by a more general question of how to combine the positive enablers that email exchange enjoys, with the general benefits of workflow systems, and more specifically with the benefits that can be introduced in a decentralised environment. This aims to equip email users with a set of tools to manage the semantics of a message exchange, contents, participants and their roles in the exchange in an environment that provides inherent assurances of security and privacy. This work is based on a survey of contemporary distributed security protocols, and considers how these protocols could be used in implementing a distributed workflow management system with decentralised control . We review a set of these protocols, focusing on the required message sequences in reviewing the protocols, and discuss how these security protocols provide the foundations for implementing core control-flow, data, and resource patterns in a distributed workflow environment.
The Deterministic Dendritic Cell Algorithm
Venue: arXiv cs.AI 2010
Year: 2010

The Dendritic Cell Algorithm is an immune-inspired algorithm orig- inally based on the function of natural dendritic cells. The original instantiation of the algorithm is a highly stochastic algorithm. While the performance of the algorithm is good when applied to large real-time datasets, it is difficult to anal- yse due to the number of random-based elements. In this paper a deterministic version of the algorithm is proposed, implemented and tested using a port scan dataset to provide a controllable system. This version consists of a controllable amount of parameters, which are experimented with in this paper. In addition the effects are examined of the use of time windows and variation on the number of cells, both which are shown to influence the algorithm. Finally a novel metric for the assessment of the algorithms output is introduced and proves to be a more sensitive metric than the metric used with the original Dendritic Cell Algorithm.
Autonomic Management of Maintenance Scheduling in Chord
Venue: arXiv cs.NI 2010
Year: 2010

This paper experimentally evaluates the effects of applying autonomic management to the scheduling of maintenance operations in a deployed Chord network, for various membership churn and workload patterns. Two versions of an autonomic management policy were compared with a static configuration. The autonomic policies varied with respect to the aggressiveness with which they responded to peer access error rates and to wasted maintenance operations. In most experiments, significant improvements due to autonomic management were observed in the performance of routing operations and the quantity of data transmitted between network members. Of the autonomic policies, the more aggressive version gave slightly better results.
Parallel Approximation Algorithms for Facility-Location Problems
Venue: arXiv cs.DS 2010
Year: 2010

This paper presents the design and analysis of parallel approximation algorithms for facility-location problems, including $\NC$ and $\RNC$ algorithms for (metric) facility location, $k$-center, $k$-median, and $k$-means. These problems have received considerable attention during the past decades from the approximation algorithms community, concentrating primarily on improving the approximation guarantees. In this paper, we ask, is it possible to parallelize some of the beautiful results from the sequential setting? Our starting point is a small, but diverse, subset of results in approximation algorithms for facility-location problems, with a primary goal of developing techniques for devising their efficient parallel counterparts. We focus on giving algorithms with low depth, near work efficiency (compared to the sequential versions), and low cache complexity. Common in algorithms we present is the idea that instead of picking only the most cost-effective element, we make room for parallelism by allowing a small slack (e.g., a $(1+\vareps)$ factor) in what can be selected---then, we use a clean-up step to ensure that the behavior does not deviate too much from the sequential steps. All the algorithms we developed are ``cache efficient'' in that the cache complexity is bounded by $O(w/B)$, where $w$ is the work in the EREW model and $B$ is the block size.
Distributed Agile Software Development: A Review
Venue: arXiv cs.SE 2010
Year: 2010

Distribution of software development is becoming more and more common in order to save the production cost and reduce the time to market. Large geographical distance, different time zones and cultural differences in distributed software development (DSD) leads to weak communication which adversely affects the project. Using agile practices for distributed development is also gaining momentum in various organizations to increase the quality and performance of the project. This paper explores the intersection of these two significant trends for software development i.e. DSD and agile. We discuss the challenges faced by geographically distributed agile teams and proven practices to address these issues, which will help in building a successful distributed team.
Perbandingan Shell Unix
Venue: arXiv cs.OS 2010
Year: 2010

Is it possible for an Information Technology [IT] product to be both mature and state-of-theart at the same time? In the case of the UNIX system, the answer is an unqualified "Yes." The UNIX system has continued to develop over the past twenty-five years. In millions of installations running on nearly every hardware platform made, the UNIX system has earned its reputation for stability and scalability. Over the years, UNIX system suppliers have steadily assimilated new technologies so that UNIX systems today provide more functionality as any other operating system.
Pembobolan website KPU (Komisi Pemilihan Umum) Apakah melanggar UU RI no.36 tahun 1999 tentang telekomunikasi ?
Venue: arXiv cs.OH 2010
Year: 2010

Information Technology KPU (Indonesia Electoral Commision) is a project in supporting democratization process in Indonesia. It is a part of General Election program of KPU-Indonesian Government. The aim of IT KPU is to build the transparency of the ballot result to the public (citizen and international world) and as the embrio of e government in Indonesia. It also has the aim for influence the citizen with Information Technology and the use of computer.
Information Delivery System through Bluetooth in Ubiquitous Networks
Venue: arXiv cs.NI 2010
Year: 2010

computers into the real world, to serve humans where the ubiquitous network is the underneath infrastructure. In order to provide ubiquitous services (u-Service) which deliver useful information to service users without human intervention, this paper implements a proactive information delivery system using Bluetooth technology. Bluetooth is a lowpowered networking service that supports several protocol profiles, most importantly file transfer.Combined together, ubiquitous computing and Bluetooth ha e the potential to furnish ubiquitous solutions (u-Solutions) that are efficient, employ simplified design characteristics, and collaboratively perform functions they are otherwise not capable. Thus, this paper first addresses the current Bluetooth technology. Then, it suggests and develops the proactive information delivery system utilizing Bluetooth and ubiquitous computing network concepts. The proactive information delivery system can be used in many ubiquitous applications such as ubiquitous commerce (u-Commerce) and ubiquitous education (u- Education)
SPIM Architecture for MVC based Web Applications
Venue: arXiv cs.NI 2010
Year: 2010

The Model / View / Controller design pattern divides an application environment into three components to handle the user-interactions, computations and output respectively. This separation greatly favors architectural reusability. The pattern works well in the case of single-address space and not proven to be efficient for web applications involving multiple address spaces. Web applications force the designers to decide which of the components of the pattern are to be partitioned between the server and client(s) before the design phase commences. For any rapidly growing web application, it is very difficult to incorporate future changes in policies related to partitioning. One solution to this problem is to duplicate the Model and controller components at both server and client(s). However, this may add further problems like delayed data fetch, security and scalability issues. In order to overcome this, a new architecture SPIM has been proposed that deals with the partitioning problem in an alternative way. SPIM shows tremendous improvements in performance when compared with a similar architecture.
Motion Detection Notification System by Short Messaging Service Using Network Camera and Global System for Mobile Modem
Venue: arXiv cs.NI 2010
Year: 2010

As the technology rapidly grows, the trend is clear that the use of mobile devices is gain an attention nowadays, thus designing a system by integrating it with notification feature is becoming an important aspect especially in tracking and monitoring system. Conventional security surveillance systems require the constant attention from the user, to monitor the location concurrently. In order to reduce the cost of computing power and advance technology of mobile phone in widespread acceptance of the Internet as a viable communication medium, this paper is aimed to design a low cost web-based system as a platform to view the image captured. When the network camera detects any movement from the intruders, it automatically captures the image and sends it to the database of the web-based directly by the network through File Transfer Protocol (FTP). The camera is attached through an Ethernet connection and power source. Therefore, the camera can be viewed from either standard Web browser or cell phone. Nowadays, when a security camera is installed, user is notified as long as the camera is switched on since any slight movement requires the attention of the supervisor. The utility of the system has proven theoretically. This system will also notify the user by sending a notification through Short Messages Services (SMS).
Robust PI Control Design Using Particle Swarm Optimization
Venue: arXiv cs.CE 2010
Year: 2010

This paper presents a set of robust PI tuning formulae for a first order plus dead time process using particle swarm optimization. Also, tuning formulae for an integrating process with dead time, which is a special case of a first order plus dead time process, is given. The design problem considers three essential requirements of control problems, namely load disturbance rejection, setpoint regulation and robustness of closed-loop system against model uncertainties. The primary design goal is to optimize load disturbance rejection. Robustness is guaranteed by requiring that the maximum sensitivity is less than or equal to a specified value. In the first step, PI controller parameters are determined such that the IAE criterion to a load disturbance step is minimized and the robustness constraint on maximum sensitivity is satisfied. Using a structure with two degrees of freedom which introduces an extra parameter, the setpoint weight, good setpoint regulation is achieved in the second step. The main advantage of the proposed method is its simplicity. Once the equivalent first order plus dead time model is determined, the PI parameters are explicitly given by a set of tuning formulae. In order to show the performance and effectiveness of the proposed tuning formulae, they are applied to three simulation examples.
Algorithm for Predicting Protein Secondary Structure
Venue: arXiv cs.CE 2010
Year: 2010

Predicting protein structure from amino acid sequence is one of the most important unsolved problems of molecular biology and biophysics.Not only would a successful prediction algorithm be a tremendous advance in the understanding of the biochemical mechanisms of proteins, but, since such an algorithm could conceivably be used to design proteins to carry out specific functions.Prediction of the secondary structure of a protein (alpha-helix, beta-sheet, coil) is an important step towards elucidating its three dimensional structure as well as its function. In this research, we use different Hidden Markov models for protein secondary structure prediction. In this paper we have proposed an algorithm for predicting protein secondary structure. We have used Hidden Markov model with sliding window for secondary structure prediction.The secondary structure has three regular forms, for each secondary structural element we are using one Hidden Markov Model.
An approach to find dynamic slice for C++ Program
Venue: arXiv cs.PL 2010
Year: 2010

Object-oriented programming has been considered a most promising method in program development and maintenance. An important feature of object-oriented programs (OOPs) is their reusability which can be achieved through the inheritance of classes or reusable components.Dynamic program slicing is an effective technique for narrowing the errors to the relevant parts of a program when debugging. Given a slicing criterion, the dynamic slice contains only those statements that actually affect the variables in the slicing criterion. This paper proposes a method to dynamically slice object-oriented (00) programs based on dependence analysis. It uses the Control Dependency Graph for object program and other static information to reduce the information to be traced during program execution. In this paper we present a method to find the dynamic Slice of object oriented programs where we are finding the slices for object and in case of function overloading.
A Decentralized Approach for Service Discovery & Availability in P-Grids
Venue: arXiv cs.NI 2010
Year: 2010

The widespread emergence of the Internet as a platform for electronic data distribution and the advent of structured information have revolutionized our ability to deliver information to any corner of the world. Although Service Oriented Architecture (SOA) is a paradigm for organizing and utilizing distributed capabilities that may be under the control of different ownership domains and implemented using various technology stacks and every organization may not be geared up for this. To harness the various software / service resources placed on various systems, we have proposed and implemented a model that is able to establish discovery and sharing in load balanced P-grid environment. The experimental results show that the proposed approach has dramatically lowered the network traffic (nearly negligible), while achieving load balancing in P2P grid systems. Our model is able to support discovery and sharing of resources also.
The Power of Nondeterminism in Self-Assembly
Venue: arXiv cs.CC 2010
Year: 2010

We investigate the role of nondeterminism in Winfree's abstract Tile Assembly Model (aTAM), which was conceived to model artificial molecular self-assembling systems constructed from DNA. Of particular practical importance is to find tile systems that minimize resources such as the number of distinct tile types, each of which corresponds to a set of DNA strands that must be custom-synthesized in actual molecular implementations of the aTAM. We seek to identify to what extent the use of nondeterminism in tile systems affects the resources required by such molecular shape-building algorithms. We first show a "molecular computability theoretic" result: there is an infinite shape S that is uniquely assembled by a tile system but not by any deterministic tile system. We then show an analogous phenomenon in the finitary "molecular complexity theoretic" case: there is a finite shape S that is uniquely assembled by a tile system with c tile types, but every deterministic tile system that uniquely assembles S has more than c tile types. In fact we extend the technique to derive a stronger (classical complexity theoretic) result, showing that the problem of finding the minimum number of tile types that uniquely assemble a given finite shape is Sigma-P-2-complete. In contrast, the problem of finding the minimum number of deterministic tile types that uniquely assemble a shape was shown to be NP-complete by Adleman, Cheng, Goel, Huang, Kempe, Moisset de Espanés, and Rothemund (Combinatorial Optimization Problems in Self-Assembly, STOC 2002). The conclusion is that nondeterminism confers extra power to assemble a shape from a small tile system, but unless the polynomial hierarchy collapses, it is computationally more difficult to exploit this power by finding the size of the smallest tile system, compared to finding the size of the smallest deterministic tile system.
How to generate an object under an ordinary Boltzmann distribution via an exponential Boltzmann sampler
Venue: arXiv cs.DM 2010
Year: 2010

This short note presents an efficient way to derive from an exponential Boltzmann sampler a ordinary Boltzmann sampler
Leveraging shared caches for parallel temporal blocking of stencil codes on multicore processors and clusters
Venue: arXiv cs.DC 2010
Year: 2010

Bandwidth-starved multicore chips have become ubiquitous. It is well known that the performance of stencil codes can be improved by temporal blocking, lessening the pressure on the memory interface. We introduce a new pipelined approach that makes explicit use of shared caches in multicore environments and minimizes synchronization and boundary overhead. Benchmark results are presented for three current x86-based microprocessors, showing clearly that our optimization works best on designs with high-speed shared caches and low memory bandwidth per core. We furthermore demonstrate that simple bandwidth-based performance models are inaccurate for this kind of algorithm and employ a more elaborate, synthetic modeling procedure. Finally we show that temporal blocking can be employed successfully in a hybrid shared/distributed-memory environment, albeit with limited benefit at strong scaling.
The Cover Time of Deterministic Random Walks
Venue: arXiv cs.DM 2010
Year: 2010

The rotor router model is a popular deterministic analogue of a random walk on a graph. Instead of moving to a random neighbor, the neighbors are served in a fixed order. We examine how fast this "deterministic random walk" covers all vertices (or all edges). We present general techniques to derive upper bounds for the vertex and edge cover time and derive matching lower bounds for several important graph classes. Depending on the topology, the deterministic random walk can be asymptotically faster, slower or equally fast as the classic random walk. We also examine the short term behavior of deterministic random walks, that is, the time to visit a fixed small number of vertices or edges.