110721.

On Nominal Delay Minimization in LUT-Based FPGA Technology Mapping
- Jason Cong,Yuzheng Ding
We study the nominal delay minimization problem in LUTbased
FPGA technology mapping, where interconnect delay
is assumed proportional to net fanout size. We prove that the
delay-optimal K-LUT mapping problem under the nominal
delay model is NP-hard when K 3, and remains NP-hard
for duplication-free mapping and tree-based mapping for
K 5 (but is polynomial time solvable for K = 2). We
also present a simple heuristic to take nominal delay into
consideration during LUT mapping for delay minimization.
1 Introduction
Lookup-table (LUT) based FPGA [8, 10] is a popular architecture
in which the basic programmable logic block is a
K-input lookup-table (K-LUT), built in SRAM, which can
implement any Boolean function of...

110722.

Automatic Verification of Transactions on an Object-Oriented Database
- David Spelt,Herman Balsters
. In the context of the object-oriented data model, a compiletime
approach is given that provides for a significant reduction of the
amount of run-time transaction overhead due to integrity constraint
checking. The higher-order logic Isabelle theorem prover is used to automatically
prove which constraints might, or might not be violated by a
given transaction in a manner analogous to the one used by Sheard and
Stemple (1989) for the relational data model. A prototype transaction
verification tool has been implemented, which automates the semantic
mappings and generates proof goals for Isabelle. Test results are discussed
to illustrate the effectiveness of our approach.
Keywords: object-oriented databases, transaction semantics, transaction
verification
1 Introduction
Static...

110723.

Guarded Evaluation: Pushing Power Management to Logic Synthesis/Design
- Vivek Tiwari,Sharad Malik,Pranav Ashar
The need to reduce the power consumption of the next
generation of digital systems is clearly recognized. At
the system level, power management is a very powerful
technique and delivers large and unambiguous savings.
This paper describes the development and application of
algorithms that use ideas similar to power management,
but that are applicable to logic level synthesis/design.
The proposed approach is termed guarded evaluation.
The main idea here is to determine, on a per clock cycle
basis, which parts of a circuit are computing results that
will be used, and which are not. The sections that are
not needed are then "shut off", thus saving the power
used in all the...

110724.

Bisimulation, Model Checking and Other Games
- Colin Stirling
Contents
1 Introduction 2
2 Process Calculi 2
3 Equivalences, Modal and Temporal Logics 6
3.1 Interactive games and bisimulations . . . . . . . . . . . . . . . 8
3.2 Modal logic and bisimulations . . . . . . . . . . . . . . . . . . . 13
3.3 Temporal properties and modal mu-calculus . . . . . . . . . . 15
3.4 Second-order propositional modal logic . . . . . . . . . . . . . . 21
4 Property Checking and Games 22
4.1 Subformulas and subsumption ....

110725.

Extending Temporal Actiom Logic for Ramification and Concurrency
- Joakim Gustafsson Link
An autonomous agent operating in a dynamical environment must be able
to perform several "intelligent" tasks, such as learning about the environment,
planning its actions and reasoning about the effects of the choosen
actions. For this purpose, it is vital that the agent has a coherent, expressive,
and well understood way to represent its knowledge about the world.
The research field "Logics of Action and Change" is concerned with using
logics for modeling agents and their interaction with dynamical, changing
environments.
In this thesis we extend an existing logic of action and change, TAL, to
handle ramification and concurrency.
Historically all knowledge about the dynamics of the modeled world has
been...

110726.

Generalized Notions of Mind Change Complexity
- Arun Sharma,Frank Stephan,Yuri Ventsov
Speed of convergence in Gold's identification in the limit
model can be measured by deriving bounds on the number
of mind changes made by a learner before the onset
of convergence. Two approaches to date are bounds
given by constants (referred here as Type 1) and bounds
expressed as constructive ordinals (referred as Type 2).
The use of ordinals has recently been successfully employed
to measure the mind change complexity of learning
rich concept classes such as unions of pattern languages,
elementary formal systems and logic programs.
Motivated by these applications, the present work introduces
two more general approaches to bounding mind
changes. These are based on counting by going down in
a...

110727.

On the Declarative and Procedural Semantics of Logic Programs
- Teodor C. Przymusinski
One of the most important and difficult problems in logic programming is
the problem of finding a suitable declarative or intended semantics for logic programs.
The importance of this problem stems from the declarative character
of logic programming, whereas its difficulty can be largely attributed to the
non-monotonic character of the negation operator used in logic programs. The
problem can therefore be viewed as the problem of finding a suitable formalization
of the type of non-monotonic reasoning used in logic programming.
In this paper we introduce a semantics of logic programs based on the class
PERF(P) of all, not necessarily Herbrand, perfect models of a program P and...

