110721.

Local Specification of Distributed Families of Sequential Objects
- Hans-dieter Ehrich
. Fully concurrent models of distributed object systems are
specified using linear temporal logic that does not per se cope with concurrency.
This is achieved by employing the principle of local sequentiality:
we specify from local viewpoints assuming that there is no intraobject
concurrency but full inter-object concurrency. Local formulae are
labelled by identity terms. For interaction, objects may refer to actions
of other objects, e.g., calling them to happen synchronously. A locality
predicate allows for making local statements about other objects. The
interpretation structures are global webs of local life cycles, glued together
at shared communication events. These interpretation structures are
embedded in an interpretation frame that is a...

110722.

Sorting on a Parallel Pointer Machine with Applications to Set Expression Evaluation
- Michael T. Goodrich,S. Rao Kosaraju
We present optimal algorithms for sorting on parallel CREW and
EREW versions of the pointer machine model. Intuitively, one can view
our methods as being based on a parallel mergesort using linked lists
rather than arrays (the usual parallel data structure). We also show how
to exploit the "locality" of our approach to solve the set expression evaluation
problem, a problem with applications to database querying and
logic-programming, in O(log n) time using O(n) processors. Interestingly,
this is an asymptotic improvement over what seems possible using previous
techniques.
Categories and Subject Descriptors: E.1 [Data Structures]: arrays, lists;
F.2.2. [Analysis of Algorithms and Problem Complexity]: Nonnumerical
Algorithms and Problems---sorting and searching
General Terms:...

110723.

Multi-Level Logic Optimization by Implication Analysis
- Wolfgang Kunz,Prem R. Menon
This paper proposes a new approach to multilevel
logic optimization based on ATPG (Automatic Test Pattern
Generation). Previous ATPG-based methods for logic
minimization suffered from the limitation that they were quite
restricted in the set of possible circuit transformations. We
show that the ATPG-based method presented here allows (in
principle) the transformation of a given combinational network
C into an arbitrary, structurally different but functionally
equivalent combinational network C'. Furthermore, powerful
heuristics are presented in order to decide what network manipulations
are promising for minimizing the circuit. By identifying
indirect implications between signals in the circuit,
transformations can be derived which are "good" candidates
for the minimization of the circuit. In particular, it...

110724.

Decidability and Finite Model Property of Substructural Logics
- Hiroakira Ono
this paper, we will give a short survey of results on decision problems and the finite
model property of substructural logics. The paper is far from a complete list of these
results, since a lot of results have been obtained already in some restricted classes of
substructural logics, like relevant logics, and therefore it is impossible to cover all of
them. ( As for surveys of decision problems and the finite model property of relevant
logics, see e.g. [1, 2, 7]. Also, see [16] for a survey of decision problems of logics related
to linear logic. ) Our aim of the present paper is to try...

110725.

Inductive Logic Programming for Natural Language Processing
- Raymond J. Mooney
. This paper reviews our recent work on applying inductive
logic programming to the construction of natural language processing
systems. We have developed a system, Chill, that learns a parser from a
training corpus of parsed sentences by inducing heuristics that control an
initial overly-general shift-reduce parser. Chill learns syntactic parsers
as well as ones that translate English database queries directly into executable
logical form. The ATIS corpus of airline information queries was
used to test the acquisition of syntactic parsers, and Chill performed
competitively with recent statistical methods. English queries to a small
database on U.S. geography were used to test the acquisition of a complete
natural language interface,...

110726.

Built-in Chaining: Introducing Complex Components into Architectural Synthesis
- Peter Marwedel,Birger L,Rainer Domer,Lehrstuhl Informatik Xii
: In this paper, we extend the set of library components which are usually considered
in architectural synthesis by components with built-in chaining. For such components, the result
of some internally computed arithmetic function is made available as an argument to some other
function through a local connection. These components can be used to implement chaining in a
data-path in a single component. Components with built-in chaining are combinatorial circuits.
They correspond to "complex gates" in logic synthesis. If compared to implementations with
several components, components with built-in chaining usually provide a denser layout, reduced
power consumption, and a shorter delay time. Multiplier/accumulators are the most prominent
example...

110727.

Logic Programming in the LF Logical Framework
- Frank Pfenning
this paper we describe Elf, a meta-language intended for environments dealing
with deductive systems represented in LF.
While this paper is intended to include a full description of the Elf core language, we only state,
but do not prove here the most important theorems regarding the basic building blocks of Elf. These
proofs are left to a future paper. A preliminary account of Elf can be found in [26]. The range of
applications of Elf includes theorem proving and proof transformation in various logics, definition
and execution of structured operational and natural semantics for programming languages, type
checking and type inference, etc. The basic idea behind Elf...

