OpenRaiser/Intern-Atlas huggingface dataset:
Propositional computability logic I
Venue: arXiv cs.LO 2004
Year: 2004

In the same sense as classical logic is a formal theory of truth, the recently initiated approach called computability logic is a formal theory of computability. It understands (interactive) computational problems as games played by a machine against the environment, their computability as existence of a machine that always wins the game, logical operators as operations on computational problems, and validity of a logical formula as being a scheme of "always computable" problems. The present contribution gives a detailed exposition of a soundness and completeness proof for an axiomatization of one of the most basic fragments of computability logic. The logical vocabulary of this fragment contains operators for the so called parallel and choice operations, and its atoms represent elementary problems, i.e. predicates in the standard sense. This article is self-contained as it explains all relevant concepts. While not technically necessary, however, familiarity with the foundational paper "Introduction to computability logic" [Annals of Pure and Applied Logic 123 (2003), pp.1-99] would greatly help the reader in understanding the philosophy, underlying motivations, potential and utility of computability logic, -- the context that determines the value of the present results. Online introduction to the subject is available at http://www.cis.upenn.edu/~giorgi/cl.html and http://www.csc.villanova.edu/~japaridz/CL/gsoll.html .
Computability Logic: a formal theory of interaction
Venue: arXiv cs.LO 2004
Year: 2004

Computability logic is a formal theory of (interactive) computability in the same sense as classical logic is a formal theory of truth. This approach was initiated very recently in "Introduction to computability logic" (Annals of Pure and Applied Logic 123 (2003), pp.1-99). The present paper reintroduces computability logic in a more compact and less technical way. It is written in a semitutorial style with a general computer science, logic or mathematics audience in mind. An Internet source on the subject is available at http://www.cis.upenn.edu/~giorgi/cl.html, and additional material at http://www.csc.villanova.edu/~japaridz/CL/gsoll.html .
Model-checking Driven Black-box Testing Algorithms for Systems with Unspecified Components
Venue: arXiv cs.SE 2004
Year: 2004

Component-based software development has posed a serious challenge to system verification since externally-obtained components could be a new source of system failures. This issue can not be completely solved by either model-checking or traditional software testing techniques alone due to several reasons: 1) externally obtained components are usually unspecified/partially specified; 2)it is generally difficult to establish an adequacy criteria for testing a component; 3)components may be used to dynamically upgrade a system. This paper introduces a new approach (called {\em model-checking driven black-box testing}) that combines model-checking with traditional black-box software testing to tackle the problem in a complete, sound, and automatic way. The idea is to, with respect to some requirement (expressed in CTL or LTL) about the system, use model-checking techniques to derive a condition (expressed in communication graphs) for an unspecified component such that the system satisfies the requirement iff the condition is satisfied by the component, and which can be established by testing the component with test cases generated from the condition on-the-fly. In this paper, we present model-checking driven black-box testing algorithms to handle both CTL and LTL requirements. We also illustrate the idea through some examples.
Near Rationality and Competitive Equilibria in Networked Systems
Venue: arXiv cs.GT 2004
Year: 2004

A growing body of literature in networked systems research relies on game theory and mechanism design to model and address the potential lack of cooperation between self-interested users. Most game-theoretic models applied to system research only describe competitive equilibria in terms of pure Nash equilibria, that is, a situation where the strategy of each user is deterministic, and is her best response to the strategies of all the other users. However, the assumptions necessary for a pure Nash equilibrium to hold may be too stringent for practical systems. Using three case studies on computer security, TCP congestion control, and network formation, we outline the limits of game-theoretic models relying on Nash equilibria, and we argue that considering competitive equilibria of a more general form may help reconcile predictions from game-theoretic models with empirically observed behavior.
A General Framework For Lazy Functional Logic Programming With Algebraic Polymorphic Types
Venue: arXiv cs.PL 2004
Year: 2004