110728.

Subsumption for Semantic Query Optimization in OODB
- Domenico Beneventano,Sonia Bergamaschi,Claudio Sartori
The purpose of semantic query optimization is to use semantic knowledge
(e.g. integrity constraints) for transforming a query into an equivalent
one that may be answered more efficiently than the original version. This
paper proposes a general method for semantic query optimization in the
framework of OODBs (Object Oriented Database Systems). The method
is applicable to the class of conjunctive queries and is based on two ingredients:
a description logic able to express both class descriptions and
integrity constraints rules (IC rules) as types; subsumption computation
between types to evaluate the logical implications expressed by IC rules.
1 Introduction
In database environment, semantic knowledge is usually expressed in terms of...

110729.

Modeling a Hardware Synthesis Methodology in Isabelle
- David Basin,Stefan Friedrich
. Formal Synthesis is a methodology developed at Kent for
combining circuit design and verification. We have reinterpreted this
methodology in Isabelle's theory of higher-order logic so that circuits
are synthesized using higher-order resolution. Our interpretation simplifies
and extends Formal Synthesis both conceptually and in implementation.
It also supports integration of this development style with
other synthesis methodologies and leads to techniques for developing new
classes of circuits, e.g., recursive descriptions of parameterized circuits.
1 Introduction
Verification by formal proof is time intensive and this is a burden in bringing
formal methods into software and hardware design. One approach to reducing the
verification burden is to combine development and verification by...

110730.

Factored Edge-Valued Binary Decision Diagrams
- Paul Tafertshofer,Massoud Pedram
Factored Edge-Valued Binary Decision Diagrams form an extension to Edge-Valued Binary Decision
Diagrams. By associating both an additive and a multiplicative weight with the edges,
FEVBDDs can be used to represent a wider range of functions concisely. As a result, the computational
complexity for certain operations can be significantly reduced compared to EVBDDs.
Additionally, the introduction of multiplicative edge weights allows us to directly represent the
so-called complement edges which are used in OBDDs, thus providing a one to one mapping of
all OBDDs to FEVBDDs. Applications such as integer linear programming and logic verification
that have been proposed for EVBDDs also benefit from the extension. We...

110731.

An Industrial Strength Theorem Prover for a Logic Based on Common Lisp
- Matt Kaufmann,J Strother Moore
ACL2 is a re-implemented extended version
of Boyer and Moore's Nqthm and Kaufmann's Pc-Nqthm,
intended for large scale verification projects. This paper
deals primarily with how we scaled up Nqthm's logic to an
"industrial strength" programming language --- namely, a
large applicative subset of Common Lisp --- while preserving
the use of total functions within the logic. This makes
it possible to run formal models efficiently while keeping
the logic simple. We enumerate many other important features
of ACL2 and we briefly summarize two industrial
applications: a model of the Motorola CAP digital signal
processing chip and the proof of the correctness of the kernel
of the floating point division algorithm on...

110732.

Paralleltermgraphrewritingand Concurrent Logic Programs
- G. A. Papadopoulos
General term graph rewriting is a powerful computational model, suitable for implementing
a wide variety of declarative language paradigms. Here, we address the problems involved
in the implementation, on a loosely-coupled architecture, of an intermediate language
based on term graph rewriting, DACTL. In general, such problems are severe, so a subset
of this language called MONSTR is defined, free from some of the inefficiencies in the
original model (such as an excessive necessity for locking). Superficially, much of the
expressiveness of the original model is compromised thereby, especially with regard to the
implementation of concurrent logic languages. However, transformation techniques that
are valid in the context of declarative...

110733.

From Sound and Complete to Approximate Deduction
- Fabio Massacci
. The computational complexity of reasoning in classical and non-classical logics
makes traditional deduction not feasible in practice. This paper advocates the introduction
of approximate proofs within automated deduction for classical and non-classical logics and
a corresponding intuition of superficial semantics to overcome this limitation.
Recent and past years have seen a vigorous development of automated deduction procedures
for classical and non-classical logics. Calculi for logics for knowledge and belief, actions and
programs, concurrency and temporal reasoning, description logics for knowledge representation
have been developed (e.g. see [2, 3, 6, 7, 10, 11]) and corresponding systems implemented.
Classical logic has gone far beyond and competitions between provers are...

110734.

