Follow


Research from 1992

PDF

Improved Queueing Analysis of Shared Buffer Switching Networks
Giuseppe Bianchi and Jonathan S. Turner
Technical Report

Abstract:

This paper describes several methods for analyzing the queueing behavior of switching networks with flow control and shared buffer switches. It compares the various methods on the basis of accuracy and computation speed, where the performance metric of the most concern is the maximum throughput. The best of the methods accurately predicts throughput for multi-stage networks constructed from large switches (greater than equal to 8 ports).

... Read More

PDF

Exact and Approximate Solution of a Multiplexing Problem
Mario Bonatti, Andreas Bovopoulos, Apostolos Dailianas, and Alexei Gaivoronski
Technical Report

Abstract:

In this paper the detailed solution of the multiplexing problem of independent but not necessarily homogenous traffic sources is presented. The "curse of dimensionality" of problems of realistic dimensions is comprehensively addressed by a methodology employing state aggregation. A number of detailed examples provide further insight into the multiplexing problems and their exact and approximate solutions.

... Read More

PDF

Optimal Burst Level Admission Control In A Broadband Network
Andreas D. Bovopoulos
Technical Report

Abstract:

In a broadband ATM network the traffic of a virtual circuit is defined at the cell, burst and call levels. All virtual circuits sharing the resources of a switch are statistically multiplexed at the cell level. In this paper the issue of how to control the admission of bursts of a particular virtual circuit is analyzed. It is demonstrated that under two optimization criteria, the optimal burst level admission control of a virtual circuit is a window control. This result suggests that while the cells of all virtual circuits sharing... Read More

PDF

Statistical Multiplexing of Semi-Markov Modulated Sources
Andreas D. Bovopoulos and Saied Hosseini-Khayat
Technical Report

Abstract:

It is shown that when a continuous buffer is driven by a semi-Markox modulated fluid flow source(s), the stationary distribution of the buffer content is governed by the same differential equation describing the distribution for continuous time Markov modulated fluid source(s) [1]. It is also shown that the same techniques can be utilized to decompose and solve the eigenvalue problem associated with the differential equation [6]. Finally it is shown that the stationary distribution of buffer content depends only on the mean time spent by each multiplexed semi-Markov source in... Read More

PDF

The Effect of Delayed Feedback Information on Network Performance
Andreas D. Bovopoulos and Aurel A. Lazar
Technical Report

Abstract:

The performance of a network subject to either state dependent or state independent flow control is investigated. In the state dependent case, the flow control policy is a function of the total number of packets for which the controller has not yet received an acknowledgement. In this case it is shown that the optimal flow control is a sliding window mechanism. The effect of the delayed feedback on the network performance as well as the size of the window are studied. The state independent optimal rate is also derived. The... Read More

PDF

Simulation of an ATM-FDDI Gateway
Milind M. Buddhikot, Sanjay Kapoor, and Gurudatta M. Parulkar
Technical Report

Abstract:

Asynchronous transfer mode (ATM) networks can support a wide variety of applications with varying data rates. Fiber Distributed Data Interface (FDDI) networks are targeted to support similar applications, but only in a LAN environment. Both of these networks are characterized by high data rates and low error rates. In addition, they can provide applications with varying degrees of performance guarantees. A problem of designing a high-performance gateway architecture for internetworking between these two important classes of networks was addressed in [Kapoor, 1991b]. An important part of the gateway design philosophy... Read More

PDF

Inversion Laws for Specifications and Recursive Procedures
Wei Chen
Technical Report

Abstract:

In this paper, we continue the work on the formal approach to program inversion by presenting programming laws for specifying the inverse program according to the specification of its forward program, and for inverting recursive procedues. The formal establishment of these laws, once more, convinces us that program inversion has nice mathematical properties that can be used in formal program development. Some examples are included to illustrate the usage of the laws developed in this paper.

... Read More

PDF

Project Zeus: Design of a Broadband Network and its Application on a University Campus
Jerome R. Cox Jr., Michael E. Gaddis, and Jonathan S. Turner
Technical Report

Abstract:

This is a report of the results of the initial step in a plan for the design, deployment and operation of a high speed campus network at Washington University. The network is based on ATM switching technology that has been developed here during the last several years. This network will support ubiquitous multimedia workstations with high-resolution graphics and video capabilities, open up 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... Read More

