OpenRaiser/Intern-Atlas huggingface dataset:
Security Policy Consistency
Venue: arXiv cs.LO 2000
Year: 2000

With the advent of wide security platforms able to express simultaneously all the policies comprising an organization's global security policy, the problem of inconsistencies within security policies become harder and more relevant. We have defined a tool based on the CHR language which is able to detect several types of inconsistencies within and between security policies and other specifications, namely workflow specifications. Although the problem of security conflicts has been addressed by several authors, to our knowledge none has addressed the general problem of security inconsistencies, on its several definitions and target specifications.
3-Coloring in Time O(1.3289^n)
Venue: arXiv cs.DS 2000
Year: 2000

We consider worst case time bounds for NP-complete problems including 3-SAT, 3-coloring, 3-edge-coloring, and 3-list-coloring. Our algorithms are based on a constraint satisfaction (CSP) formulation of these problems. 3-SAT is equivalent to (2,3)-CSP while the other problems above are special cases of (3,2)-CSP; there is also a natural duality transformation from (a,b)-CSP to (b,a)-CSP. We give a fast algorithm for (3,2)-CSP and use it to improve the time bounds for solving the other problems listed above. Our techniques involve a mixture of Davis-Putnam-style backtracking with more sophisticated matching and network flow based ideas.
Systematic Testing of Multicast Routing Protocols: Analysis of Forward and Backward Search Techniques
Venue: arXiv cs.NI 2000
Year: 2000

In this paper, we present a new methodology for developing systematic and automatic test generation algorithms for multipoint protocols. These algorithms attempt to synthesize network topologies and sequences of events that stress the protocol's correctness or performance. This problem can be viewed as a domain-specific search problem that suffers from the state space explosion problem. One goal of this work is to circumvent the state space explosion problem utilizing knowledge of network and fault modeling, and multipoint protocols. The two approaches investigated in this study are based on forward and backward search techniques. We use an extended finite state machine (FSM) model of the protocol. The first algorithm uses forward search to perform reduced reachability analysis. Using domain-specific information for multicast routing over LANs, the algorithm complexity is reduced from exponential to polynomial in the number of routers. This approach, however, does not fully automate topology synthesis. The second algorithm, the fault-oriented test generation, uses backward search for topology synthesis and uses backtracking to generate event sequences instead of searching forward from initial states. Using these algorithms, we have conducted studies for correctness of the multicast routing protocol PIM. We propose to extend these algorithms to study end-to-end multipoint protocols using a virtual LAN that represents delays of the underlying multicast distribution tree.
Incremental construction of minimal acyclic finite-state automata
Venue: arXiv cs.CL 2000
Year: 2000

In this paper, we describe a new method for constructing minimal, deterministic, acyclic finite-state automata from a set of strings. Traditional methods consist of two phases: the first to construct a trie, the second one to minimize it. Our approach is to construct a minimal automaton in a single phase by adding new strings one by one and minimizing the resulting automaton on-the-fly. We present a general algorithm as well as a specialization that relies upon the lexicographical ordering of the input strings.
Examples, Counterexamples, and Enumeration Results for Foldings and Unfoldings between Polygons and Polytopes
Venue: arXiv cs.CG 2000
Year: 2000

We investigate how to make the surface of a convex polyhedron (a polytope) by folding up a polygon and gluing its perimeter shut, and the reverse process of cutting open a polytope and unfolding it to a polygon. We explore basic enumeration questions in both directions: Given a polygon, how many foldings are there? Given a polytope, how many unfoldings are there to simple polygons? Throughout we give special attention to convex polygons, and to regular polygons. We show that every convex polygon folds to an infinite number of distinct polytopes, but that their number of combinatorially distinct gluings is polynomial. There are, however, simple polygons with an exponential number of distinct gluings. In the reverse direction, we show that there are polytopes with an exponential number of distinct cuttings that lead to simple unfoldings. We establish necessary conditions for a polytope to have convex unfoldings, implying, for example, that among the Platonic solids, only the tetrahedron has a convex unfolding. We provide an inventory of the polytopes that may unfold to regular polygons, showing that, for n>6, there is essentially only one class of such polytopes.
Polynomial-time Computation via Local Inference Relations
Venue: arXiv cs.LO 2000
Year: 2000