110728.

Programming with Logical Queries, Bulk Updates and Hypothetical Reasoning
- Weidong Chen
This paper presents a language of update programs that integrates logical queries, bulk updates
and hypothetical reasoning in a seamless manner. There is no syntactic or semantic distinction
between queries and updates. Update programs extend logic programs with negation in both syntax
and semantics. Users can specify bulk updates in which an arbitrary update is applied simultaneously
for all answers of an arbitrary query. Hypothetical reasoning is naturally supported by testing the
success or failure of an update. We describe an alternating fixpoint semantics of update programs
and show that it can express all nondeterministic database transformations. Current techniques of
logical query evaluation can be generalized for...

110729.

Fuzzy Based Rate Control for Real-Time MPEG Video
- Danny H. K. Tsang,Brahim Bensaou
In this paper, we propose a fuzzy logic based
control scheme for real time MPEG video to avoid long delay
or excessive loss at the user-network interface (UNI) in
an ATM network. The system consists of a shaper whose
role is to smooth the MPEG output traffic to reduce the
burstiness of the video stream. The input and output rates
of the shaper buffer are controlled by two fuzzy logic based
controllers. To avoid a long delay at the shaper, the first
controller aims to tune the output rate of the shaper based
on the number of available transmission credits at the UNI
and the occupancy of the shaper's buffer...

110730.