PDF

CtoVis: An Interface between C Programs and Pavane Visualizations
Kenneth C. Cox
Technical Report

PDF

Abstraction in Algorithm Animation
Kenneth C. Cox and Gruia-Catalin Roman
Technical Report

Abstract:

Abstraction of information into visual form plays a key role in the development of algorithm animations. We present a classification for abstraction as applied to algorithm animation. The classification emphasizes the expressive power of the abstraction, ranging from simple direct presentation of the program's state to complex animations intended to explain the behavior of the program. We illustrate our classification by presenting several visualizations of a shortest path algorithm.

... Read More

PDF

Experiences with the Pavane Program Visualization Environment
Kenneth C. Cox and Gruia-Catalin Roman
Technical Report

Abstract:

The Pavane system is an implementation of the declarative visualization model, which treats visualization as a mapping form the state of some entity (a program, an execution, a data set, etc.) to images. We briefly discuss the declarative visualization model and the implementation of Pavane. We then present some of the results that we have obtained with Pavane. These results are divided into three parts: a discussion of the development of visualizations focusing on the roles played by the various participants, a critique of declarative visualization in general and Pavane... Read More

PDF

An Implementation Model for Connection-Oriented Internet Protocols
Charles D. Cranor and Gurudatta M. Parulkar
Technical Report

Abstract:

Recently a number of research groups have proposed connection-oriented access protocols that can provide a variable grade of service with performance guarantees on top of diverse networks. These connection-oriented internet protocols (COIPs) have different performance trade-offs. The purpose of this paper is to create a COIP-Kernel which can be used as a toolkit to implement any of the proposed COIPs. COIP-K features module interchanges and incremental software support. The paper presents the COIP-K implementation and its performance characterization.

... Read More

PDF

Formal Specifications and Design of a Message Router
Christian Creveull and Gruia-Catalin Roman
Technical Report

Abstract:

Formal derivation refers to a family of design techniques that entail the development of programs which are guaranteed to be correct by construction. This paper investigates the possible application of one such technique-- UNITY-style specification refinement-- to industrial-grade problems. The formal specification and design of a message router illustrates the derivation process and helps identify those methodological elements that are likely to contribute to successful use of this technique in industrial environment. Although, the message router cannot be characterized as being industrial-grade, it is a sophisticated problem that pose significant... Read More

PDF

Efficient Accommodation of May-Alias Information in SSA Form
Ron Cytron and Reid Gershbein
Technical Report

Abstract:

We present an algorithm for incrementally including may-alias information into Static Single Assignment form by computing a sequence of increasingly precise (and correspondingly larger) partial SSA forms. Our experiments show significant speedup of our method over exhaustive use of may-alias information, as optimization problems converge well before most may-aliases are needed.

... Read More

PDF

Connection Management Access Protocol (CMAP) Specification
John DeHart, Mike Gaddis, and Rick Bubenik
Technical Report

Abstract:

This document specifies a Connection Management Access Protocol (CMAP) for managing multipoint connectinos in high-speed packet switched networks. We target CMAP to networks employing the Asynchronous Transfer Mode (ATM) communication standard. We define a multipoint connection as a communication channel between two or more clients of the network, where all data sent by one client is received by all other clients who have elected to receive. A point-to-point connection is a special case of a multipoint connection involving only two clients. CMAP specifies the access procedures exercised by clients to... Read More

PDF

Algorithms for Designing Nonblockings Communication Networks with General Topologies
J. Andrew Fingerhut
Technical Report

Abstract:

A framework is given for specifying nonblocking traffic requirements in a connection-oriented communications network. In this framework, connections may be form one point to one other point, or they may involve multiple points. Different connections may have different data rates. The communication networks are constructed from switches (or nodes) and trunks, which connect pairs of switches. This framework is intended to model Asynchronous Transfer Mode (ATM) networks and traffic. Several computational problems are formulated, each intended to find a minimum cost configuration of switches and trunks which satisfy given traffic... Read More

PDF

Designing Communication Networks with Fixed or Nonblocking Traffic Requirements
J. Andrew Fingerhut
Technical Report

Abstract:

A general framework for specifying communication network design problems is given. We analyze the computational complexity of several specific problems within this framework. For fixed multirate traffic requirements, we prove that a particular network analysis problem is NP-complete, although several related network design problems are either efficiently solvable or have good approximation algorithms. For the case when we wish the network to operate without blocking any connection requests, we give efficient algorithms for dimensioning the link capacities of the network.

