We present a new proof methodology that uses dynamic process creation to capture the structure of recutsive distributed algorithms> Each recursive invocation of a distributed algorithm is modeled as a separate process, encouraging local reasoning about the individual recursive invocations and making explicit the communicatino that takes place among the concurrently executing invocations. Our methodology involves the construction of hierarchical correctness proofs in which the state of each individual call in a refined algorithm is mapped to the state of a corresponding call in a simpler or more abstract algorithm. ...Read More

This thesis investigates a process of designing a gesture system for a simple graphical editor on a pen-based computer. The graphical editor, named Box and Arrow Editor, was developed to test the designed gestures. The results of the testing and the evaluation of the principles used to formulate the gestures are presented. The design process covers issues of application of principles to gesture design, elimination of all menus, user evaluations and recognition problems.

At the heart of any communication system is the switching system for supporting connections between sets of endpoints. A switching system consists of one or more switching networks connected by communication links. Effective design of switching networks is critical to the success of a communication system. This paper proposes the study of three problems in the design of switching networks: design of nonblocking multirate distribution, evaluation of blocking probability in distributors and quantitative comparison of architectures. Each of these problems is significant in the design of practical networks and lacks ...Read More

Yang and Masson [14] have demonstrated that the Clos network is a nearly nonblocking distributer, with the proper choice of network parameters. The resulting network has better asymptotic crosspoint compleixty than other known constructions when the number of stages is fixed. In addition, the routing algorithm is efficient, taking time linear in the number of network inputs to route a new connection. We extend these results to the multirate environment in which each connection has an associated weight indicating the fraction of link bandwidth which it requires. Connections may share ...Read More

This paper examines the performance of synchronous checkpointing in a distributed computing environment with and without load redistribution. Performance models are developed, and optimum checkpoint intervals are determined. We extend earlier work by allowing for multiple nodes, state dependent checkpoint intervals, and a performance metric which is coupled with failure-free performance. We show that the optimum checkpoint intervals in the presence of load redestribution has a numerical solution in all cases and a closed form in many reasonable cases. These new results are then used to determine when performance can ...Read More

We have proposed a very high speed internet (VHSI) abstraction for the next generation of internetwork. An important component of the VHSI is a novel Multipoint Congram-Oriented High Performance Internet Protocol (MCHIP). The congram is the basic service primitive of MCHIP which incorporates strengths of both connection and datagram approaches. MCHIP supports two types of congrams: the user congram (UCon) and the persistent internet congram (PICon). A UCon is similar to a soft connection and can be used to provide strict performance guarantees to applications that need it. PICon are ...Read More

The major goal of the Completely Reliable Auto Shopping Heuristic (CRASH) system is to simulate a car buying marketplace using belief networks as the inference engine. This paper describes the design, knowledge acquisition, and implementation stages of the CRASH system. The paper also describes the additional work needed to implement CRASH as commercially viable product.

Future ATM networks will be required to support a plethora of services, transaction types and cell sequence behaviors with performance guarantees. Before this goal can be realized, however, some basically problems related to bandwidth allocation and traffic control in the ATM layer must be resolve. Such problems will in all likelihood defy solution as long as they studied in isolation without a unifying traffic characterization and traffic control framework. This work presented in this paper is part of an ongoing effort directed at the development of an integrated traffic characterization ...Read More

In this paper, we present a simple wp semantics and a programming law for the exit statement.

Belief networks have become an increasingly popular mechanism for dealing with uncertainty in systems. Unfortunately, it is known that finding the probability values of belief network nodes given a set of evidence is not tractable in general. Many different simulation algorithms for approximating solutions to this problem have been proposed and implemented. In this report, we describe the implementation of a collection of such algorithms, CABeN. CABeN contains a library of routines for simulating belief networks, a program for accessing the routines through menus on any 'tty' interface, and some ...Read More

The detection of temporal relationships among time-ordered patient data is an important, but difficult, clinical task. Large volumes of computer-stored clinical data offer the possibility of aiding in the early detection of subtle trends and states, but the presence of irrelevant data can obscure relevant findings and relationships. We present a formal system for representing complex temporal data as events on an abstract entity called a time limit. We define five time line operations, SLICE, FILTER, OVERLAY, NEW, and ADD. For each operation, we precisely define the operator's effect on ...Read More