We consider the concept of a local set of inference rules. A local rule set can be automatically transformed into a rule set for which bottom-up evaluation terminates in polynomial time. The local-rule-set transformation gives polynomial-time evaluation strategies for a large variety of rule sets that cannot be given terminating evaluation strategies by any other known automatic technique. This paper discusses three new results. First, it is shown that every polynomial-time predicate can be defined by an (unstratified) local rule set. Second, a new machine-recognizable subclass of the local rule sets is identified. Finally we show that locality, as a property of rule sets, is undecidable in general.
Knowledge Theoretic Properties of Topological Spaces
Venue: arXiv cs.LO 2000
Year: 2000

We study the topological models of a logic of knowledge for topological reasoning, introduced by Larry Moss and Rohit Parikh. Among our results is a solution of a conjecture by the formentioned authors, finite satisfiability property and decidability for the theory of topological models.
Min-Max Fine Heaps
Venue: arXiv cs.DS 2000
Year: 2000

In this paper we present a new data structure for double ended priority queue, called min-max fine heap, which combines the techniques used in fine heap and traditional min-max heap. The standard operations on this proposed structure are also presented, and their analysis indicates that the new structure outperforms the traditional one.
Structure of some sand pile model
Venue: arXiv cs.DM 2000
Year: 2000

SPM (Sand Pile Model) is a simple discrete dynamical system used in physics to represent granular objects. It is deeply related to integer partitions, and many other combinatorics problems, such as tilings or rewriting systems. The evolution of the system started with n stacked grains generates a lattice, denoted by SPM(n). We study here the structure of this lattice. We first explain how it can be constructed, by showing its strong self-similarity property. Then, we define SPM(infini), a natural extension of SPM when one starts with an infinite number of grains. Again, we give an efficient construction algorithm and a coding of this lattice using a self-similar tree. The two approaches give different recursive formulae for the cardinal of SPM(n), where no closed formula have ever been found.
Measuring efficiency in high-accuracy, broad-coverage statistical parsing
Venue: arXiv cs.CL 2000
Year: 2000

Very little attention has been paid to the comparison of efficiency between high accuracy statistical parsers. This paper proposes one machine-independent metric that is general enough to allow comparisons across very different parsing architectures. This metric, which we call ``events considered'', measures the number of ``events'', however they are defined for a particular parser, for which a probability must be calculated, in order to find the parse. It is applicable to single-pass or multi-stage parsers. We discuss the advantages of the metric, and demonstrate its usefulness by using it to compare two parsers which differ in several fundamental ways.
Succinct quantum proofs for properties of finite groups
Venue: arXiv cs.CC 2000
Year: 2000

In this paper we consider a quantum computational variant of nondeterminism based on the notion of a quantum proof, which is a quantum state that plays a role similar to a certificate in an NP-type proof. Specifically, we consider quantum proofs for properties of black-box groups, which are finite groups whose elements are encoded as strings of a given length and whose group operations are performed by a group oracle. We prove that for an arbitrary group oracle there exist succinct (polynomial-length) quantum proofs for the Group Non-Membership problem that can be checked with small error in polynomial time on a quantum computer. Classically this is impossible--it is proved that there exists a group oracle relative to which this problem does not have succinct proofs that can be checked classically with bounded error in polynomial time (i.e., the problem is not in MA relative to the group oracle constructed). By considering a certain subproblem of the Group Non-Membership problem we obtain a simple proof that there exists an oracle relative to which BQP is not contained in MA. Finally, we show that quantum proofs for non-membership and classical proofs for various other group properties can be combined to yield succinct quantum proofs for other group properties not having succinct proofs in the classical setting, such as verifying that a number divides the order of a group and verifying that a group is not a simple group.
The Rectilinear Crossing Number of K_10 is 62
Venue: arXiv cs.DM 2000
Year: 2000

