 | |
Sessions
take place in auditorium 4 unless otherwise indicated.Chair:
Peter Stuckey and Henning Christiansen | 09:15- | 09:30
| Introduction
and Prize Giving |
| 09:30- | 10:00
| Alessandra Russo, Imperial College, UK
Rob
Miller, U College London, UK
Bashar
Nuseibeh, The Open U, UK
Jeff
Kramer, Imperial College, UK
An
abductive approach for analysing event-based requirements
specifications
We
present a logic and logic programming based approach for
analysing event-based requirements specifications given in terms of a
system's reaction to events and safety properties. The approach uses a
variant of Kowalski and Sergot's Event Calculus to represent such
specifications declaratively and an abductive reasoning mechanism for
analysing safety properties. Given a system description and a safety
property, the abductive mechanism is able to identify a complete set of
counterexamples (if any exist) of the property in terms of symbolic "current"
states and associated
event-based transitions. A case study of an automobile cruise control
system specified in the SCR framework is used to illustrate our approach.
The technique described is implemented using existing tools for abductive
logic programming. |
| 10:00- | 10:30
| Tom Schrijvers, K.U. Leuven, Belgium
María
García de la Banda, Monash U, Australia
Bart
Demoen, K.U. Leuven, Belgium
Trailing
analysis for HAL
The
HAL language includes a Herbrand constraint solver which uses
Taylor's PARMA scheme rather than the standard WAM representation. This
allows HAL to generate more efficient Mercury code. Unfortunately, PARMA's
variable representation requires value trailing with a trail stack
consumption about twice as large as for the WAM. We present a trailing
analysis aimed at determining which Herbrand variables do not need to be
trailed. The accuracy of the analysis comes from HAL's semi-optional
determinism and mode declarations. The analysis has been partially
integrated in the HAL compiler and benchmark programs show good
speed-up. |
Chair:
Ulf Nilsson | 11:00- | 11:30
| Steve Barker, U Westminster, UK
Access
control for deductive databases by logic programming
We
show how logic programs may be used to protect deductive
databases from the unauthorized retrieval of positive and negative
information, and from unauthorized insert and delete requests. To achieve
this protection, a deductive database is expressed in a form that is
guaranteed to permit only authorized access requests to be performed. The
protection of the positive information that may be retrieved from a
database and the information that may be inserted are treated in a uniform
way as is the protection of the negative information in the database, and
the information that may be deleted. |
| 11:30- | 12:00
| Kung-Kiu Lau, U Manchester, UK
Michel
Vanden Bossche, Mission Critical, Belgium
Logic
programming for software engineering: A second chance
Current
trends in Software Engineering and developments in Logic
Programming lead us to believe that there will be an opportunity for Logic
Programming to make a breakthrough in Software Engineering. In this paper,
we explain how this has arisen, and justify our belief with a real-life
application. Above all, we invite fellow workers to take up the challenge
that the opportunity offers. |
| 12:00- | 12:30
| Alexander Bockmayr, LORIA Nancy, France
Arnaud
Courtois, LORIA Nancy, France
Using
hybrid concurrent constraint programming to model dynamic
biological systems
Systems
biology is a new area in biology that aims at achieving a
systems-level understanding of biological systems. While current genome
projects provide a huge amount of data on genes or proteins, lots of
research is still necessary to understand how the different parts of a
biological system interact in order to perform complex biological
functions. Computational models that help to analyze, explain or predict
the behavior of biological systems play a crucial role in systems biology.
The goal of this paper is to show that hybrid concurrent constraint
programming (Gupta/Jagadeesan/Saraswat 98) may be a promising alternative
to existing modeling approaches in systems biology. Hybrid cc is a
declarative compositional programming language with a well-defined
semantics. It allows one to model and simulate the dynamics of hybrid
systems, which exhibit both discrete and continuous change. We show that
Hybrid cc can be used naturally to model a variety of biological phenomena,
such as reaching thresholds, kinetics, gene interaction or biological
pathways. |
| 14:00- | 15:30
| David S. Warren, State U of New York-Stony Brook, USA
Invited
tutorial: Tabled logic programming |
Chair:
Kostis Sagonas | 16:00- | 16:30
| Witold Charatonik, MPI Saarbrücken, Germany
Supratik
Mukhopadhyay, MPI Saarbrücken, Germany
Andreas
Podelski, MPI Saarbrücken, Germany
Constraint-based
infinite model checking and tabulation for
stratified CLP
We
consider Gottlob, Grädel and Veith's
translation of branching time logic into Datalog LITE where global
model checking amounts to bottom-up
query evaluation. We define the safe branching time logic
Sµ that yields the fragment Datalog LIT
under this translation, and investigate an alternative evaluation strategy
for this fragment. Datalog LIT corresponds to Stratified CLP when we
represent the transition relation of an infinite-state system by a CLP
program. We give a tabulation procedure for the top-down
evaluation of stratified CLP programs and thus obtain a constraint-based local model checking procedure for Sµ. |
| 16:30- | 17:00
| Giridhar Pemmasani, State U of New York-Stony Brook,
USA
C.
R. Ramakrishnan, State U of New York-Stony Brook, USA
I.
V. Ramakrishnan, State U of New York-Stony Brook, USA
Efficient
real-time model checking using tabled logic programming
and constraints
Logic
programming based tools for real-time model checking are
beginning to emerge. In a previous work we had demonstrated the feasibility
of building such a model checker by combining constraint processing and
tabulation. But efficiency and practicality of such a model checker were
not adequately addressed. In this paper we describe XMC/dbm, an efficient
model checker for real-time systems using tabling. Performance gains in
XMC/dbm directly arise from the use of a lightweight constraint solver
combined with tabling. Specifically the timing constraints are represented
by difference bound matrices which are encoded as Prolog terms. Operations
on these matrices, the dominant component in real-time model checking, are
shared using tabling. We provide experimental evidence that the performance
of XMC/dbm is considerably better than our previous real-time model checker
and is highly competitive to other well known real-time model checkers
implemented in C/C++. An important aspect of XMC/dbm is that it can handle
verification of systems consisting of untimed components with performance
comparable to verification systems built specifically for untimed
systems. |
| 17:00- | 17:30
| Hasan M. Jamil, Mississipi State U, USA
Gillian
Dobbie, U Auckland, New Zealand
A
model theoretic semantics for multi-level secure deductive
databases
The
impetus for our current research is the need to provide an
adequate framework for belief reasoning in multi-level
secure (MLS) databases. We demonstrate that a prudent application of the
concept of inheritance in a deductive database setting will
help capture the notion of declarative belief and belief
reasoning in MLS databases in an elegant way. In this paper, we show that
these concepts can be captured in a F-logic style declarative query
language, called MultiLog, for MLS deductive databases for
which a model theoretic semantics exists. This development is significant
from a database perspective as it now enables us to compute the semantics
of MultiLog databases in a bottom-up fashion. The semantics developed here
is reminiscent of the stable model semantics of logic programs with
negation. We also define a bottom-up procedure to compute unique models of
stratified MultiLog databases. Finally, we also establish the equivalence
of MultiLog's three logical characterizations - model
theory, fixpoint theory and proof theory. |
Room:
Lobby Room:
Main entrance
|