The requirements for the rapid display of radiographic images exceed the capabilities of widely available display, computer and communication technologies. Computed radiography captures data with a resolution of about four megapixels. Large format displays are available that can present over four megapixels. One megapixel displays are practical for use in combination with large format displays and in areas where the viewing task does not require primary diagnosis. This paper describes an electronic radiology system that approximates the highest quality systems, but through the use of several interesting techniques allows the ...Read More

This proposal outlines a plan for the design, deployment, and operation of the high speed campus network at Washington University based on fast packet switching technology that has been developed here during the last several years. This new network will support ubiquitous multimedia workstations with high-resolution graphics and video capabilities, opening a wide range of new applications in research and education. It will support aggregate throughputs of hundreds of gigabits per second and will be designed to support port interfaces at up to 2.4 Gb/s. Initial implementations will emphasize 155 ...Read More

We have implemented a C-based graphic engine, called SwarmView, which is used to display animation traces as produced by SwarmExec the Prolong-based Swarm execution engine. SwarmView runs on a Silicon Graphics Personal Iris running IRIX, a UNIX-based operating system. This paper describes the major design elements of SwarmView. A basic familiarity with Swarm and its visualization extension is assumed; the interested reader is referred to the referenced papers. Familiarity with the paper "SwarmView Animation Vocabulary and Interpretation" is required; the appendices of this paper are reproduced from that one.

When using random clone overlap based methods to make DNA maps, fragment matching mistakes, the incorrect matching of similar length restriction fragments, are a common problem that produces incorrect maps. This technical report discusses techniques for fragment splitting and fragment combining, which attempts to correct maps containing a fragment matching mistake, given that the location of the mistake is known. These techniques are based on operations that decompose and merge virtual fragments (a collection of matched real fragments), add virtual fragments to existing groups in the map and insert virtual ...Read More

In this paper z-transform theory is used to develop the discrete orthonormal wavelet transpform for multidimensional signals. The tone is tutorial and expository. Some rudimentary knowledge of z-transforms and vector spaces is assumed. The wavelet transform of a signal consists of a sequence of inner products of a signal computed against the elements of a complete orthonorml set of basis vectors. The signal is recovered as a weighted sum of the basis vectors. This paper addresses the necessary and sufficient conditions that such a basis muct respect. An algorithm for ...Read More

Largely unnoticed amid the cry for better mathematics teaching, Kumon is quietly helping a million mathematics students (from infants to adults; 75% are elementary children). Though conservative in diction and device (including 5000+ worksheets to be solved in "standard" times), it is surprisingly student-centered in practice. The author's investigation during the past year reflects his background in both education and computer science. The paper considers the demands, theories, methods and record of Kumon mathematics from the standpoint of educational theory, cognitive science, and language processing. It considers syntactic and semantic ...Read More

Conflict resolution is a form of global control used in production systems to achieve an efficient sequential execution of a rule-based program. This type of control is not used to parallel production system models [6,13]. Instead, only those programs that make no assumptions regarding conflict resolution are executed in parallel. Therefore, the initial sequential rule-based programs are either executed in parallel without their conflict resolution strategy, which normally results in incorrect behavior, or the programs are transformed in an ad hoc manner to execute on an particular parallel production system ...Read More

Reliability, defined as the guarantee that a program satisfies its specifications, is an important aspect of many applications for which rule-based expert systems are suited. Verification refer to the process used to determine the reliability of the rule-based program. Because past approaches to verification are informal, guarantees of reliability cannot fully be made without severely restricting the system. On the other hand, by constructing formal specifications for a program and showing the program satisfies those specifications, guarantees of reliability can be made. This paper presents an assertional approach to the ...Read More

The conceptual aspects of and the implementation details of a set of self-identifying abstract data types (ADT) are described. Each of the ADTs constitutes a specific class of object, upon which a set of well-defined access functions is available. The intent of these ADTs is to supply a paradigm in which a class of object is available for manipulation, but in which the underlying implementation is hidden from the application programmer. Specific ADTs are the described in some detail. The tagged architecture used to achieve the self-identifying property of the ...Read More