A drawing of a graph G in the plane is said to be a rectilinear drawing of G if the edges are required to be line segments (as opposed to Jordan curves). We assume no three vertices are collinear. The rectilinear crossing number of G is the fewest number of edge crossings attainable over all rectilinear drawings of G. Thanks to Richard Guy, exact values of the rectilinear crossing number of K_n, the complete graph on n vertices, for n = 3,...,9, are known (Guy 1972, White and Beinke 1978, Finch 2000, Sloanes A014540). Since 1971, thanks to the work of David Singer (1971, Gardiner 1986), the rectilinear crossing number of K_10 has been known to be either 61 or 62, a deceptively innocent and tantalizing statement. The difficulty of determining the correct value is evidenced by the fact that Singer's result has withstood the test of time. In this paper we use a purely combinatorial argument to show that the rectilinear crossing number of K_10 is 62. Moreover, using this result, we improve an asymptotic lower bound for a related problem. Finally, we close with some new and old open questions that were provoked, in part, by the results of this paper, and by the tangled history of the problem itself.
Computing the Depth of a Flat
Venue: arXiv cs.CG 2000
Year: 2000

We give algorithms for computing the regression depth of a k-flat for a set of n points in R^d. The running time is O(n^(d-2) + n log n) when 0 < k < d-1, faster than the best time bound for hyperplane regression or for data depth.
Design of an Electro-Hydraulic System Using Neuro-Fuzzy Techniques
Venue: arXiv cs.RO 2000
Year: 2000

Increasing demands in performance and quality make drive systems fundamental parts in the progressive automation of industrial processes. Their conventional models become inappropriate and have limited scope if one requires a precise and fast performance. So, it is important to incorporate learning capabilities into drive systems in such a way that they improve their accuracy in realtime, becoming more autonomous agents with some degree of intelligence. To investigate this challenge, this chapter presents the development of a learning control system that uses neuro-fuzzy techniques in the design of a tracking controller to an experimental electro-hydraulic actuator. We begin the chapter by presenting the neuro-fuzzy modeling process of the actuator. This part surveys the learning algorithm, describes the laboratorial system, and presents the modeling steps as the choice of actuator representative variables, the acquisition of training and testing data sets, and the acquisition of the neuro-fuzzy inverse-model of the actuator. In the second part of the chapter, we use the extracted neuro-fuzzy model and its learning capabilities to design the actuator position controller based on the feedback-error-learning technique. Through a set of experimental results, we show the generalization properties of the controller, its learning capability in actualizing in realtime the initial neuro-fuzzy inverse-model, and its compensation action improving the electro-hydraulics tracking performance.
Applications of Data Mining to Electronic Commerce
Venue: arXiv cs.LG 2000
Year: 2000

Electronic commerce is emerging as the killer domain for data mining technology. The following are five desiderata for success. Seldom are they they all present in one data mining application. 1. Data with rich descriptions. For example, wide customer records with many potentially useful fields allow data mining algorithms to search beyond obvious correlations. 2. A large volume of data. The large model spaces corresponding to rich data demand many training instances to build reliable models. 3. Controlled and reliable data collection. Manual data entry and integration from legacy systems both are notoriously problematic; fully automated collection is considerably better. 4. The ability to evaluate results. Substantial, demonstrable return on investment can be very convincing. 5. Ease of integration with existing processes. Even if pilot studies show potential benefit, deploying automated solutions to previously manual processes is rife with pitfalls. Building a system to take advantage of the mined knowledge can be a substantial undertaking. Furthermore, one often must deal with social and political issues involved in the automation of a previously manual business process.
Fault Detection using Immune-Based Systems and Formal Language Algorithms
Venue: arXiv cs.CE 2000
Year: 2000