We propose a general framework for first-order functional logic programming, supporting lazy functions, non-determinism and polymorphic datatypes whose data constructors obey a set C of equational axioms. On top of a given C, we specify a program as a set R of C-based conditional rewriting rules for defined functions. We argue that equational logic does not supply the proper semantics for such programs. Therefore, we present an alternative logic which includes C-based rewriting calculi and a notion of model. We get soundness and completeness for C-based rewriting w.r.t. models, existence of free models for all programs, and type preservation results. As operational semantics, we develop a sound and complete procedure for goal solving, which is based on the combination of lazy narrowing with unification modulo C. Our framework is quite expressive for many purposes, such as solving action and change problems, or realizing the GAMMA computation model.
Maximum-likelihood decoding of Reed-Solomon Codes is NP-hard
Venue: arXiv cs.CC 2004
Year: 2004

Maximum-likelihood decoding is one of the central algorithmic problems in coding theory. It has been known for over 25 years that maximum-likelihood decoding of general linear codes is NP-hard. Nevertheless, it was so far unknown whether maximum- likelihood decoding remains hard for any specific family of codes with nontrivial algebraic structure. In this paper, we prove that maximum-likelihood decoding is NP-hard for the family of Reed-Solomon codes. We moreover show that maximum-likelihood decoding of Reed-Solomon codes remains hard even with unlimited preprocessing, thereby strengthening a result of Bruck and Naor.
A Grid Service Broker for Scheduling Distributed Data-Oriented Applications on Global Grids
Venue: arXiv cs.DC 2004
Year: 2004

The next generation of scientific experiments and studies, popularly called as e-Science, is carried out by large collaborations of researchers distributed around the world engaged in analysis of huge collections of data generated by scientific instruments. Grid computing has emerged as an enabler for e-Science as it permits the creation of virtual organizations that bring together communities with common objectives. Within a community, data collections are stored or replicated on distributed resources to enhance storage capability or efficiency of access. In such an environment, scientists need to have the ability to carry out their studies by transparently accessing distributed data and computational resources. In this paper, we propose and develop a Grid broker that mediates access to distributed resources by (a) discovering suitable data sources for a given analysis scenario, (b) suitable computational resources, (c) optimally mapping analysis jobs to resources, (d) deploying and monitoring job execution on selected resources, (e) accessing data from local or remote data source during job execution and (f) collating and presenting results. The broker supports a declarative and dynamic parametric programming model for creating grid applications. We have used this model in grid-enabling a high energy physics analysis application (Belle Analysis Software Framework). The broker has been used in deploying Belle experiment data analysis jobs on a grid testbed, called Belle Analysis Data Grid, having resources distributed across Australia interconnected through GrangeNet.
The Largest Compatible Subset Problem for Phylogenetic Data
Venue: arXiv cs.AI 2004
Year: 2004

The phylogenetic tree construction is to infer the evolutionary relationship between species from the experimental data. However, the experimental data are often imperfect and conflicting each others. Therefore, it is important to extract the motif from the imperfect data. The largest compatible subset problem is that, given a set of experimental data, we want to discard the minimum such that the remaining is compatible. The largest compatible subset problem can be viewed as the vertex cover problem in the graph theory that has been proven to be NP-hard. In this paper, we propose a hybrid Evolutionary Computing (EC) method for this problem. The proposed method combines the EC approach and the algorithmic approach for special structured graphs. As a result, the complexity of the problem is dramatically reduced. Experiments were performed on randomly generated graphs with different edge densities. The vertex covers produced by the proposed method were then compared to the vertex covers produced by a 2-approximation algorithm. The experimental results showed that the proposed method consistently outperformed a classical 2- approximation algorithm. Furthermore, a significant improvement was found when the graph density was small.
Optimization of Evolutionary Neural Networks Using Hybrid Learning Algorithms
Venue: arXiv cs.AI 2004
Year: 2004