Composition, superposition, and encapsulation are important techniques that work well together for designing large distributed software systems. Composition is a symmetric operator that allows system components to communicate with each other across module boundaries. Superposition is an asymmetric relationship that allows one system component to observe the state of another. Encapsulation is the ability to define the reason about the behavior of a module in terms of a well-defined boundary between that module and its environment, while hiding the internal operations of that module. In this paper, the I/O automation ...Read More

We present the Spectrum Simulation System, a new research tool for the design and study of distributed algorithms. Based on the formal Input/Output Automation model of Lynch and Tuttle, Spectrum allows one to express distributed algorithms as collections of I/O automata and simulate them directly in terms of the semantics of that model. This permits integration of algorithm specification, design, debugging, analysis, and proof of correctness within a single formal framework that is natural for describing distributed algorithms. Spectrum provides a language for expressing algorithms as I/O automata, a simulator ...Read More

This manuscript is a compilation of lecture notes from the graduate level course CS 582, "Computational Learning Theory," I taught at Washington University in the spring of 1991. Students taking the course were assumed to have background in the design and analysis of algorithms as well as good mathematical background. Given that there is no text available on this subject, the course material was drawn from recent research papers. I selected the first twelve topics and the remainder were selected by the students from a list of provided topics. This ...Read More

In this paper we describe a new technique for exactly identifying certain classes of read-once Boolean formulas. The method is based on sampling the input-output behavior of the target formula on a probability distribution which is determined by the fixed point of the formula's application function (defined as the probability that a 1 is output by the formula when each input bit is 1 independently with probability p). By performing various statistical tests on easily sampled variants of the fixed-point distribution, we are able to efficiently infer all structural information ...Read More

This paper studies the robustness of pac learning algorithms when the instance space is {0,1}n, and the examples are corrupted by purely random noise affecting only the instances (and not the labels). In the past, conflicting results on this subject have been obtained-- the "best agreement" rule can only tolerate small amounts of noise, yet in some cases large amounts of noise can be tolerated. We show the truth lies somewhere between the two alternatives. For uniform attribute noise, in which each attribute is flipped independently at random with the ...Read More

This paper studies self-directed learning, a variant of the on-line learning model in which the learner selects the presentation order for the instances. We give tight bounds on the complexity of self-directed learning for the concept classes of monomials, k-term DNF formulas, and orthogonal rectangles in {0, 1, . . ., n-1}d. These results demonstrate that the number of mistakes under self-directed learning can be surprisingly small. We then prove that the model of self-directed learning is more powerful than all other commonly unused on-line and query learning models. Next ...Read More

This paper presents an analytical model for performance analysis of asynchronous pipelines based on recurrence relations. The model accurately describes the behavior of an asynchronous pipeline, yet yields to very efficient computations. It has been implemented and verified using discrete event simulations. Results of the verification experiments are also described. We also outline a number of ways that the proposed recurrence model can be used to gain insight into many issues concerning engineering of asynchronous pipelines.

The problem of selecting database tuples is central to the task of resolving many forms of queries. The report defines a class of selection queries and presents a set of algorithms for their efficient resolution. The class of queries investigated is those queries which impose a quasi order on the tuples in a database.

Most parser generators are programs that take a context-free grammar specification for a language and generate a parser for that language. Usually, the parsers generated by these parser generators are based on some variations of LL(k) or LR(k) parsing algorithms. The parser generators discussed in this paper creates parsers based on Earlcy's Algorithm. This parser generator creates parsers from any arbitrary context-free grammar specifications; even from ambiguous, cyclic, and unbounded look ahead grammar. These parsers are more powerful than LL(k) and LR(k) parsers and enable the user to create many ...Read More

Radiotherapy treatment optimization is done by generating a set of tentative treatment plans, evaluating them and selecting the plan closest to achieving a set of conflicting treatment objectives. The evaluation of potential plans involves making tradeoffs among competing possible outcomes. Multiattribute decision theory provides a framework for specifying such tradeoffs and using them to select optimal actions. Using these concepts, we have developed a plan-ranking model which ranks a set of tentative treatment plans from best to worst. Heuristics are used to refine this model so that it reflects the ...Read More