This paper describes two approaches for fault detection: an immune-based mechanism and a formal language algorithm. The first one is based on the feature of immune systems in distinguish any foreign cell from the body own cell. The formal language approach assumes the system as a linguistic source capable of generating a certain language, characterised by a grammar. Each algorithm has particular characteristics, which are analysed in the paper, namely in what cases they can be used with advantage. To test their practicality, both approaches were applied on the problem of fault detection in an induction motor.
If P \neq NP then Some Strongly Noninvertible Functions are Invertible
Venue: arXiv cs.CC 2000
Year: 2000

Rabi, Rivest, and Sherman alter the standard notion of noninvertibility to a new notion they call strong noninvertibility, and show -- via explicit cryptographic protocols for secret-key agreement ([RS93,RS97] attribute this to Rivest and Sherman) and digital signatures [RS93,RS97] -- that strongly noninvertible functions would be very useful components in protocol design. Their definition of strong noninvertibility has a small twist (``respecting the argument given'') that is needed to ensure cryptographic usefulness. In this paper, we show that this small twist has a large, unexpected consequence: Unless P=NP, some strongly noninvertible functions are invertible.
Towards rule-based visual programming of generic visual systems
Venue: arXiv cs.PL 2000
Year: 2000

This paper illustrates how the diagram programming language DiaPlan can be used to program visual systems. DiaPlan is a visual rule-based language that is founded on the computational model of graph transformation. The language supports object-oriented programming since its graphs are hierarchically structured. Typing allows the shape of these graphs to be specified recursively in order to increase program security. Thanks to its genericity, DiaPlan allows to implement systems that represent and manipulate data in arbitrary diagram notations. The environment for the language exploits the diagram editor generator DiaGen for providing genericity, and for implementing its user interface and type checker.
Extraction of semantic relations from a Basque monolingual dictionary using Constraint Grammar
Venue: arXiv cs.CL 2000
Year: 2000

This paper deals with the exploitation of dictionaries for the semi-automatic construction of lexicons and lexical knowledge bases. The final goal of our research is to enrich the Basque Lexical Database with semantic information such as senses, definitions, semantic relations, etc., extracted from a Basque monolingual dictionary. The work here presented focuses on the extraction of the semantic relations that best characterise the headword, that is, those of synonymy, antonymy, hypernymy, and other relations marked by specific relators and derivation. All nominal, verbal and adjectival entries were treated. Basque uses morphological inflection to mark case, and therefore semantic relations have to be inferred from suffixes rather than from prepositions. Our approach combines a morphological analyser and surface syntax parsing (based on Constraint Grammar), and has proven very successful for highly inflected languages such as Basque. Both the effort to write the rules and the actual processing time of the dictionary have been very low. At present we have extracted 42,533 relations, leaving only 2,943 (9%) definitions without any extracted relation. The error rate is extremely low, as only 2.2% of the extracted relations are wrong.
Static Analysis Techniques for Equational Logic Programming
Venue: arXiv cs.LO 2000
Year: 2000

An equational logic program is a set of directed equations or rules, which are used to compute in the obvious way (by replacing equals with ``simpler'' equals). We present static analysis techniques for efficient equational logic programming, some of which have been implemented in $LR^2$, a laboratory for developing and evaluating fast, efficient, and practical rewriting techniques. Two novel features of $LR^2$ are that non-left-linear rules are allowed in most contexts and it has a tabling option based on the congruence-closure based algorithm to compute normal forms. Although, the focus of this research is on the tabling approach some of the techniques are applicable to the untabled approach as well. Our presentation is in the context of $LR^2$, which is an interpreter, but some of the techniques apply to compilation as well.
Abductive reasoning with temporal information
Venue: arXiv cs.CL 2000
Year: 2000