... Read More

PDF

Performance Comparison of Clocked and Asynchronous Pipelines
Mark A. Franklin and Tienyo Pan
Technical Report

Abstract:

Clock (synchronous) and self-timed (asynchronous) represent the two principal methodologies associated with timing control and synchronization of digital systems. In this paper, clocked and the asynchronous instruction and arithmetic pipelines are modeled and compared. The approach, which yields the best performance is dependent on technology parameters, operating range and pipeline algorithm characteristics. Design curves are presented which permit selection of the best approach for a given application and technology environment.

... Read More

PDF

Energy-related Feature Abstraction for Handwritten Digit Recognition
Thomas H. Fuller Jr.
Technical Report

Abstract:

Most handwritten character recognizers use either graphical (static) or first-order dynamic data. Our research speculates that the mental signal to write a digit might be partially encoded as an energy profile. We used artificial neural networks (ANN) to analyze energy-related features (first and second time derivatives) of handwritten digits of 20 subjects and later 40 subjects. An experimenal environment was developed on a NeXTstation with a real-time link to a pen-based GO computer. Although such an experiment cannot confirm an energy profile encoded in the writer, it did indicate the... Read More

PDF

DNA Mapping Algorithms: Strategies for Single Restriction Enzyme and Multiple Restriction Enzyme Mapping
Will Gillett
Technical Report

Abstract:

An approach to high-resolution restriction-fragment DNA mapping, known as Multiple-Restriction-Enzyme mapping (MRE mapping), is present. This approach significantly reduces the uncertainty of clone placement by using clone ends to synchronize the position in of clones within different maps, each map being constructed from fragment-length data produced by digestion of each clone with a specific restriction enzyme. Maps containing both fragments-length data and clone-end data are maintained for each restriction enzyme, and synchronization between two such maps is achieved by requiring them to have "compatible" clone-end map projections. Basic definitions of... Read More

PDF

Separating Structure from Function in the Specification and Design of Distributed Systems
Kenneth J. Goldman
Technical Report

Abstract:

A distributed system is viewed as a collection of functional components and a unifying structure that defines relationships among the components. In the paper, we advocate a particular approach to distributed system specification and design in which the structure of a distributed system is specified separately from the functional components. This permits one to reason about individual functional components in isolation, and encourages one to make explicit not only the input/output behavior of the functional components but also the logical placement of these components within the overall structure of the... Read More

PDF

The Programmers' Playground: I/O Abstraction for Heterogeneous Distributed Systems
Kenneth J. Goldman and Michael D. Anderson
Technical Report

Abstract:

A new high-level approach to interprocess communication in heterogeneous distributed systems in introduced, This approach, called I/O Abstraction, allows one to write each functional component of a distributed system as an encapsulated program that acts upon a set of local data structures, some of which may be published for external use. The functional components are separately configured by establishing logical connections among the published data structures. In order to illustrate this approach, we describe the The Programmers' Playground, a high-level language "veneer" and protocol designed to support I/O abstraction in... Read More

PDF

On the Complexity of Teaching
Sally A. Goldman and Michael J. Kearns
Technical Report

Abstract:

While most theoretical work in machine learning has focused on the complexity of learning, recently there has been increasing interest in formally studying the complexity of teaching. In this paper we study the complexity of teaching by considering a variant of the on-line learning model in which a helpful teacher selects the instances. We measure the complexity of teaching a concept from a given concept class by a combinatorial measure we call the teaching dimension. Informally, the teaching dimension of a concept class is the minimum number of instances a... Read More

PDF

On the Sample Complexity of Weakly Learning
Sally A. Goldman, Michael J. Kearns, and Robert E. Schapire
Technical Report

Abstract:

In this paper, we study the sample complexity of weak learning. That is, we ask how much data must be collected from an unknown distribution in order to extract a small but significant advantage in prediction. We show that it is important to distinguish between those learning algorithms that output deterministic hypotheses and those that output randomized hypotheses. We prove that in the weak learning model, any algorithm using deterministic hypotheses to weakly learn a class of Vapnik-Chervonenkis dimension d(n) requires (omega) (square root of d(n) examples.

... Read More

PDF

Learning k-term DNF Formulas with an Incomplete Oracle
Sally A. Goldman and H. David Mathais
Technical Report

Abstract:

We consider the problem of learning k-term DNF formulas using equivalence queries and incomplete membership queries as defined by Angluin and Slonim. We demonstrate the this model can be applied to non-monotone classes. Namely, we describe a polynomial algorithm that exactly identifies a k-term DNF formula with a k-term DNF hypothesis using incomplete membership queries and equivalence queries from the class of DNF formulas.

... Read More

PDF

Can PAC Learning Algorithms Tolerate Random Attribute Noise?
Sally A. Goldman and Robert H. Sloane
Technical Report

Abstract:

This paper studies the robustness of pac learning algorithms when the instances 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 that the truth lies somewhere in between these two alternatives. For uniform attribute noise, in which each attribute is flipped independently at... Read More

PDF

The Power of Self-Directed Learning
Sally A. Goldman and Robert H. Sloan
Technical Report

Abstract:

This paper studies self-directed learning, a variant of the on-line (or incremental) learning model in which the learner selects the presentation order for the instances. Alternatively, one can view this model as a variation of learning with membership queries in which the learner is only "charged" for membership queries for which it could not predict the outcome. We give tight bounds on the complexity of self-directed learning for the concept classes of monomials, monotone DNF formulas, and axis-parallel rectangles in {0,1 ' ' ', n-1}d. These results demonstrate that the... Read More

PDF

An Application-Oriented Error Control Scheme for High Speed Networks
Fengmin Gong and Guru Parulkar
Technical Report

Abstract:

Many new network applications demand interprocess communication (IPC) services that are not supported by existing transport network protocol mechanisms. Large bandwidth-delay products of high-speed networks also render the existing error control mechanism inefficient. This paper presents the design, evaluation, and implementations of an application-oriented error control scheme that can support efficient IPC for these applications in high-speed network environments.

... Read More

PDF

A Two-Level Flow Control Scheme for High Speed Networks
Fengmin Gong and Guru Parulkar
Technical Report

Abstract:

Many new network applications demand interprocess communication (IPC) services with guaranteed bandwidth, delay, and low. Existing transport protocol mechanisms have not been designed with these service objectives. Large bandwidth-delay products of high-speed networks also render the existing flow control mechanism inefficient. This paper presents the design, evaluation, and implementation of a two-level flow control scheme that can support efficient IPC for these applications in high-speed network environments.

... Read More

PDF

An Overview of Segment Streaming for Efficient Pipelined Televisualization
Fengmin Gong and Gurudatta M. Parulkar
Technical Report

Abstract:

The importance of scientific visualization for both science and engineering endeavors has been well recognized. Televisualization becomes necessary because of the physical distribution of data, computation resources, and users invovled in the visualization process. However, televisualization is not adequately supported by existing communication protocols. We believe that a pielined televisualization model (PTV) is suitable for efficient implementation of most visualization applications. In order to support this model over high speed networks, we are developing a segment streaming interprocess communication (IPC) mechanism within the Axon communication architecture. Important aspects of this... Read More

PDF

Design of a Multimedia Applications Development System
Raman Gopalakrishnan and Andreas D. Bovopoulos
Technical Report

Abstract:

The application envisaged for high speed packet switched networks have diverse and demanding transport requirements that are not satisfied by current communications software implementations. In addition, existing communication interfaces for distributed programs are not general enough to express the communication patterns and control required for distributed applications. This Multimedia Applications Development (MAD) system is designed to address these problems mentioned above. It is intended as a platform for implementing and experimenting with protocols and their implementation, network service access methods, and communication primitives for constructing distributed multimedia applications. It is... Read More

PDF

Exact Dominance without Search in Decision Trees
Nilesh L. Jain and Ronald P. Loui
Technical Report

Abstract:

In order to improve understanding of how planning and decision analysis relate, we propose a hybrid model containing concepts from both. This model is comparable to [Hartman90], with slightly more detail. Dominance is simple concept in decision theory. In a restricted version of our model, we give conditions under which dominance can be detected without search: that is, it can be used as a pruning strategy to avoid growing large trees. This investigation follows the lead of [Wellman87]. The conditions seem hard to meet, but may nevertheless be useful in... Read More

PDF

Hyperflow: A Uniform Visual Language for Different Levels of Programming
Takayuki Dan Kimura
Technical Report

Abstract:

We propose a visual language, Hyperflow, for system programming as well as for end user shell programming. Hyperflow is designed for a multimedia pen computer system for children. It is a dataflow-based graphical language similar to Show and Tell. In order to demonstrate the capability of Hyperflow, we solve the programming problem of implementing a help command for children to telephone their instructor or parents using voice communication hardware (modem, microphone, speaker, and a clock). The resulting program includes visual programs to implement device drivers for the modem and clock... Read More

PDF

Hyperflow: A Visual Programming Language for Pen Computers
Takayuki Dan Kimura
Technical Report

Abstract:

This paper presents the design philosophy of the Hyperflow visual programming language. It also gives an overview of its semantic model. The primary purpose of language is to provide a user interface for a pen-based multimedia computer system designed for school children. Yet it is versatile enough to be used as a system programming language. The concept of visually interactive process, vip in short, is introduced as the fundamental element of the semantics. Vips communicate with each other through exchange of signals, either discrete or continuous. Each vip communicates with... Read More

PDF

Kumon Machine: Learning Math with Silicon Paper
Takayuki Dan Kimura
Technical Report

PDF

A Protocol for Dynamic Assessment of Network Topology in DQDB MANs
Lakshmana N. Kumar and Andreas D. Bovopoulos
Technical Report

Abstract:

The 802.6 protocol of DQDB MANs aims to maintain a distributed queue for network access and yet inherits access unfairness. In this paper, the DANT protocol is proposed to provide head-end nodes as well as each active node in a DQDB network with real time information about the active node population, the intermodal distance, the position of each node along what bus and the length of a node's downstream bus segment. DANT's current implementation introduces an overhead of 5 bits per slot but alternative implementations which retain the current slot... Read More

PDF

The 3-Tier Structured Access Protocol to Control Unfairness in DQDB MANs
Lakshmana N. Kumar and Andreas D. Bovopoulos
Technical Report

Abstract:

This paper addresses the unfairness problem appearing in 802.6-based DQDB MANs. Traffic load demand is characterized as low (below 0.4 of the channel capacity), normal (from 0.4 to 0.9 of the channel capacity) or heavy (greater than 0.9 of the channel capacity). At low loads the 802.6 protocol is acceptably fair. At normal loads, however, the protocol performance is markedly unfair. The unfairness is related to the latency in transporting a request. At heavy loads the unfairness is both latency-related and flooding-related. In this paper, both types of unfairness are... Read More

PDF

An Argument Game
Ronald Loui and William Chen
Technical Report

Abstract:

This game was designed to investigate protocols and strategies for resource-bounded disputation. The rules presented here correspond very closely to the problem of controlling search in an actual program.

PDF

Computing Specificity
Ronald Loui, J. Norman, K. Stiefvater, A. Merrill, A. Costello, and J. Olson
Technical Report

Abstract:

This note reports on an effort to implement a version of Poole's rule for specificity. Relatively, efficient implementation relies on correcting and improving a pruning lemma of Simari-Loui [92]. This in turn requires revision of Poole's specificity concept. The resulting system is a usable knowledge representation system with first-order-language and defeasible reasoning. Sample input and output are included in an appendix. It is a good candidate for multiple inheritance applications; it is useful for planning, but limited by the underlying search for plans.

... Read More

PDF

Process and Policy: Resource-Bounded Non-Demonstrative Reasoning
Ronald P. Loui
Technical Report

Abstract:

This paper investigates the appropriateness of formal dialectics as a basis for non-monotonic and defeasible reasoning that takes computational limits seriously. Rules that can come into conflict should be regarded as policies, which are inputs to deliberative processes. Dialectical protocols are appropriate for such deliberations when resources are bounded and search is serial. AI, it is claimed here, is now perfectly positioned to correct many misconceptions about reasoning that have resulted from mathematical logic's enormous success in this century: among them (1) that all reasons are demonstrative, (2) that rational... Read More

PDF

A Model for Detecting Motifs in Biological Sequences
Andrew F. Neuwald and Phillip P. Green
Technical Report

Abstract:

A method for detecting patterns in biological sequences is described that incorporates rigorous statistics for determining significances, and an algebraic system that, in combination with a depth first search procedure, can be used to efficiently search for all patterns up to a specified length. This method includes a context free command language grammar and is formulated using a mathematical model amendable to additions enhancements, The method was implemented and verified by detection of various types of patterns in protein sequences.

... Read More

PDF

Experimental Evaluation of SUNOS IPC and TCP/IP Protocol Implementations
Christos Papadopoulos and Gurudatta M. Parulkar
Technical Report

Abstract:

Progress in the field of high speed networking and distributed applications has led to the debate in the research community on suitability of existing protocols such as TCP/IP for emerging applications over high speed networks. Protocols have to operate in a complex environment comprising of various operating systems, host architectures, and a rapidly growing and evolving internet of large number of heterogeneous subnetworks. Thus, evaluation of protocols is definitely a challenging task and cannot be achieved by studying protocols in isolation. This paper presents results of a research project that... Read More

PDF

An Improved Activation Function for Energy Minimization
Gadi Pinkas and Rina Dechter
Technical Report

Abstract:

Symmetric networks that are based on energy minimization, such as Boltzmann machines or Hopfield nets, are used extensively for optimization, constraint satisfaction, and approximation of NP-hard problems. Nevertheless, finding a global minimum for the energy function is not guaranteed, and even a local minimum may take an exponential number of steps. We propose and improvement to the standard activation function used for such networks. The improved algorithm guarantees that a global minimum is found in linear time for tree-like subnetworks. The algorithm is uniform and does not assume that the... Read More

PDF

Pavane User's Manual
Jerome Y. Plun
Technical Report

Abstract:

This report describes the Pavane visualization system. Pavane is set to a set of tools allowing on to 1) simulate the execution of a computation specified with the Swarm model and 2) visualize the state of the computation by mean of a set of rules. Pavane also provides the means to visualize other computations. This manual describes how to initiate a Pavane session to visualize a Swarm computation as well as the role of each of the component of such as session.