Evolutionary artificial neural networks (EANNs) refer to a special class of artificial neural networks (ANNs) in which evolution is another fundamental form of adaptation in addition to learning. Evolutionary algorithms are used to adapt the connection weights, network architecture and learning algorithms according to the problem environment. Even though evolutionary algorithms are well known as efficient global search algorithms, very often they miss the best local solutions in the complex solution space. In this paper, we propose a hybrid meta-heuristic learning approach combining evolutionary learning and local search methods (using 1st and 2nd order error information) to improve the learning and faster convergence obtained using a direct evolutionary approach. The proposed technique is tested on three different chaotic time series and the test results are compared with some popular neuro-fuzzy systems and a recently developed cutting angle method of global optimization. Empirical results reveal that the proposed technique is efficient in spite of the computational complexity.
A Distributed TDMA Slot Assignment Algorithm for Wireless Sensor Networks
Venue: arXiv cs.DC 2004
Year: 2004

Wireless sensor networks benefit from communication protocols that reduce power requirements by avoiding frame collision. Time Division Media Access methods schedule transmission in slots to avoid collision, however these methods often lack scalability when implemented in \emph{ad hoc} networks subject to node failures and dynamic topology. This paper reports a distributed algorithm for TDMA slot assignment that is self-stabilizing to transient faults and dynamic topology change. The expected local convergence time is O(1) for any size network satisfying a constant bound on the size of a node neighborhood.
Synchronous Relaxation for Parallel Ising Spin Simulations
Venue: arXiv cs.DC 2004
Year: 2004