An in situ sorting algorithm, based on Quicksort, is presented with its proof of correctness. The proof illustrates a concise and elegant way to represent a sequence that has been partially sorted by Quicksort. A list representation turns out to be well suited to this purpose, and the discussion is entirely in terms of lists.

A derivation of a parallel algorithm for rank order filtering is presented. Both derivation and result differ from earlier designs: the derivations are less complicated and the result allows a number of different implementations. The same derivation is used to design a collection of priority queues. Both filters and priority queues are highly efficient: they have constant response time and small latency.

Asynchronous transfer mode (ATM) networks are capable of supporting a wide variety of applications with varying data rates. FDDI networks offer to support similar applications in the LAN environment. Both these networks are characterized by high data rates, low error rates, and are capable of providing performance guarantees. In this paper we present the design of an ATM-FDDI gateway that can provide high performance internetworking between these two important classes of networks. An important part of the gateway design philosophy is to partition the functionality into critical and non-critical paths. ...Read More

This paper discusses the unfairness issue arising in a 802.6 DQDB network at high loads-- when the traffic demand to a bus exceeds the capacity of that bus. As per the 802.6 protocol, at heavy loads, the end nodes along a bus experience longer delays than the other nodes. The origin and remedy of this heavy load unfairness is discussed. An access control scheme is proposed as a solution. The comparison of the proposed scheme with 802.6 protocol is presented. The simulation results and performance characteristics are discussed under several ...Read More

The DNA restriction mapping problem can be abstracted to the Shortest Common Matching String problem by viewing the restriction fragment lengths as symbols and the clones as bags. The Shortest Common Matching String problem can be decomposed into the Bag Sequencing problem and the Symbol Sequencing problem. All three of these problems have bene shown to be NP-hard. Rhee has proposed a family of greedy algorithms to compute polynomial time approximations to the Bag Sequencing problem, which produced surprisingly good performance results on abstracted data. In the test data generated ...Read More

Asset Allocation has become a dominant factor for investment strategies in recent years. It has found that by holding a strategically diversified portfolio, a high total return on investments can be maintained while, at the same time, reducing portfolio volatility. With recent federal regulations mandating pension investment responsibilities, appropriate asset allocation has become more important than ever. SAAM is a software package specifically designed to be used as a tool to aid the investment professional in determining pension portfolio allocations. SAAM uses the expect system shell CLIPS, has a user-friendly ...Read More

In this paper we present a simulation study of the Ethernet performance under conditions of bursty traffic. This study is motivated by two observations: Ethernet will continue to be a widely used Local Area Network (LAN), especially as an access LAN for future high speed internet (or Broadband ISDN); and future high speed applications can best be modeled as bursty sources. Bursty traffic in this study is specified using three parameters: peak bandwidth, average bandwidth, and burst factor. The simulation study shows that the inherent behavior of the Ethernet does ...Read More

There are several basic approaches that can be used in attempting to produce high-resolution DNA restriction maps. A standard approach is the match/merge approach in which first the topology of the map units being mapped together is suppressed and lists of potential matches between fragments are generated, and second the topology is introduced to eliminate matchlists which are inconsistent with the topology. This technical report documents a different approach to DNA mapping, known as topological mapping. In topological mapping the precedence of the two criteria are reversed, i.e., the topology ...Read More

We give algorithms to convert any network of binary threshold units (that does not oscillate) into an equivalent network with symmetric weight matrix (like Hopfield networks [Hopfield 82] or Boltzmann machines [Hinton, Sejnowski 88]). The motivation for the transformation is dual: a) to demonstrate the expressive power of symmetric networks; i.e. binary threshold networks (that do not oscillate) are subsumed in the energy minimization paradigm; 2) to use network modules (developed for the spreading activation paradigm for example), within the energy minimization paradigm. Thus optimization [Tank, Hopfield 88] and approximation ...Read More

This paper considers the problem of expressing predicate calculus in connectionist networks that are based on energy minimization. Given a first-order-logic knowledge base and a bound k, a symmetric network is constructed (like a Boltzman machine or a Hopfield network) that searches for a proof fora given query. If a resolution-based proof is length no longer k exists, then the global minima of the energy function that is associated with the network represent such proofs. If no proof exist then the global minima indicate the lack of a proof. The ...Read More