... Read More

PDF

Swarm Language Reference Manual
Jerome Y. Plun, C. Donald Wilcox, and Kenneth C. Cox
Technical Report

Abstract:

This document contains a description of the grammar and syntax rules of the Swarm programming language. This language, which is an implementation of the program specification language used with the Swarm computational model, is used both to specify programs and their visualizations, for the use of the Pavane program visualization system.

PDF

Program Visualization: The Art of Mapping Programs to Pictures
Gruia-Catalin Roman and Kenneth C. Cox
Technical Report

Abstract:

In this paper program visualization is defined as a mapping from programs to graphical representations. Simple forms of program visualization are frequently encountered in software engineering. For this reason current advances in program visualization are likely to influence future developments concerning software engineering tools and environments. This paper provides a new taxonomy of program visualization research. The proposed taxonomy becomes the vehicle through which we carry out a systematic review of current systems, techniques, trends, and ideas in program visualization.

... Read More

PDF

Seeking Concurrency in Rule-based Programming
Gruia-Catalin Roman, Rose F. Gamble, and William E. Ball
Technical Report

Abstract:

This paper describes a formal approach for developing concurrent rule-based programs. Specification of 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 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 programs. To the best of our knowledge, this is the first time... Read More

PDF

Architecture-Directed Refinement
Gruia-Catalin Roman and C. Donald Wilcox
Technical Report