A new parallel algorithm for simulating Ising spin systems is presented. The sequential prototype is the n-fold way algorithm cite{BKL75}, which is efficient but is hard to parallelize using conservative methods. Our parallel algorithm is optimistic. Unlike other optimistic algorithms, e.g., Time Warp, our algorithm is synchronous. It also belongs to the class of simulations known as ``relaxation'' cite{CS8 hence it is named ``synchronous relaxation.'' We derive performance guarantees for this algorithm. If N is the number of PEs, then under weak assumptions we show that the number of correct events processed per unit of time is, on average, at least of order N/log(N). All communication delays, processing time, and busy waits are taken into account.
MammoGrid: A Service Oriented Architecture based Medical Grid Application
Venue: arXiv cs.DC 2004
Year: 2004

The MammoGrid project has recently delivered its first proof-of-concept prototype using a Service-Oriented Architecture (SOA)-based Grid application to enable distributed computing spanning national borders. The underlying AliEn Grid infrastructure has been selected because of its practicality and because of its emergence as a potential open source standards-based solution for managing and coordinating distributed resources. The resultant prototype is expected to harness the use of huge amounts of medical image data to perform epidemiological studies, advanced image processing, radiographic education and ultimately, tele-diagnosis over communities of medical virtual organisations. The MammoGrid prototype comprises a high-quality clinician visualization workstation used for data acquisition and inspection, a DICOM-compliant interface to a set of medical services (annotation, security, image analysis, data storage and querying services) residing on a so-called Grid-box and secure access to a network of other Grid-boxes connected through Grid middleware. This paper outlines the MammoGrid approach in managing a federation of Grid-connected mammography databases in the context of the recently delivered prototype and will also describe the next phase of prototyping.
Reactive Programming in Standard ML
Venue: arXiv cs.PL 2004
Year: 2004

Reactive systems are systems that maintain an ongoing interaction with their environment, activated by receiving input events from the environment and producing output events in response. Modern programming languages designed to program such systems use a paradigm based on the notions of instants and activations. We describe a library for Standard ML that provides basic primitives for programming reactive systems. The library is a low-level system upon which more sophisticated reactive behaviors can be built, which provides a convenient framework for prototyping extensions to existing reactive languages.
High-Level Networking With Mobile Code And First Order AND-Continuations
Venue: arXiv cs.PL 2004
Year: 2004

We describe a scheme for moving living code between a set of distributed processes coordinated with unification based Linda operations, and its application to building a comprehensive Logic programming based Internet programming framework. Mobile threads are implemented by capturing first order continuations in a compact data structure sent over the network. Code is fetched lazily from its original base turned into a server as the continuation executes at the remote site. Our code migration techniques, in combination with a dynamic recompilation scheme, ensure that heavily used code moves up smoothly on a speed hierarchy while volatile dynamic code is kept in a quickly updatable form. Among the examples, we describe how to build programmable client and server components (Web servers, in particular) and mobile agents.
Propositional Defeasible Logic has Linear Complexity
Venue: arXiv cs.AI 2004
Year: 2004

Defeasible logic is a rule-based nonmonotonic logic, with both strict and defeasible rules, and a priority relation on rules. We show that inference in the propositional form of the logic can be performed in linear time. This contrasts markedly with most other propositional nonmonotonic logics, in which inference is intractable.
Pruning Search Space in Defeasible Argumentation
Venue: arXiv cs.AI 2004
Year: 2004

Defeasible argumentation has experienced a considerable growth in AI in the last decade. Theoretical results have been combined with development of practical applications in AI & Law, Case-Based Reasoning and various knowledge-based systems. However, the dialectical process associated with inference is computationally expensive. This paper focuses on speeding up this inference process by pruning the involved search space. Our approach is twofold. On one hand, we identify distinguished literals for computing defeat. On the other hand, we restrict ourselves to a subset of all possible conflicting arguments by introducing dialectical constraints.
A Framework for Combining Defeasible Argumentation with Labeled Deduction
Venue: arXiv cs.AI 2004
Year: 2004

In the last years, there has been an increasing demand of a variety of logical systems, prompted mostly by applications of logic in AI and other related areas. Labeled Deductive Systems (LDS) were developed as a flexible methodology to formalize such a kind of complex logical systems. Defeasible argumentation has proven to be a successful approach to formalizing commonsense reasoning, encompassing many other alternative formalisms for defeasible reasoning. Argument-based frameworks share some common notions (such as the concept of argument, defeater, etc.) along with a number of particular features which make it difficult to compare them with each other from a logical viewpoint. This paper introduces LDSar, a LDS for defeasible argumentation in which many important issues concerning defeasible argumentation are captured within a unified logical framework. We also discuss some logical properties and extensions that emerge from the proposed framework.
Zipf's law and the creation of musical context
Venue: arXiv cs.CL 2004
Year: 2004

This article discusses the extension of the notion of context from linguistics to the domain of music. In language, the statistical regularity known as Zipf's law -which concerns the frequency of usage of different words- has been quantitatively related to the process of text generation. This connection is established by Simon's model, on the basis of a few assumptions regarding the accompanying creation of context. Here, it is shown that the statistics of note usage in musical compositions are compatible with the predictions of Simon's model. This result, which gives objective support to the conceptual likeness of context in language and music, is obtained through automatic analysis of the digital versions of several compositions. As a by-product, a quantitative measure of context definiteness is introduced and used to compare tonal and atonal works.
Algorithms for Drawing Media
Venue: arXiv cs.DS 2004
Year: 2004

We describe algorithms for drawing media, systems of states, tokens and actions that have state transition graphs in the form of partial cubes. Our algorithms are based on two principles: embedding the state transition graph in a low-dimensional integer lattice and projecting the lattice onto the plane, or drawing the medium as a planar graph with centrally symmetric faces.
Better algorithms for unfair metrical task systems and applications
Venue: arXiv cs.DS 2004
Year: 2004

Unfair metrical task systems are a generalization of online metrical task systems. In this paper we introduce new techniques to combine algorithms for unfair metrical task systems and apply these techniques to obtain improved randomized online algorithms for metrical task systems on arbitrary metric spaces.
Propositional Computability Logic II
Venue: arXiv cs.LO 2004
Year: 2004

Computability logic is a formal theory of computational tasks and resources. Its formulas represent interactive computational problems, logical operators stand for operations on computational problems, and validity of a formula is understood as being a scheme of problems that always have algorithmic solutions. A comprehensive online source on the subject is available at http://www.cis.upenn.edu/~giorgi/cl.html . The earlier article "Propositional computability logic I" proved soundness and completeness for the (in a sense) minimal nontrivial fragment CL1 of computability logic. The present paper extends that result to the significantly more expressive propositional system CL2. What makes CL2 more expressive than CL1 is the presence of two sorts of atoms in its language: elementary atoms, representing elementary computational problems (i.e. predicates), and general atoms, representing arbitrary computational problems. CL2 conservatively extends CL1, with the latter being nothing but the general-atom-free fragment of the former.
Long Nonbinary Codes Exceeding the Gilbert - Varshamov Bound for any Fixed Distance
Venue: arXiv cs.IT 2004
Year: 2004

Let A(q,n,d) denote the maximum size of a q-ary code of length n and distance d. We study the minimum asymptotic redundancy ρ(q,n,d)=n-log_q A(q,n,d) as n grows while q and d are fixed. For any d and q<=d-1, long algebraic codes are designed that improve on the BCH codes and have the lowest asymptotic redundancy ρ(q,n,d) <= ((d-3)+1/(d-2)) log_q n known to date. Prior to this work, codes of fixed distance that asymptotically surpass BCH codes and the Gilbert-Varshamov bound were designed only for distances 4,5 and 6.
Non-Termination Inference of Logic Programs
Venue: arXiv cs.PL 2004
Year: 2004

We present a static analysis technique for non-termination inference of logic programs. Our framework relies on an extension of the subsumption test, where some specific argument positions can be instantiated while others are generalized. We give syntactic criteria to statically identify such argument positions from the text of a program. Atomic left looping queries are generated bottom-up from selected subsets of the binary unfoldings of the program of interest. We propose a set of correct algorithms for automating the approach. Then, non-termination inference is tailored to attempt proofs of optimality of left termination conditions computed by a termination inference tool. An experimental evaluation is reported. When termination and non-termination analysis produce complementary results for a logic procedure, then with respect to the leftmost selection rule and the language used to describe sets of atomic queries, each analysis is optimal and together, they induce a characterization of the operational behavior of the logic procedure.
Cheap Recovery: A Key to Self-Managing State
Venue: arXiv cs.NI 2004
Year: 2004

Cluster hash tables (CHTs) are a key persistent-storage component of many large-scale Internet services due to their high performance and scalability. We show that a correctly-designed CHT can also be as easy to manage as a farm of stateless servers. Specifically, we trade away some consistency to obtain reboot-based recovery that is simple, maintains full data availability, and only has modest impact on performance. This simplifies management in two ways. First, it simplifies failure detection by lowering the cost of acting on false positives, allowing us to use simple but aggressive statistical techniques to quickly detect potential failures and node degradations; even when a false alarm is raised or when rebooting will not fix the problem, attempting recovery by rebooting is relatively non-intrusive to system availability and performance. Second, it allows us to re-cast online repartitioning as failure plus recovery, simplifying dynamic scaling and capacity planning. These properties make it possible for the system to be continuously self-adjusting, a key property of self-managing, autonomic systems.
P=NP
Venue: arXiv cs.CC 2004
Year: 2004

We claim to resolve the P=?NP problem via a formal argument for P=NP.
Proofs of Zero Knowledge
Venue: arXiv cs.CR 2004
Year: 2004

We present a protocol for verification of ``no such entry'' replies from databases. We introduce a new cryptographic primitive as the underlying structure, the keyed hash tree, which is an extension of Merkle's hash tree. We compare our scheme to Buldas et al.'s Undeniable Attesters and Micali et al.'s Zero Knowledge Sets.