Breaking Security Protocols as an AI Planning Problem
- Fabio Massacci
. Properties like confidentiality, authentication and integrity
are of increasing importance to communication protocols. Hence the development
of formal methods for the verification of security protocols.
This paper proposes to represent the verification of security properties as
a (deductive or model-based) logical AI planning problem. The key intuition
is that security attacks can be seen as plans. Rather then achieving
"positive" goals a planner must exploit the structure of a security protocol
and coordinate the communications steps of the agents and the
network (or a potential enemy) to reach a security violation.
The planning problem is formalized with a variant of dynamic logic where
actions are explicit computation (such as...

110731.

Towards the Functional Verification of Large Sequential Circuits
- C. A. J. Van Eijk,J. A. G. Jess
Verifying the equivalence of sequential circuits is computationally
expensive. Therefore it is interesting to investigate
whether a divide-and-conquer strategy can be used to
manage the complexity of this problem. This approach
requires a verification method which combines an effective
decomposition technique with a powerful base verification
algorithm. In this paper, we discuss how functional
dependencies can be used to find a good decomposition
and to improve the performance of the base verification
algorithm.
1. Introduction
Formal verification methods are clearly gaining acceptance
in industry. Especially for combinational equivalence
checking, automated tools are being developed which are
sufficiently powerful to verify the functional correctness of
circuits generated by a logic synthesis tool or manually by a
designer....

110732.

Entrenchment Relations: A Uniform Approach to Nonmonotonicity
- Konstantinos Georgatos
. We show that Gabbay's nonmonotonic consequence relations can be
reduced to a new family of relations, called entrenchment relations. Entrenchment
relations provide a direct generalization of epistemic entrenchment and expectation
ordering introduced by Gardenfors and Makinson for the study of belief
revision and expectation inference, respectively.
Keywords: Nonmonotonic consequence, epistemic entrenchment, belief revision.
1 Introduction
Nonmonotonicity has offered great promise as a logical foundation for knowledge representation
formalisms. The reason for such a promise is that nonmonotonic logic completes
in a reasonable way our (incomplete) knowledge and withdraws conclusions in
the light of new information. Therefore, most approaches to central problems of Artificial
Intelligence, such as belief revision, database updating,...

110733.

Mathematical Models for Computing Science
- C. A. R. Hoare
ion and Quantification 46
6.1 Transistor nets implement logic gates : : : : : : : : : : : : : : 49
6.2 Combinational logic implements natural numbers : : : : : : : 50
6.3 Sequential circuits implement combinational : : : : : : : : : : 50
6.4 From transistors to sequential circuits : : : : : : : : : : : : : 51
6.5 Functions implement relations : : : : : : : : : : : : : : : : : : 53
6.6 Sequential programs implement parallel : : :...

110734.

A Natural Deduction Approach to Dynamic Logic
- Furio Honsell
. Natural Deduction style presentations of program logics are
useful in view of the implementation of such logics in interactive proof
development environments, based on type theory, such as LEGO, Coq,
etc. In fact, ND-style systems are the kind of systems which can take
best advantage of the possibility of reasoning "under assumptions" offered
by proof assistants generated by Logical Frameworks. In this paper
we introduce and discuss sound and complete proof systems in Natural
Deduction style for representing various "truth" consequence relations of
Dynamic Logic. We discuss the design decisions which lead to adequate
encodings of these logics in Coq. We derive in Dynamic Logic a set of
rules...

110735.

An Automata-Theoretic Decision Procedure for Propositional Temporal Logic with Since and Until
- Y. S. Ramakrishna,L. E. Moser,L. K. Dillon,P. M. Melliar-smith,G. Kutty
We present an automata-theoretic decision procedure for Since/Until Temporal
Logic (SUTL), a linear-time propositional temporal logic with strong non-strict
since and until operators. The logic, which is intended for specifying and reasoning
about computer systems, employs neither next nor previous operators. Such
operators obstruct the use of hierarchical abstraction and refinement and make
reasoning about concurrency difficult. A proof of the soundness and completeness
of the decision procedure is given, and its complexity is analyzed.
AMS Subject Classification: 03B25, 03B35, 03B45, 68Q40, 68Q68, 68T15
1 Introduction
Since/Until Temporal Logic (SUTL) is a linear-time temporal logic based on propositional
calculus and the temporal operators until U and since S. The U...

110736.

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...

110737.

An Algebraic Characterization of First-Order Definability
- A. J. Kfoury,M. Wymann-boni
We give a variable-free relational calculus which defines exactly all first-order definable relations
in a arbitrary structure. We then show that, over an arbitrary class C of finite ordered
structures with signature f!!!; R 1 ; : : : ; R ff g, the unary relations uniformly defined by this calculus
over C are characterized by a another simplified variable-free calculus which we call Q. Q is
the least set of formal expressions such that:
Q ' f?; R 1 ; : : : ; R ff g [
f(QPhiPhiPhix) j Q 2 Q; x 2 ! [ f1gg [ f(QPsiPsiPsix) j Q 2 Q; x...

110738.

Toward the Optimization of a Class of Black Box Optimization Algorithms
- Gang Wang,Erik D. Goodman,William F. Punch
Many black box optimization algorithms have sufficient
flexibility to allow them to adapt to the varying
circumstances they encounter. These capabilities
are of two primary sorts: 1) user-determined choices
among alternative parameters, operations, and logic
structures, and 2) the algorithm-determined alternative
paths chosen during the process of seeking a solution
to a particular problem. This paper discusses
the process of algorithm design and operation, with
the intent of integrating the seemingly distinct aspects
described above within a unified framework. We relate
this algorithmic optimization process to the field
of dynamic process control. An approach is proposed
toward the optimization of a process for controlling
a specific class of systems, and its application to dynamic
adjustment...

110739.

Pattern Independent Maximum Current Estimation in Power and Ground Buses of CMOS VLSI Circuits: Algorithms, Signal Correlations and Their Resolution
- Harish Kriplani,Farid Najm,Ibrahim Hajj
Currents flowing in the power and ground (P&G) buses of CMOS digital circuits affect both
circuit reliability and performance by causing excessive voltage drops. Excessive voltage drops
manifest themselves as glitches on the P&G buses and cause erroneous logic signals and degradation
in switching speeds. Maximum current estimates are needed at every contact point in
the buses to study the severity of the voltage drop problems and to redesign the supply lines
accordingly. These currents, however, depend on the specific input patterns that are applied
to the circuit. Since it is prohibitively expensive to enumerate all possible input patterns, this
problem has, for a long time, remained...

110740.

Probabilistic Reasoning under Ignorance
- Marco Ramoni,Alberto Riva,Vimla L. Patel
The representation of ignorance is a long standing challenge
for researchers in probability and decision theory.
During the past decade, Artificial Intelligence researchers
have developed a class of reasoning systems,
called Truth Maintenance Systems, which are able to
reason on the basis of incomplete information. In this
paper we will describe a new method for dealing with
partially specified probabilistic models, by extending
a logic-based truth maintenance method from Boolean
truth-values to probability intervals. Then we will illustrate
how this method can be used to represent Bayesian
Belief Networks --- one of the best known formalisms to
reason under uncertainty --- thus producing a new class
of Bayesian Belief Networks, called Ignorant Belief...