We define a notion of reasoning using world-rank-functions, independently of any symbolic language. We then show that every symmetric neural network (like Hopfield networks or Boltzman machines) can be seen as performing a search for a satisfying model of some knowledge that is wired into the network's topology and weights. Several equivalent languages are then shown to describe symbolically the knowledge embedded in these networks. We extend propositional calculus by augmenting assumptions with penalties. The extended calculus (called "penalty logic") is useful in expressing default knowledge, preference between arguments, and ...Read More

The goal of this article is to construct a connectionist inference engine that is capable of representing and learning nonmotonic knowledge. An extended version of propositional calculus is developed and is demonstrated to be useful for nonmonotonic reasoning and for coping with inconsistency that may be a result of noisy, unreliable sources of knowledge. Formulas of the extended calculus (called penalty logic) are proved to be equivalent in a very strong sense to symmetric networks (like Hopfield networks and Boltzmann machines), and efficient algorithms are given for translating back and ...Read More

Connectionist networks with symmetric weights (like Hopfield networks and Boltman Machines) use gradient descent to find a minimum for quadratic energy functions. We show an equivalence between the problem of satisfiability in propositional calculus and the problem of minimizing those energy functions. The equivalence is in the sense that for an satisfiable Well Formed Formula (WFF) we can find a quadratic function that describes it, such that the set of solutions that minimize the function is equal to the set of truth assignments that satisfy the WFF. We also show ...Read More

A consequence relation (CR) relates sets of beliefs to the appropriate conclusions that might be deduced. Of special interest to Artificial Intelligence are CRs that cope with inconsistency within the set of beliefs. Default reasoning, belief revision, social choice and reasoning from conflicting knowledge sources are just a few examples of mechanisms that need to handle inconsistency, In this paper we show a taxonomy in which many existing mechanisms are mapped, and new interesting ones are revealed. We identify simple relations among the CRs and give a language for their ...Read More

This paper describes the conceptual model, specification method, and visualization methodology for Pavane-- a visualization environment concerned with exploring, monitoring, and presenting concurrent computations. The underlying visualization model is declarative in the sense that visualization is treated as a mapping from program states to a three-dimensional world of geometric objects. The latter is rendered in full color and may be examined freely by a viewer who is allowed to navigate through the geometric world. The state-to-geometry mapping is defined as a composition of several simpler mappings. The choice is determined ...Read More

Swarm is a computational model which extends the UNITY model in three important ways: (1) UNITY's fixed set of variables is replaced by an unbounded set of tuples which are addressed by content rather than by name; (2) UNITY's static set of statements is replaced by a dynamic set of transactions; and (3) UNITY's state II-composition is augmented by dynamic coupling of transactions into synchronic groups. This last feature, unique to Swarm, facilitates formal specification of the mode of execution (synchronous or asynchronous) associated with portions of a concurrent program ...Read More

This paper describes a formal approach to developing concurrent rule-based programs. Our program derivation strategy starts with a formal specification of the problem. Specification refinement is used to generate an initial version of the program. Program refinement is then applied to produce a highly concurrent and efficient version of the same program. Techniques for the deriving concurrent programs through either specification or program refinement have been described in previous literature. The main contribution of this paper consists of extending the applicability of these techniques to a broad class of rule-based ...Read More

Reliability, defined as the guarantee that a program satisfies its specifications, is an important aspect of many applications for which rule-based expert systems are suited. Executing rule-based programs on a series of test cases. To show a program is reliable, it is desirable to construct formal specifications for the program and to prove that it obeys those specifications. This paper presents an assertional approach to the verification of a class of rule-based programs characterized by the absence of conflict resolution. The proof logic needed for verification is already in use ...Read More

The arguments against centralized solutions focus on the performance bottleneck associated with a single central uniprocessor having a limited throughput and, possibly, a small number of ports. These limitations can be overcome to some extent if the central processor is replaced by a modern SIMD (Single Instruction Multiple Data) machine. Several orders of magnitude gains in parallelism are thus achievable while maintaining the logical simplicity of a centralized control. We call such a scheme parallel synchronous control (PSC). In this paper, we explore this approach by presenting a PSC solution ...Read More