Abstract:

As critical computer systems continue to grow in complexity, the task of demonstrating that they are correct, that is, guaranteed to operate without failure, becomes more difficult. For this reason, research in software engineering has turned to formal methods, i.e. rigorous approaches to demonstrating the correctness of software systems. Unfortunately, the formal methods currently used for concurrent systems do no provide a mechanism for expressing and manipulating non-functional constraints formally. In this paper, we show that one class of non-functional constraints, the target architectures, can be expressed using formal notation... Read More

PDF

On Deriving Distributed Programs from Formal Specifications of Functional Requirements and Architectural Constraints
Gruia-Catalin Roman, C. Donald Wilcox, and Jerome Y. Plum
Technical Report

Abstract:

This design of distributed programs is a difficult task which can greatly benefit from the application of formal methods. Since design solutions are determined not only by functional requirements imposed by the application but also by the structure and behavior of the underlying hardware architecture, a complete formal treatment of the program derivation process becomes a significant challenge. The common approach is to state with a formal specification of the functional requirements and to derive the desired program through systematic refinements which factor in the architectural constraints informally, in an... Read More

PDF

Hardware Based Error and Flow Control in the Axon Gigabit Host-Network Interface
James P. G. Sterbenz, Anshul Kantawala, Milind Buddhikot, and Gurudatta M. Parulkar
Technical Report