Texts in natural language contain a lot of temporal information, both explicit and implicit. Verbs and temporal adjuncts carry most of the explicit information, but for a full understanding general world knowledge and default assumptions have to be taken into account. We will present a theory for describing the relation between, on the one hand, verbs, their tenses and adjuncts and, on the other, the eventualities and periods of time they represent and their relative temporal locations, while allowing interaction with general world knowledge. The theory is formulated in an extension of first order logic and is a practical implementation of the concepts described in Van Eynde 2001 and Schelkens et al. 2000. We will show how an abductive resolution procedure can be used on this representation to extract temporal information from texts. The theory presented here is an extension of that in Verdoolaege et al. 2000, adapted to VanEynde 2001, with a simplified and extended analysis of adjuncts and with more emphasis on how a model can be constructed.
Available and Stabilizing 2-3 Trees
Venue: arXiv cs.DC 2000
Year: 2000

Transient faults corrupt the content and organization of data structures. A recovery technique dealing with such faults is stabilization, which guarantees, following some number of operations on the data structure, that content of the data structure is legitimate. Another notion of fault tolerance is availability, which is the property that operations continue to be applied during the period of recovery after a fault, and successful updates are not lost while the data structure stabilizes to a legitimate state. The available, stabilizing 2-3 tree supports find, insert, and delete operations, each with O(lg n) complexity when the tree's state is legitimate and contains n items. For an illegitimate state, these operations have O(lg K) complexity where K is the maximum capacity of the tree. Within O(t) operations, the state of the tree is guaranteed to be legitimate, where t is the number of nodes accessible via some path from the tree's root at the initial state. This paper resolves, for the first time, issues of dynamic allocation and pointer organization in a stabilizing data structure.
Questions for a Materialist Philosophy Implying the Equivalence of Computers and Human Cognition
Venue: arXiv cs.GL 2000
Year: 2000

Issues related to a materialist philosophy are explored as concerns the implied equivalence of computers running software and human observers. One issue explored concerns the measurement process in quantum mechanics. Another issue explored concerns the nature of experience as revealed by the existence of dreams. Some difficulties stemming from a materialist philosophy as regards these issues are pointed out. For example, a gedankenexperiment involving what has been called "negative" observation is discussed that illustrates the difficulty with a materialist assumption in quantum mechanics. Based on an exploration of these difficulties, specifications are outlined briefly that would provide a means to demonstrate the equivalence of of computers running software and human experience given a materialist assumption.
Value Withdrawal Explanation in CSP
Venue: arXiv cs.SE 2000
Year: 2000

This work is devoted to constraint solving motivated by the debugging of constraint logic programs a la GNU-Prolog. The paper focuses only on the constraints. In this framework, constraint solving amounts to domain reduction. A computation is formalized by a chaotic iteration. The computed result is described as a closure. This model is well suited to the design of debugging notions and tools, for example failure explanations or error diagnosis. In this paper we detail an application of the model to an explanation of a value withdrawal in a domain. Some other works have already shown the interest of such a notion of explanation not only for failure analysis.
A General Framework for Automatic Termination Analysis of Logic Programs
Venue: arXiv cs.PL 2000
Year: 2000

This paper describes a general framework for automatic termination analysis of logic programs, where we understand by ``termination'' the finitenes s of the LD-tree constructed for the program and a given query. A general property of mappings from a certain subset of the branches of an infinite LD-tree into a finite set is proved. From this result several termination theorems are derived, by using different finite sets. The first two are formulated for the predicate dependency and atom dependency graphs. Then a general result for the case of the query-mapping pairs relevant to a program is proved (cf. \cite{Sagiv,Lindenstrauss:Sagiv}). The correctness of the {\em TermiLog} system described in \cite{Lindenstrauss:Sagiv:Serebrenik} follows from it. In this system it is not possible to prove termination for programs involving arithmetic predicates, since the usual order for the integers is not well-founded. A new method, which can be easily incorporated in {\em TermiLog} or similar systems, is presented, which makes it possible to prove termination for programs involving arithmetic predicates. It is based on combining a finite abstraction of the integers with the technique of the query-mapping pairs, and is essentially capable of dividing a termination proof into several cases, such that a simple termination function suffices for each case. Finally several possible extensions are outlined.