Disjunctive Defaults
- Michael Gelfond,Vladimir Lifschitz
A generalization of Reiter's default logic is
proposed that provides an improved treatment
of default reasoning with disjunctive information.
The new system --- the disjunctive
default logic --- is used in the paper to reexamine
the "broken-hand" example of Poole.
We also compare the expressive power of this
approach with two other approaches which
interpret disjunctive information within the
standard default logic. Finally, we show that
our semantics of disjunctive default logic is a
generalization of the semantics of disjunctive
and extended disjunctive databases.
1 INTRODUCTION
In this paper we generalize the theory of default reasoning
developed by Reiter [Rei80]. The generalization
is motivated by a difficulty encountered in attempts to
use defaults in the presence of...

110735.

A Logical Characterization of Bisimulation for Labeled Markov Processes
- Abbas Edalat,Prakash Panangaden
This paper gives a logical characterization of probabilistic bisimulation for Markov processes
introduced in [BDEP97]. The thrust of that work was an extension of the notion of bisimulation
to systems with continuous state spaces; for example for systems where the state space is
the real numbers. In the present paper we study the logical characterization of probabilistic
bisimulation for such general systems. This study revealed some unexpected results even for
discrete probabilistic systems.
ffl Bisimulation can be characterized by a very weak modal logic. The most striking feature
is that one has no negation or any kind of negative proposition.
ffl Bisimulation can be characterized by several inequivalent...

110736.

Induction of First-Order Decision Lists: Results on Learning the Past Tense of English Verbs
- Raymond J. Mooney,Mary Elaine Califf
This paper presents a method for inducing logic programs from examples that learns
a new class of concepts called first-order decision lists, defined as ordered lists of clauses
each ending in a cut. The method, called Foidl, is based on Foil (Quinlan, 1990) but
employs intensional background knowledge and avoids the need for explicit negative examples.
It is particularly useful for problems that involve rules with specific exceptions,
such as learning the past-tense of English verbs, a task widely studied in the context of the
symbolic/connectionist debate. Foidl is able to learn concise, accurate programs for this
problem from significantly fewer examples than previous methods (both connectionist...

110737.

Reinforcement Learning of Hierarchical Fuzzy Behaviors for Autonomous Agents
- Andrea Bonarini,Proyecto Sur Ediciones
Reinforcement learning is a suitable
approach to learn behaviors for
Autonomous Agents, but it is usually too
slow to be applied in real time on embodied
agents [8]. In this paper, we present the
results that we have obtained by adopting a
careful design of the control architecture and
of the learning sessions, aimed at reducing
the learning computation. The agent learns
in simplified environments one or more
basic behaviors, then it learns how to put
them together, and, finally, it adapts the
behaviors previously learnt, running in the
operating environment. This makes it
possible to cut the computational effort to
learn the control system. Moreover, this
approach produces in simulation a first
behavior that enables the...

110738.

Performance Prediction for the HTMT: A Programming Example
- Jose Nelson Amaral,Guang R. Gao,Phillip Merkey,Thomas Sterling,Zachary Ruiz,Sean Ryan
This paper presents an analytical performance prediction
for the implementation of Cannon's matrix multiply
algorithm in the Hybrid Technology Multi-Threading
(HTMT) architecture [8]. The HTMT subsystems are
built from new technologies: super-conducting processor
elements (called SPELLs [5]), a network based on
RSFQ (Rapid Single Flux Quantum) logic devices (called

110739.

Oracle Semantics for Prolog
- Roberto Barbuti,Michael Codish,Roberto Giacobazzi,Michael Maher
This paper proposes to specify semantic definitions for logic programming languages such
as Prolog in terms of an oracle which specifies the control strategy and identifies which
clauses are to be applied to resolve a given goal. The approach is quite general. It is
applicable to Prolog to specify both operational and declarative semantics as well as other
logic programming languages.
Previous semantic definitions for Prolog typically encode the sequential depth-first search
of the language into various mathematical frameworks. Such semantics mimic a Prolog
interpreter in the sense that following the "leftmost" infinite path in the computation tree
excludes computation to the right of this path from being...

110740.

Generalized Search Trees for Database Systems
)
Joseph M. Hellerstein
University of Wisconsin, Madison
jmh@cs.berkeley.edu
Jeffrey F. Naughton
University of Wisconsin, Madison
naughton@cs.wisc.edu
Avi Pfeffer
University of California, Berkeley
avi@cs.berkeley.edu
Abstract
This paper introduces the Generalized Search Tree (GiST), an index
structure supporting an extensible set of queries and data types. The
GiST allows new data types to be indexed in a manner supporting
queries natural to the types; this is in contrast to previous work on
tree extensibility which only supported the traditional set of equality
and range predicates. In a single data structure, the GiST provides
all the basic search tree logic required by a database system, thereby
unifying disparate structures such as B+-trees and R-trees in a single
piece of code, and...