Abstract:

We have proposed a new architecture called Axon that meets the challenges of delivering high performance network bandwidth directly to applications. Its pipelines network interface must perform critical per packet processing in hardware a packets flow through the pipeline, without imposing any store-and-forward buffering of packets. This requires the design of error and flow control mechanisms to be simple enough for implementation in the network interface hardware, while providing functionality required by applications. This paper describes the implementation of the Axon host-network interface, and in particular the hardware design of... Read More

PDF

Hierarchical Correctness Proofs for Recursive Distributed Algorithms using Dynamic Process Creation
Bala Swaminathan and Kenneth J. Goldman
Technical Report

Abstract:

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

PDF

Gesture System for a Graph Editor
Burak Muammer Taysi
Technical Report

Abstract:

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.

... Read More

PDF

Research Proposal: Design and Analysis of Practical Switching Networks
Ellen E. White
Technical Report

Abstract:

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

PDF

The Clos Network as a Multirate Distributer with a Greedy Routing Algorithm
Ellen E. White
Technical Report

Abstract:

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

PDF

Multicomputer Checkpointing
Ken Wong and Mark Franklin
Technical Report

Abstract:

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

Research from 1991

PDF

Persistent Connections in High Speed Internets
James M. Anderson, Gurudatta M. Parulkar, and Zubin Dittia
Technical Report

Abstract:

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

PDF

Completely Reliable Auto Shopping Heuristic (CRASH)
Todd Bashuk, David Donat, and Kieth Marrs
Technical Report

Abstract:

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.

... Read More

PDF

Performance Evaluation of a Traffic Control Mechanism for ATM Networks
Andreas D. Bovopoulos
Technical Report

Abstract:

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

PDF

Exit Statements are Executable Miracles
Wei Chen
Technical Report

Abstract:

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

PDF

CABeN: A Collection of Algorithms for Belief Networks
Steve B. Cousins, William Chen, and Mark E. Frisse
Technical Report

Abstract:

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

PDF

The Visual Display of Temporal Information
Steve B. Cousins and Michael G. Kahn
Technical Report

Abstract:

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

PDF

Rapid Display of Radiographic Images
Jerome R. Cox Jr., Stephen M. Moore, Robert A. Whitman, G. James Blaine, R. Gilbert Jost, L. Magnus Karlsson, Thomas L. Monsees, Gregory L. Hansen, and Timothy C. David
Technical Report

Abstract:

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

PDF

Project Zeus: Design of a Broadband Network and its Application on a University Campus
Jerome R. Cox Jr. and Jonathan S. Turner
Technical Report

Abstract:

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

PDF

SwarmView: A Graphical Engine for the Interpretation and Display of Visualizations
Kenneth C. Cox
Technical Report

Abstract:

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.

... Read More

PDF

DNA Mapping Algorithms: Fragment Splitting and Combining
James Daues and Will Gillet
Technical Report

Abstract:

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

PDF

The Discrete Orthonormal Wavelet Transform: An Introduction
Michael Frazier and Arun Kumar
Technical Report

Abstract:

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

PDF

The Kumon Approach to Learning Mathematics: An Educator's Perspective
Thomas H. Fuller Jr.
Technical Report

Abstract:

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

PDF

Transforming a Rule-based Program
Rose F. Gamble
Technical Report

Abstract:

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

PDF

Applying Formal Verification Methods to Pure Rule-Based Programs
Rose F. Gamble, Gruia-Catalin Roman, William E. Ball, and H. Conrad Cunningham
Technical Report

Abstract:

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

PDF

DNA Mapping Algorithms: Abstract Data Types - Concepts and Implementation
Will Gillett and Liz Hanks
Technical Report

Abstract:

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

PDF

Composition, Superposition, and Encapsulation in the Formal Specification of Distributed Systems
Kenneth J. Goldman
Technical Report

Abstract:

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

PDF

The Spectrum Simulation System: A Formal Approach to Distributed Algorithm Development Tools
Kenneth J. Goldman
Technical Report

Abstract:

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

PDF

Computational Learning Theory Lecture Notes for CS 582 Spring Semester, 1991
Sally A. Goldman
Technical Report

