A New Approach for Specification and Verification of Distributed Agents
- Andrew M. Mironov,Virendra C. Bhavsar
We propose a language for formal description of distributed
agents and introduce a new approach to their specification.
The specification language uses the concept of a fixpoint
construction, which is a generalization of temporal operators
in temporal logic. With the proposed formalism we
are also able to construct correctness proofs for distributed
agents. The verification technique is a generalization of
the Floyd's inductive assertion method.
Keywords: distributed agents, specification, verification,
assertions, fixpoint construction.
The problem of specification and formal verification of distributed
communicating systems (DCS) is one of most important
problems in theoretical computer science. DCSs
arise in a wide range of applications, for example in distributed
information processing, telecommunications, control
of complex systems...
A Calculus for Interrogatives Based on Their Algebraic Semantics
- Rani Nelken,Nissim Francez
We present a novel calculus for reasoning with both indicative and interrogative sentences, simultaneously
modeling entailment between indicative sentences, entailment between interrogative
sentences and answerhood relations. The logic is based on an interpretation of questions
as entities of type t, the type of propositions. This is achieved by an algebraic reinterpretation
of the domain of type t as a bilattice, rather than the standard boolean interpretation. We
provide a Gentzen style axiomatization of the logic and prove its soundness and completeness
with respect to the bilattice semantics. We also consider an alternative formulation using
multi-valued free variable first-order tableaux, allowing for e#cient algorithmic proof-search.
We have implemented the...
Sequents, Frames, and Completeness
- Thierry Coquand
. Entailment relations, originated from Scott, have been used
for describing mathematical concepts constructively and for representing
categories of domains. This paper gives an analysis of the freely generated
frames from entailment relations. This way, we obtain completeness
results under the unifying principle of the spatiality of coherence logic. In
particular, the domain of disjunctive states, derived from the hyperresolution
rule as used in disjunctive logic programs, can be seen as the frame
freely generated from the opposite of a sequent structure. At the categorical
level, we present equivalences among the categories of sequent
structures, distributive lattices, and spectral locales using appropriate
Entailment relations were introduced by Scott as an...
Declarative Specification of Z39.50 Wrappers using Description Logics
- Yannis Velegrakis,Vassilis Christophides,Panos Constantopoulos
. Z39.50 is a client#server protocol widely used in digital libraries
and museums for searching and retrieving information spread over
anumber of heterogeneous sources. Toovercome semantic and schematic
discrepancies among the various data sources the protocol relies on a
world view of information as a #at list of #elds, called Access Points
#AP#. One of the major issues for building Z39.50 wrappers is to map
this unstructured list of APs to the underlying source data. Unfortunately,
existing Z39.50 wrappers have been developed from scratch and
they do not provide high-level mapping languages with veri#able properties.
In this paper, we propose a Description Logic based toolkit for
the declarative speci#cation of...
Possibly Infinite Sequences in Theorem Provers: A Comparative Study
- Marco Devillers,David Griffioen
. We compare four different formalizations of possibly infinite
sequences in theorem provers based on higher-order logic. The formalizations
have been carried out in different proof tools, namely in Gordon's
HOL, in Isabelle and in PVS. The comparison considers different logics
and proof infrastructures, but emphasizes on the proof principles that are
available for each approach. The different formalizations discussed have
been used not only to mechanize proofs of different properties of possibly
infinite sequences, but also for the verification of some non-trivial
theorems of concurrency theory.
Sequences occur frequently in all areas of computer science and mathematics.
In particular, formal models of distributed systems often employ (possibly infinite)
Binding-Time Analysis for Mercury
- Wim Vanhoof,Maurice Bruynooghe
In this paper, we describe a binding-time analysis (BTA) for a statically typed and
strongly moded pure logic programming language, in casu Mercury. Binding-time
analysis is the key concept in achieving o-line program specialisation: the analysis
starts from a description of the program's input available for specialisation, and
propagates this information throughout the program, deriving directives for when
and how to perform specialisation. Exploiting the possibilities oered by Mercury's
strong type and mode system, we present a completely automatic BTA dealing with
partially static binding-times.
Program specialisation is a well-studied source-to-source transformation, capable
of optimising a program P with respect to a known part s of its input
Formalising UML Use Cases in the Refinement Calculus
- Ralph-johan Back,Luigia Petre,Porres Paltor,Turku Centre,Computer Science
The Unified Modeling Language (UML) consists of a set of diagrams that
describe a system under development. A use case diagram specifies the required
functionality of the system, showing the collaboration among a set
of actors that are to perform certain tasks. We enhance use case diagrams
by providing formal documents (like specifications or programs), called contracts
that regulate the behaviour of the agents involved. These agents
could be programs, modules, systems, users. The contract is written in a
language with a precise semantics and logic for reasoning, the refinement
calculus. Hence, it can be analysed for the preconditions required in order
to achieve certain goals. In order to...
A WAM-based implementation for Composition of Logic Programs
- A. Chiarelli,V. Mazzotta,C. Renso
The main aim of this paper is to show an abstract machine for
compiling logic programs composed by means of meta-operators; in
particular, we deal with union, intersection and closure, which are
directly supported by the most common abstract machine for logic
programming: the Warren Abstract Machine. The proposed solution
is a mix of the interpretation-oriented and the compilation-oriented
approach such that it is possible to exploit the benefits and to reduce,
as possible, the drawbacks.
Many extensions of logic programming have been proposed to increase its
expressive power and to widen application area. Such extensions provide
tools to deal with typical problems of Artificial Intelligence (hypothetical
reasoning, knowledge assimilation)...
Linear Logical Characterization of Polyspace Functions (Extended Abstract)
Light Linear Logic (LLL) of [Gir95] characterizes the
polytime functions through a careful handling of structural
inference rules of logic. Based on this purely
logical approach, we give a characterization of the
Our logical system is an extension of Intuitionistic
Light Affine Logic (ILAL) of [Asp98], a variant of LLL
with full (unrestricted) weakening. We introduce the
notion of split terms and enrich ILAL by allowing a !-
box to be formed from a split term. The resulting system,
called Intuitionistic Polyspace Affine Logic, precisely
characterizes the polyspace functions.
Linear Logical Approach to Computational
Over the past few decades, a considerable number
of studies have been made on logical characterizations
Term-Rewriting Implementation of Equational Logic Programming
- Michael J. O'donnell
In 1975 I started a small project to explore the consequences of implementing
equational programs with no semantic compromises. Latest results
include a compiler that executes exactly the logical consequences of an equational
program, with run-time speed comparable to compiled Franz LISP.
This paper describes the accomplishments of the project very briefly, concentrating
on shortcomings and directions for future work.
The most common approach to providing semantics for programming languages
is to regard a program as the definition of a collection of functions.
In some cases great ingenuity is required to construct the unique function
associated with each symbol in a program. Inputs and outputs are regarded
Residuation and Guarded Rules for Constraint Logic Programming
- Gert Smolka
A major difficulty with logic programming is combinatorial explosion: since goals are solved
with possibly indeterminate (i.e., branching) reductions, the resulting search trees may grow
wildly. Constraint logic programming systems try to avoid combinatorial explosion by building
in strong determinate (i.e., non-branching) reduction in the form of constraint simplification.
In this paper, we present two concepts, residuation and guarded rules, for further strengthening
determinate reduction. Both concepts apply to constraint logic programming in general and
yield an operational semantics that coincides with the declarative semantics. Residuation
is a control strategy giving priority to determinate reductions. Guarded rules are logical
consequences of programs adding otherwise unavailable determinate reductions.
First Order Linear Temporal Logic over Finite Time Structures
- Serenella Cerrito,Marta Cialdea Mayer
In this work, the notion of provability for first order linear temporal logic over finite time structures, FO-LTL fin , is studied. We show that the validity problem for such a logic is not recursively enumerable, hence FO-LTL fin is not recursively axiomatizable. This negative result however does not hold in the case of bounded validity, that is truth in all temporal models where the object domain is possibly infinite, but the underlying sequence of time points does not exceed a given size. A formula is de ned to be k-valid if it is true in all temporal models whose...
HyTech: A Model Checker for Hybrid Systems
- Thomas A. Henzinger,Pei-hsin Ho,Howard Wong-toi
A hybrid system is a dynamical system whose behavior exhibits both discrete and continuous
change. A hybrid automaton is a mathematical model for hybrid systems, which combines, in
a single formalism, automaton transitions for capturing discrete change with differential equations
for capturing continuous change. HyTech is a symbolic model checker for linear hybrid
automata, a subclass of hybrid automata that can be analyzed automatically by computing with
polyhedral state sets. A key feature of HyTech is its ability to perform parametric analysis,
i.e. to determine the values of design parameters for which a linear hybrid automaton satisfies
a temporal-logic requirement.
A hybrid system typically consists of a...
Decision Procedure for
- Fausto Giunchiglia,Roberto Sebastiani
The goal of this paper is to describe and
thoroughly test a decision procedure, called
Ksat, checking satisfiability in the terminological
logic ALC. Ksat is said to be SATbased
as it is defined in terms of a decision
procedure for propositional satisfiability
(SAT). The tests are performed comparing
Ksat with, among other procedures, Kris,
a state-of-the-art tableau-based implementation
of a decision procedure for ALC. Ksat
outperforms Kris of orders of magnitude.
Furthermore, the empirical results highlight
an intrinsic weakeness that tableau-based decision
procedures have with respect to SATbased
The goal of this paper is to describe and thoroughly
test a new decision procedure, called Ksat, checking
satisfiability in the terminological logic ALC, as defined
Verification of Logic Programs and Imperative Programs
- Lee Naish
This paper explores the relationship between verification of logic programs and
imperative programs with the aim of uncovering the kinds of reasoning used
to construct logic programs. We discuss forward reasoning, such as that used
for verifying imperative programs using the inductive assertion method, and
backward reasoning, such as that used for verifying imperative programs using
subgoal induction and logic programs using consequence verification. We
argue that consequence verification is often inadequate for Prolog programs because
programmers make implicit assumptions about how procedures are called.
These assumptions can be made explicit using general type declarations.
Verification of logic programs with type declarations can be done in two steps.
A Constructive Game Semantics for the Language of Linear Logic
- Giorgi Japaridze
I present a semantics for the language of first order additive-multiplicative
linear logic, i.e. the language of classical first order logic with two sorts
of disjunction and conjunction. The semantics allows us to capture intuitions
often associated with linear logic or constructivism such as sentences
=games, sentences=resources or sentences=problems, where "truth"
means existence of an effective winning (resource-using, problem-solving)
The paper introduces a decidable first order logic ET in the above
language and gives a proof of its soundness and completeness (in the full
language) with respect to this semantics. Allowing noneffective strategies
in the latter is shown to lead to classical logic.
The semantics presented here is very similar...
Preference Logics for Automated Decision Making
- Vu Ha
Classical decision theory provides a normative theory for representing and reasoning with complex preferences. But straightforward application of this theory to construct automated decision making agents is difficult due to the high cost of eliciting utilities. People tend to express their preferences in qualitative terms and have troubles translating them into numeric utilities. This difficulty has recently sparked interests in studies of qualitative theories for decision making. In this paper I sample several such proposals which share the same focus on developing logic-oriented approaches to representing and reasoning with preferences.
Sharing and Groundness Dependencies in Logic Programs
- M. Codish,H. Sndergaard,P. J. Stuckey
We investigate Jacobs and Langen's Sharing domain for the analysis of set-sharing and show that it is
isomorphic to the Pos domain, introduced by Marriott and Sndergaard for the analysis of groundness
dependencies. The key idea is to view the sets of variables in a Sharing domain element as the models of a
corresponding Boolean function. This leads to re-casting set-sharing analysis in terms of the property of
"not being affected by the binding of a single variable." Such an "unaffectedness dependency" analysis
reveals close connections with groundness dependency analysis using positive Boolean functions. The
new view of set-sharing analysis improves our understanding of this type...
Exploiting ILP in Page-Based Intelligent Memory
- Mark Oskin,Justin Hensley,Diana Keen,Frederic T. Chong,Matthew Farrens,Aneet Chopra
This study compares the speed, area, and power of different
implementations of Active Pages [OCS98], an intelligent
memory system which helps bridge the growing gap between
processor and memory performance by associating simple
functions with each page of data. Previous investigations
have shown up to 1000X speedups using a block of reconfigurable
logic to implement these functions next to each subarray
on a DRAM chip.
In this study, we show that instruction-level parallelism,
not hardware specialization, is the key to the previous success
with reconfigurable logic. In order to demonstrate this
fact, an Active Page implementation based upon a simplified
VLIW processor was developed. Unlike conventional VLIW
processors, power and area constraints lead...
Pre-Layout Estimation of Individual Wire Lengths
- Srinivas Bodapati,Farid N. Najm
We present a novel technique for estimating
individual wire lengths in a given standardcell
-based design during the technology mapping
phase of logic synthesis. The proposed method is
based on creating a black box model of the place
and route tool as a function of a number of parameters
which are all available before layout. The place
and route tool is characterized, only once, by applying
it to a set of typical designs in a certain technology.
We also propose a net bounding box estimation
technique based on the layout style and net neighborhood
analysis. We show that there is inherent
variability in wire lengths obtained using commercially
available place and route tools...