 |
2004
. 2003
. 2002 . 2001
. 2000
. 1999
. 1998
. 1997
. 1996
. 1995
. 1994
. 1993
. 1992
. 1991
. 1990
MS-CIS-03-01
Modular Strategies
for Recursive Game Graphs
Authors: Rajeev Alur,
Salvatore La Torre, P. Madhusudan
MS-CIS-03-02
Li Tan, Oleg Sokolsky, and Insup Lee
Testing has been used in practice to check the conformation of an
implementation to a specification. Recently, there has been much
research in automatic generatoin of tests from specifications based
on counterexample and witness generation techniques of model checking.
One important issue in test generation is the notion of coverage,
which limits the type and number of tests generated. Many coverage
criteria have been proposed to reflect different test requirements,
such as control-flow and data-flow based coverages. However, these
general criteria are not for generating tests that are tailored
to checking if an implementation satisfies specific properties.
This paper proposes a framework in which tests are generated from
user specified properties. In our framework, temporal logic LTL
is used to express both desirable and undesirable properties. One
difficulty in employing LTL for test generation is that, for a given
LTL formula, it may be necessary to generate a test suite in which
a test is arbitrarily long and the number of tests is infinite.
The paper shows that it is possible to test a given LTL property
on a black-box implementation with a finite test suite, assuming
that an upper bound on the number of states in the implementation
is known.
MS-CIS-03-03
Herbert Tanner, Ali Jadbabaie, George
J. Pappas
This paper investigates the aggregated stability properties of of
a system of multiple mobile agents described by simple dynamical
systems. The agents are steered through local coordinating control
laws that arise as a combination of attractive/repulsive and alignment
forces. These forces ensure collision avoidance and cohesion of
the group and result to all agents attaining a common heading angle,
exhibiting flocking motion. Two cases are considered: in the first,
position information from all group members is available to each
agent; in the second, each agent has access to position information
of only the agents laying inside its neighborhood. It is then shown
that regardless of any arbitrary changesin the neighbor set, the
flocking motion remains stable as long as the graph that describes
the neighboring relations among the agents in the group is always
connected.
MS-CIS-03-04
Hyho: Hybrid Hierarchical
Overlay Routing with Reduced Route Stretch and Replica Support
Noriyuki Takahashi,
Jonathan M. Smith
MS-CIS-03-05
Jonathan M. Smith
MS-CIS-03-06
"IHA: Ensuring Sound
Numerical Simulation of Hybrid Automata"
Jin-Young Choi, Yerang
Hur, and Insup Lee
MS-CIS-03-07
Generating embedded
software from hierarchical hybrid models
Rajeev Alur, Franjo
Ivancic, Jesung Kim, Insup Lee, and Oleg Sokolsky
MS-CIS-03-08
A Language for Bi-Directional
Tree Transformations
Michael B. Greenwald,
Jonathan T. Moore, Benjamin C. Pierce, and Alan Schmitt
MS-CIS-03-09
Oleg Naroditsky and
Kostas Daniilidis
MS-CIS-03-10
Bootstrapping Annotation
for Information Extraction using Pre-Existing Knowledge Sources
Andrew I. Schein, Sharon
J. Diskin, S. Ted Sandler, Fernando C. N. Pereira and Lyle H.
Ungar
MS-CIS-03-11
Daniel M. Bikel
This paper documents a large set of heretofore unpublished details
Collins used in his parser, such that, along with Collins' thesis
(Collins, 1999), this paper contains all information necessary to
duplicate Collins' benchmark results. Indeed, these as-yet-unpublished
details account for a full 11% reduction in error between a clean-room
implementation of Collins' model and an implementation including
all details. We also show a cleaner and equally--well-performing
method for the handling of punctuation and conjunction, and reveal
certain other probabilistic oddities about Collins' parser. We analyze
not only the effect of the unpublished details, but also re-analyze
the effect of certain well-known details, revealing that bilexical
dependencies are barely used by the model and that head choice is
not nearly as important to overall parsing performance as once thought.
Finally, we perform experiments that show that the true discriminative
power of lexicalization appears to lie in the fact that unlexicalized
syntactic structures are generated conditioning on the head word
and its part of speech.
MS-CIS-03-12
Fei Sha, Lawrence K. Saul and Daniel D.
Lee
Various problems in nonnegative quadratic programming arise in the
training of large margin classifiers. We derive multiplicative updates
for these problems that converge monotonically to the desired solutions
for hard and soft margin classifiers. The updates differ strikingly
in form from other multiplicative updates used in machine learning.
In this paper, we provide complete proofs of convergence for these
updates and extend previous work to incorporate sum and box constraints
in addition to nonnegativity.
MS-CIS-03-13
Reasoning about the
updatability of XML views over relational databases
Vanessa Braganholo, Susan Davidson and
Carlos Heuser
XML has become an important medium for data exchange, and is also
used as an interface to - i.e. a view of - a relational database.
While previous work has considered XML views for the purpose of
querying relational databases (e.g. Silkroute), in this paper we
consider the problem of updating a relational database through an
XML view. Using the nested relational algebra as the formalism for
an XML view of a relational database, we study the problem of when
such views are updatable. Our results rely on the observation that
in many XML views of relational databases, the nest operator occurs
last and the unnest operator does not occur at all. Since in this
case the nest operator is invertible, we can consider this important
class of XML views as if they were flat relational views."
MS-CIS-03-14
3XNF:Redundancy eliminating
XML storage in relations
Yi Chen,Susan Davidson,Yifeng Zheng
MS-CIS-03-15
Efficient XPath Processing
using T-labeling
Yi Chen,Susan Davidson,Yifeng Zheng
MS-CIS-03-16
Quadrilateral Meshes
for FE-Based Image Registration
Suneeta Ramaswami, Marcelo Siqueira, Tessa
Sundaram, James Gee, Jean Gallier
MS-CIS-03-17
Byron Choi, Peter Buneman
The usual method for storing tables in a relational database is
to store each tuple contiguously in secondary storage. A simple
alternative is to store the columns contiguously, so that a table
is represented as a set of vectors all of the same length. It has
been shown that such a representation performs well on queries requiring
few columns. This paper reviews the shredding scheme used in XMill,
an XML compressor, which represents the document structure by using
a set of files, consisting of a file describing the structure, and
files describing the character data to be found on designated paths
(corresponding to the column data). We consider such a shredding
as a storage model -- XML vectorization -- by presenting an indexing
scheme and a physical algebra associated with a detailed cost model.
We study query processing on the XML vectorization, in particular
the XML join queries. XML join queries are often translated into
a few relational join operations in the relational-based XML storage
systems. The use of columns enables us to develop a fast join algorithm
for vectorized XML based on two hash-based join algorithms. The
important feature of the join algorithm is that the disk access
of the algorithm is mostly sequential and the data not needed are
not read from disk. Experimental results demonstrate the effectiveness
of the join algorithm for vectorized XML.
MS-CIS-03-18
Using XQuery to build
updatable XML views over relational databases
Vanessa Braganholo, Susan Davidson and
Carlos Heuser
XML has become an important medium for data exchange, and is frequently
used as an interface to -- i.e. a view of -- a relational database.
Although much attention has been paid to the problem of querying
relational databases through XML views, the problem of updating
relational databases through XML views has not been addressed. In
this paper we investigate how a subset of XQuery can be used to
build updatable XML views, so that an update to the view can be
unambiguously translated to a set of updates on the underlying relational
database, assuming that certain key and foreign key constraints
hold. In particular, we show how views defined in this subset of
XQuery can be mapped to a set of relational views, thus transforming
the problem of updating relational databases through XML views into
a classical problem of updating relational databases though relational
views.
MS-CIS-03-19
Lawrence K. Saul, Fei Sha and Daniel D.
Lee
Nonnegativity constraints arise frequently in statistical learning
and pattern recognition. Multiplicative updates provide natural
solutions to optimizations involving these constraints. One well
known set of multiplicative updates is given by the Expectation-Maximization
algorithm for hidden Markov models, as used in automatic speech
recognition. Recently, we have derived similar algorithms for nonnegative
deconvolution and nonnegative quadratic programming. These algorithms
have applications to low-level problems in voice processing, such
as fundamental frequency estimation, as well as high-level problems,
such as the training of large margin classifiers. In this paper,
we describe these algorithms and the ideas that connect them.
MS-CIS-03-20
Ying Liu
Human hair simulation is a very challenging problem in computer
graphics. There are mainly three tasks in hair simulation - Hair
Shape Modeling, Hair Animation, and Hair Rendering. Many research
efforts have been done and various models have been developed for
these tasks, which fall mainly in the categories of explicit hair
models and volume density models. In this review, we present three
recent papers in the field of hair simulation. These three papers
employ different methods and concentrate on different tasks in hair
simulation. The first paper developed a dynamics-based explicit
model suitable for both hairstyle modeling and animation. The second
paper proposed a new method based on fluid flow, which can be taken
as a hybrid of explicit hair model and volume density model and
is designed specifically for hair shape modeling. The third paper
used a hybrid of explicit model and volume density model, called
cluster model, to deal with both modeling and rendering. Underlying
physical principles involved in the papers are especially explored
and explained. Advantages and disadvantages of each of these approaches
are discussed followed by a comparison of them with respect to the
three aspects of hair simulation.
MS-CIS-03-21
Preliminary Proceedings
of the Third International Workshop on Run-time Verification
Oleg Sokolsky and Mahesh Viswanathan,
Eds.
This volume contains the preliminary proceedings of the Third International
Workshop on Run-time Verification (RV~'03). RV~03 was held on July
13, 2003, as a satellite workshop of the International Conference
of Computer-Aided Verification (CAV~'03). The purpose of this workshop
has been to bring together researchers and practitioners, interested
in various aspects related to the dynamic analysis of software and
systems, with respect to formally specified correctness requirements.
Run-time verification aims to provide a ``lightweight'' complement
to traditional verification methods like model checking and theorem
proving, by analysing an actual implementation with respect to the
reduced correctness obligations of certifying the correctness of
a single execution. Despite the weaker guarantees, run-time verification
improves upon other more ad-hoc approaches in monitoring, by providing
formal proofs.
MS-CIS-03-22
Ubiquitous Peer-to-Peer
Network Architecture and Applications
Honghui Lu, Michael B. Greenwald, Björn
Knutsson, Jonathan T. Moore and Jonathan M. Smith
Ubiquitous peer-to-peer (UP2P) networking extends the peer-to-peer
model into the realms of ``thin clients'' and sensors. To address
increases in scale and diversity, as well as resource constraints,
we add programmability to some network nodes, so that the peers
share both processing and storage.
Our approach is motivated by two potential applications, PMIX and
STP. PMIX (Programmable Media Interchange) distributes computing
that transforms media contents appropriately for display and download
on user devices, ranging from desktops to a large variety of ``thin-clients''.
STP (Sensors to Peers) is designed to perform selection from, and
integration of, real-time sensory data from distributed groups of
sensors. UP2P node programmability is used to specify what data
are of interest (this can be thought of as {\it focus}) and how
to combine streams of data into more relevant information (this
can be thought of as fusion).
In UP2P, the programs executed ``in-network'' are conceptually part
of the producers or consumers of the data at the ends of the communication.
We are building the UP2P architecture using a combination of active
networking and transcoding systems that we have already implemented.
MS-CIS-03-23
V. Isler and J. Spletzer and S. Khanna
and C. J. Taylor
In this paper, we investigate data fusion techniques for target
tracking using distributed sensors. Specifically, we are interested
in how pairs of bearing or range sensors can be best assigned to
targets in order to minimize the expected error in the estimates.
We refer to this as the "focus of attention" (FOA) problem.
In its general form, FOA is NP-hard and not well approximable. However,
for specific geometries we obtain significant approximation results:
a 2-approximation algorithm for stereo cameras on a line, a PTAS
for when the cameras are equidistant, and a 1.42 approximation for
equally spaced range sensors on a circle. In addition to constrained
geometries, we further investigate the problem for general sensor
placement. By reposing as a maximization problem - where the goal
is to maximize the number of tracks with bounded error - we are
able to leverage results from maximum set-packing to render the
problem approximable. We demonstrate these in simulation for a target
tracking task, and for localizing a team of mobile agents in a sensor
network. These results provide insights into sensor/target assignment
strategies, as well as sensor placement in a distributed network.
MS-CIS-03-24
Sooha Park Lee
MS-CIS-03-25
Volkan Isler, Sampath Kannan and Sanjeev
Khanna
We study the following pursuit-evasion game: One or more hunters
are seeking to capture an evading rabbit on a graph. At each round,
the rabbit tries to gather information about the location of the
hunters but it can see them only if they are located on adjacent
nodes.
We show that two hunters always suffice for catching rabbits with
limited visibility. We distinguish between reactive rabbits who
move only when the hunter is visible and general rabbits who can
employ more sophisticated strategies. We present polynomial time
algorithms that decide whether a graph $G$ is hunter-win, that is,
if a single hunter can capture a rabbit of either kind on $G$.
MS-CIS-03-26
Geoffrey Washburn and
Stephanie Weirich
Higher-order abstract syntax is a
simple technique for implementing languages with functional programming.
Object variables and binders are implemented by variables and
binders in the host language. By using this technique, one can
avoid implementing common and tricky routines dealing with variables,
such as capture-avoiding substitution. However, despite the advantages
this technique provides, it is not commonly used because it is
difficult to write sound elimination forms (such as folds or catamorphisms)
for higher-order abstract syntax. To fold over such a datatype,
one must either simultaneously define an inverse operation (which
may not exist) or show that all functions embedded in the datatype
are parametric.
In this paper, we show how first-class polymorphism can be used
to guarantee the parametricity of functions embedded in higher-order
abstract syntax. With this restriction, we implement a library
of iteration operators over data-structures containing functionals.
From this implementation, we derive ``fusion laws'' that functional
programmers may use to reason about the iteration operator. Finally,
we show how this use of parametric polymorphism corresponds to
the Schürmann, Despeyroux and Pfenning method of enforcing
parametricity through modal types. We do so by using this library
to give a sound and complete encoding of their calculus into System
F<sub>ω</sub>. This encoding can serve as
a starting point for reasoning about
higher-order structures in polymorphic languages.
MS-CIS-03-27
Kostas G. Anagnostakis and Michael B.
Greenwald
Performance of peer-to-peer resource sharing networks depends upon
the level of cooperation of the participants. To date, cash-based
systems have seemed too complex, while lighter-weight credit mechanisms
have not provided strong incentives.
We propose exchange-based mechanisms for providing incentives for
cooperation in peer-to-peer file sharing networks. Peers give higher
service priority to requests from peers that can provide a simultaneous
and symmetric service in return. We generalize this approach to
n-way exchanges among rings of peers and present a search algorithm
for locating such rings. We have used simulation to analyze the
effect of exchanges on performance. Our results show that exchange-based
mechanisms can provide strong incentives for sharing, offering significant
improvements in service times for sharing users compared to free-riders,
without the problems and complexity of cash- or credit-based systems.
MS-CIS-03-28
Insik Shin and Insup Lee
We address the problem of providing compositional hard real-time
guarantees in a hierarchy of schedulers. We first propose a resource
model to characterize a periodic resource allocation and present
exact schedulability conditions for our proposed resource model
under the EDF and RM algorithms. Using the exact schedulability
conditions, we then provide methods to abstract the timing requirements
that a set of periodic tasks demands under the EDF and RM algorithms
as a single periodic task. With these abstraction methods, for a
hierarchy of schedulers, we introduce a composition method that
derives the timing requirements of a parent scheduler from the timing
requirements of its child schedulers in a compositional manner such
that the timing requirement of the parent scheduler is satisfied,
if and only if, the timing requirements of its child schedulers
are satisfied.
MS-CIS-03-29
E. Altug, V. Kumar, J. Ostrowski
This paper is about interpolation of three-dimensional rigid body
motions. In 3D motion, a rigid body moves along a curve as it changes
its position and orientation. Such a curve can be found using the
key frames, which are the frames at the beginning and the end. In
this study, five different methods are introduced. These methods
are product of exponentials, exponential of sum of twists, matrix
interpolation, linear quaternion interpolation and spherical linear
quaternion interpolation. Methods are compared analytically and
numerically, smooth interpolation curves are obtained. Comparison
of the methods is important, since each of these methods generate
the curve differently; some methods can be preferred over others
for some applications based on performance, computation requirements
or singularities involved.
MS-CIS-03-30
Sound Synchronization
of Communicating Hybrid Automata
Jin-Young Choi, Yerang
Hur, Jesung Kim, Insup Lee
MS-CIS-03-31
Björn Knutsson, Bryan Hopkins and Honghui
Lu
This paper addresses the problem of adapting streaming media to
various mobile and handheld devices. We propose a proxy-based approach
to improve the service scalability and availability. The proxy adapts
streams on-line to be a better match for increasingly diversified
client capabilities (such as screen size and color depth) and last-hop
bandwidths. In contrast to traditional transcoding, which breaks
the end-to-end model of the Web, we use server-directed transcoding
to support aggressive aggressive content transformations, while
preserving content semantics.
We show how server-directed transcoding can be integrated into the
implementation of a proxy. We discuss several useful transformations
for streaming content to demonstrate the potential of server-directed-transcoding.
Our approach can be implemented with minor modifications to off-the-shelf
codecs and tools. Measurements show that on-the-fly transcoding
for continuous media is a feasible solution with current processor
technology.
MS-CIS-03-32
A Survey and Critique
of American Sign Language Natural Language Generation and Machine
Translation Systems
Matthew P. Huenerfauth
MS-CIS-03-33
Volkan Isler, Sampath Kannan and Sanjeev
Khanna
This paper contains two main results: First, we revisit the well-known
visibility based pursuit-evasion problem and show that, in contrast
to deterministic strategies, a single pursuer can locate an unpredictable
evader in any simply-connected polygonal environment using a randomized
strategy. The evader can be arbitrarily faster than the pursuer
and it may know the position of the pursuer at all times. Second,
using the randomized algorithm together with the solution of a known
lion and man problem as subroutines, we present a strategy for two
pursuers (one of which is at least as fast as the evader) to quickly
capture an evader in a simply-connected polygonal environment.
MS-CIS-03-34
Energy-Aware Pre-Execution
and P-Thread Selection
Vlad Petric and Amir
Roth
MS-CIS-03-35
A Static Profile-Driven
Approach to Energy Efficient Register Integration
Anne Bracy, Vlad Petric,
and Amir Roth
MS-CIS-03-36
Unison: A File Synchronizer
and its Specification
Benjamin C. Pierce
and Jerome Vouillon
MS-CIS-03-37
G.Milford
Recently Grigoriev introduced
a new paradigm for applying representation theory to public-key
cryptography. This paper builds upon this application of algebra
and presents a practical public-key encryption system. Preliminary
evaluation is presented as well as suggestions for further work.
MS-CIS-03-38
LOOJ: Weaving LOOM
into Java
MS-CIS-03-39
Dynamic Principals
in Security-typed Languages
Stephen Tse and Steve
Zdancewic
MS-CIS-03-40
A Temporal Logic of
Nested Calls and Returns
Rajeev Alur, Kousha
Etessami, P. Madhusudan
MS-CIS-03-41
Visibly Pushdown Automata
Rajeev Alur, P. Madhusudan
MS-CIS-03-42
Bringing Harmony to
Optimistic Replication: A Synchronization Framework for Heterogeneous
Tree-Structured Data
Benjamin C. Pierce, Alan Schmitt, and
Michael B. Greenwald
MS-CIS-03-43
XML Goes Native: Run-time
Representations for Xtatic
Vladimir Gapeyev, Michael Y. Levin, Benjamin
C. Pierce, and Alan Schmitt
MS-CIS-03-44
Aaron Bloomfield, Norman I. Badler
MS-CIS-03-45
Aaron Bloomfield, Norman I. Badler
|
|