Abstract:

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

PDF

Exact Identification of Read-once Formulas Using Fixed Points of Amplification Functions
Sally A. Goldman, Michael J. Kearns, and Robert E. Schapire
Technical Report

Abstract:

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

PDF

The Difficulty of Random Attribute Noise
Sally A. Goldman and Robert H. Sloan
Technical Report

Abstract:

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

PDF

The Power of Self-Directed Learning
Sally A. Goldman and Robert H. Sloan
Technical Report

Abstract:

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

PDF

A Recurrence Model for Asynchronous Pipeline Analysis
Fengmin Gong, Zubin Dittia, and Gurudatta M. Parulkar
Technical Report

Abstract:

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.

... Read More

PDF

Efficient Queries For Quasi-Ordered Databases
Victor Jon Griswold
Technical Report

Abstract:

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.

PDF

A Parser Generator Based on Earley's Algorithm
Jawaid Hakim
Technical Report

Abstract:

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

PDF

Ranking Radiotherapy Treatment Plans using Decision-Analytic and Heuristic Techniques
Nilesh L. Jain and Michael G. Kahn
Technical Report

Abstract:

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

PDF

Quicksort in Constant Space
Anne Kaldewaij and Jan Tijmen Udding
Technical Report

Abstract:

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.

PDF

Rank Order Filters and Priority Queues
Anne Kaldewaij and Jan Tijmen Udding
Technical Report

Abstract:

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.

... Read More

PDF

Design of an ATM-FDDI Gateway
Sanjay Kapoor and Gurudatta M. Parulkar
Technical Report

Abstract:

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

PDF

An Access Protection Solution for Heavy Load Unfairness in DQDB
Lakshmana N. Kumar and Andreas D. Bovopoulos
Technical Report

Abstract:

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

PDF

DNA Mapping Algorithms: Clone Sequencing
Judith H. Lewis and Will Gillett
Technical Report

Abstract:

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

PDF

SAAM: The Strategic Asset Allocation Model
Judy Lewis, Todd Gamble, and John Tai
Technical Report

Abstract:

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

PDF

Performance Analysis of the Ethernet under Conditions of Bursty Traffic
Tony Y. Mazraani and Gurudatta M. Parulkar
Technical Report

Abstract:

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

PDF

DNA Mapping Algorithms: Topological Mapping
Kenneth Moorman, Paul Poulosky, and Will Gillett
Technical Report

Abstract:

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

PDF

Remote Visualization: Challenges and Opportunities Panel Statement
Gurudatta M. Parulkar
Technical Report

PDF

Converting Binary Thresholds Networks into Equivalent Symmetric Networks
Gadi Pinkas
Technical Report

Abstract:

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

PDF

First-Order Logic Proofs using Connectionist Constraints Relaxation
Gadi Pinkas
Technical Report

Abstract:

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

PDF

Propositional Non-Monotonic Reasoning and Inconsistency in Symmetric Neural Networks
Gadi Pinkas
Technical Report

Abstract:

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

PDF

Representation and Learning of Propositional Knowledge in Symmetric Connectionist Networks
Gadi Pinkas
Technical Report

Abstract:

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

PDF

Symmetric Neural Nets and Propositional Logic Satisfiability
Gadi Pinkas
Technical Report

Abstract:

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

PDF

Reasoning for Inconsistency-- A Taxonomy and a Connectionist Approach
Gadi Pinkas and Ron P. Loui
Technical Report

Abstract:

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

PDF

Pavane: A System for Declarative Visualization of Concurrent Computations
Gruia-Catalin Roman, Kenneth C. Cox, C. Donald Wilcox, and Jerome Y. Plum
Technical Report

Abstract:

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

PDF

Reasoning about Synchronic Groups
Gruia-Catalin Roman and H. Conrad Cunningham
Technical Report

Abstract:

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

PDF

Formal Derivation of Rule-Based Program
Gruia-Catalin Roman, Rose F. Gamble, and William E. Ball
Technical Report

Abstract:

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

PDF

Formal Verification of Pure Production Systems Programs
Gruia-Catalin Roman, Rose F. Gamble, and William E. Ball
Technical Report

Abstract:

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

PDF

Parallel Synchronous Control
Gruia-Catalin Roman and Jerome Y. Plum
Technical Report

Abstract:

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