For referring to the publications from within LATEX download the
.bib-file
(6 kB, needs
string definitions)
Data Refinement: Model-Oriented Proof
Methods and their Comparison
by Willem-Paul de Roever
and Kai Engelhardt (with the
assistance of Jos Coenen, Karl-Heinz Buth, Paul Gardiner, Yassine
Lakhnech, and Frank Stomp; Cambridge University
Press, 3rd December, 1998; 247
x 174 mm, ca. 430 pages, 18 half-tones, 44 diagrams, and 93 exercises;
ISBN 0 521 64170 5;
£45/US$69.95).
Abstract:
The goal of this book is to provide a comprehensive and systematic
introduction to the important and highly applicable method of data
refinement and proving simulation. The authors concentrate in the
first part on the general principles needed to prove data refinement
correct, and begin with an explanation of the fundamental notions,
showing that data refinement proofs reduce to proving simulation. The
topics of Hoare Logic and the Refinement Calculus are then introduced
and a general theory of simulations is developed and related to them.
Accessibility and comprehension are emphasised in order to guide
newcomers to the area.
The book's second part contains a detailed survey of important methods
in this area, such as VDM, and the methods due to Abadi & Lamport,
Hehner, Lynch and Reynolds, Back's refinement calculus and Z. All
these methods are carefully analysed, and shown to be either
incomplete, with counterexamples to their application, or to be always
applicable whenever data refinement holds.
This is shown by proving, for the first time, that all of them can be
described and analysed in terms of two simple notions: forward and
backward simulation.
The book is self-contained, going from advanced undergraduate level but
taking the reader to the state-of-the-art in methods for proving simulation.
It has its own web site
with a pointer to a
corrigendum.
Modal Logics with a Linear Hierarchy of Local Propositional
Quantifiers
by Kai Engelhardt, Ron van der
Meyden, and Kaile Su.
(Philippe Balbiani, Nobu-Yuki Suzuki, Frank Wolter, and Michael
Zakharyaschev, editors, Advances in Modal Logic IV, pages
9-30, King's College London Publications, 2003.)
Abstract:
Local propositions arise in the context of the semantics for logics
of knowledge in multi-agent systems. A proposition is local to an
agent when it depends only on that agent's local state. We consider
a logic, LLP, that extends S5, the modal logic of necessity (in
which the modality refers to truth at all worlds) by adding a
quantifier ranging over the set of all propositions and, for each
agent, a propositional quantifier ranging over the agent's local
propositions. LLP is able to express a large variety of epistemic
modalities, including knowledge, common knowledge and distributed
knowledge. However, this expressiveness comes at a cost: the logic
is equivalent to second order predicate logic when two independent
agents are present
[Engelhardt, van der Meyden and Moses,
TARK'98], hence undecidable and not
axiomatizable. This paper identifies a class of multi-agent S5
structures,
hierarchical structures, in which the agents'
information has the structure of a linear hierarchy. All systems
with just a single agent are hierarchical. It is shown that LLP
becomes decidable with respect to hierarchical systems. The main
result of the paper is the completeness of an axiomatization for the
hierarchical case.
Download a version of this paper similar to the published one.
(gnuzipped PostScript, 105kB)
Towards a Practitioners' Approach to Abadi and Lamport's
Method
by Kai Engelhardt and Willem-Paul de Roever
(Formal Aspects of Computing, 7(5):550-575,
1995.)
Abstract:
Our own basic intuitions are presented when introducing the method
developed by Abadi and Lamport in
[AL88]
for proving refinement
between specifications of nondeterministic programs correct to
people unacquainted with it. The example we use to illustrate this
method is a nontrivial communication protocol that provides a
mechanism analogous to message passing between migrating processes
within a fixed finite network of nodes due to Kleinman, Moscowitz,
Pnueli, and Shapiro
[KMPS91]. Especially the cruel last step of
a three step refinement proof of that protocol gives rise to a
deeper understanding of, and some small enhancements to, Abadi and
Lamport's 1988 method.
Download a version of this paper similar to the published one.
(gnuzipped PostScript, 100kB)
published (or to appear) in refereed proceedings.
A Refinement Theory that Supports Reasoning about
Knowledge and Time for Synchronous Agents
by Kai Engelhardt, Ron van der Meyden, and Yoram Moses. (In
Robert Nieuwenhuis and Andrei Voronkov, editors, 8th
International Conference on Logic for Programming, Artificial
Intelligence and Reasoning,
volume 2250 of LNAI, pages 125-141.
©Springer-Verlag, December 2001.)
Abstract:
An expressive semantic framework for program refinement that
supports both temporal reasoning and reasoning about the knowledge
of multiple agents is developed.
The refinement calculus owes the cleanliness of its decomposition
rules for all programming language constructs and the relative
simplicity of its semantic model to a rigid synchrony assumption
which requires all agents and the environment to proceed in
lockstep.
The new features of the calculus are illustrated in a derivation of
the two-phase-commit protocol.
Download a version of this paper similar to the published one.
(gnuzipped PostScript, 63kB,
or pdf, 145kB)
A Program Refinement Framework Supporting Reasoning about
Knowledge and Time
by Kai Engelhardt, Ron van der Meyden, and Yoram Moses. (In Jerzy
Tiuryn, editor, Foundations of Software
Science and Computation
Structures, pages 114-129, LNCS,
©Springer-Verlag, March, 2000.)
Abstract:
This paper develops a highly expressive semantic framework for
program refinement that supports both temporal reasoning and
reasoning about the knowledge of a single agent. The framework
generalizes a previously developed temporal refinement framework by
amalgamating it with a logic of quantified local propositions, a
generalization of the logic of knowledge. The combined framework
provides a formal setting for development of knowledge-based
programs, and addresses two problems of existing theories of such
programs: lack of compositionality and the fact that such programs
often have only implementations of high computational complexity.
Use of the framework is illustrated by a control theoretic example
concerning a robot operating with an imprecise position sensor.
Download a version of this paper similar to the published one.
(gnuzipped PostScript, 51kB,
or pdf, 137kB)
Knowledge and the Logic of Local Propositions
by Kai Engelhardt, Ron van der Meyden, and Yoram Moses. (In Itzhak
Gilboa, editor, Theoretical Aspects of Rationality and
Knowledge, Proceedings of the Seventh Conference
(TARK 1998), pages 29-41,
Morgan Kaufmann, July 1998.)
Abstract:
An agent's limited view of the state of a distributed system may
render globally different situations indistinguishable. A
proposition is local for this agent whenever his view suffices to
decide this proposition. Motivated by a framework for the
development of distributed programs from knowledge-based
specifications, we introduce a modal logic of local propositions, in
which it is possible to quantify over such propositions. We show
that this logic is able to represent a rich set of epistemic
notions. Under the usual strong semantics, this logic is not
recursively axiomatizable, however. We show that by weakening the
semantics of quantification, it is possible to obtain a logic that
is axiomatizable and is still able to express interesting epistemic
notions.
Download a version of this paper similar to the published one.
(gnuzipped PostScript, 84kB)
by Kai Engelhardt and Willem-Paul de Roever. (In Wojciech Penczek and
Andrzej Szalas, editors, Mathematical Foundations of Computer
Science 1996, 21st International Symposium,
MFCS
'96, Cracow,
Poland, Proceedings, volume 1113 of LNCS, pages 324-335.
©Springer-Verlag, September 1996.)
Abstract:
Data refinement is a powerful technique to derive implementations in
terms of low-level data structures like bytes from specification in
terms of high-level data structures like queues. The higher level
operations need not be coded as ordinary programs; it is more
convenient to introduce specification statements to the programming
language and use them instead of actual code. Specification
statements represent the maximal program satisfying a given
Hoare-triple. Sound and (relatively) complete simulation techniques
allow for proving data refinement by local arguments. A major
challenge for simulation consists of expressing the weakest lower
level specification simulating a given higher level specification
w.r.t. a given relation between these two levels of abstraction. We
present solutions to this challenge for upward and downward
simulation in both partial and total correctness frameworks, thus
reducing the task of proving data refinement to proving validity of
certain Hoare-triples.
Download a version of this paper similar to the published one.
(gnuzipped PostScript, 46kB)
by Kai Engelhardt and Willem-Paul de
Roever
(In Jim C.P.
Woodcock and Peter Gorm Larsen, editors, FME '93:
Industrial-Strength Formal Methods, volume 670 of LNCS,
pages 294-313. ©Springer-Verlag, April 1993.)
Abstract:
By adding a new technique and a simple proof strategy to Abadi &
Lamport's 1988 method
[AL88]
for proving refinement between
specifications of distributed programs correct, the inherent
limitation of their method, occurring when the abstract level of
specification features so-called infinite invisible nondeterminism
or internal discontinuity, can be sometimes overcome. This technique
is applied to the cruel last step of a three step correctness proof
for an algorithm for communication between migrating processes
within a finite network due to Kleinman, Moscowitz, Pnueli, &
Shapiro
[KMPS91].
©Springer-Verlag
Download a version of this paper similar to the published one.
(gnuzipped PostScript, 85kB)
Get Towards a Practitioners'
Approach to Abadi and Lamport's Method instead.
by Kai Engelhardt. (In John Derrick, Eerke Boiten, Jim Woodcock, and
Joakim von Wright, organisers, REFINE
'02
-- An
FME
sponsored
Refinement Workshop in collaboration with BCS FACS, 23 pages,
20-21 July 2002 in Copenhagen, Denmark, 2002. This workshop was part
of FME 2002 at the Third Federated Logic Conference
FLoC '02, Copenhagen,
Denmark.)
Abstract:
We report on some progress made in a project that has as its main
goal to devise a distributed system refinement calculus with an
assertion language that can express epistemic as well as temporal
notions.
Modal Logics with a Linear Hierarchy of Local Propositional
Quantifiers
by Kai Engelhardt, Ron van der
Meyden, and Kaile Su.
(Presented at Advances in Modal Logic
2002 -- AiML
2002,
September 30 - October 2, 2002, Institut de recherche en informatique
de Toulouse Université Paul Sabatier, Toulouse, France)
Abstract:
Local propositions arise in the context of the semantics for logics
of knowledge in multi-agent systems. A proposition is local to an
agent when it depends only on that agent's local state. We consider
a logic, LLP, that extends S5, the modal logic of necessity (in
which the modality refers to truth at all worlds) by adding a
quantifier ranging over the set of all propositions and, for each
agent, a propositional quantifier ranging over the agent's local
propositions. LLP is able to express a large variety of epistemic
modalities, including knowledge, common knowledge and distributed
knowledge. However, this expressiveness comes at a cost: the logic
is equivalent to second order predicate logic when two independent
agents are present
[Engelhardt, van der Meyden and Moses,
TARK'98], hence undecidable and not
axiomatizable. This paper identifies a class of multi-agent S5
structures,
hierarchical structures, in which the agents'
information has the structure of a linear hierarchy. All systems
with just a single agent are hierarchical. It is shown that LLP
becomes decidable with respect to hierarchical systems. The main
result of the paper is the completeness of an axiomatization for the
hierarchical case.
(This paper won the best paper award. It is superseded
by 1.2.1 above.)
by Kai Engelhardt and Ron van der
Meyden. (Presented at the
FLoC'99
satellite workshop on Complexity-Theoretic and
Recursion-Theoretic Methods in Databases and Artificial
Intelligence;
June 1999.)
(This preliminary version is superseded by 1.2.1 above.)
by Kai Engelhardt and Willem-Paul de
Roever. (In John Tromp,
editor, A dynamic and quick intellect, Paul Vitányi 25 years
@ CWI, pages 59-66. CWI, Amsterdam, November 1996.)
A more elaborate version under the prosaic title
A pure, sound, and complete (in the sense of Cook) Hoare logic for a
language with specification statements and recursion.
can be obtained as gnuzipped PostScript
(32 kB) and dvi
(15 kB).
This version has some more proofs and a small example.
Model-Oriented Data Refinement
by Kai Engelhardt. (PhD thesis, Institut für Informatik und
Praktische Mathematik, Christian-Albrechts-Universität zu Kiel,
280 pages, July 1997.)
Abstract:
The goal of this thesis is to provide a comprehensive and systematic
introduction to the important and highly applicable method of data
refinement and proving simulation. We concentrate in the first part
on the general principles needed to prove data refinement correct,
and begin with an explanation of the fundamental notions, showing
that data refinement proofs reduce to proving simulation. The
topics of Hoare Logic and the Refinement Calculus are then
introduced and a general theory of simulations is developed and
related to them. Accessibility and comprehension are emphasised in
order to guide newcomers to the area. The second part of this thesis
contains a detailed survey of important methods in this area, such
as VDM, and the methods due to Abadi & Lamport, Hehner, Lynch and
Reynolds, and Back's refinement calculus. All these methods are
carefully analysed, and shown to be either incomplete, with
counterexamples to their application, or to be always applicable
whenever data refinement holds. This is shown by proving, for the
first time, that all of them can be described and analysed in terms
of two simple notions: forward and backward simulation.
Not available for download. Most printed copies of this pamphlet have
been consumed, and possibly sent to a library near you, by the
main library of Kiel University.
by Kai Engelhardt. (Master's thesis, Institut für Informatik und
Praktische Mathematik, Christian-Albrechts-Universität zu Kiel,
German title but English text, 47 pages, January 1993.)
Abstract:
By adding a new technique and a simple proof strategy to Abadi &
Lamport's 1988 method [
AL88] for proving refinement between
specifications of distributed programs correct, the inherent
limitation of their method, occurring when the abstract level of
specification features so-called infinite invisible nondeterminism
or internal discontinuity, can be sometimes overcome. This technique
is applied to the cruel last step of a three step correctness proof
for an algorithm for communication between migrating processes
within a finite network due to Kleinman, Moscowitz, Pnueli, &
Shapiro [
KMPS91].
Not available for download.
Recommendation: Get Towards a Practitioners'
Approach to Abadi and Lamport's Method instead.
Smaller Abstractions for ∀CTL* without Next
by Kai Engelhardt and Ralf
Huuck, January 2004.
Abstract:
The successful application of model-checking to large systems relies
strongly on the choice of good abstractions. In this work we present
an approach for constructing abstractions when checking Next-free
universal CTL* properties. It is known that functional
abstractions are safe and that Next-free universal CTL* is
insensitive to finite stuttering. We exploit these results by
introducing a safe Next-free abstraction which is typically
smaller that the usual functional one while at the same time more
precise, i.e., it has less spurious counter-examples.
Download a version of this paper similar to the submitted one.
(gnuzipped PostScript, 159kB)
by Kai Engelhardt and Yoram Moses, February 2005.
Abstract:
This paper addresses the problem of composing distributed programs
when communication is reliable but not necessarily FIFO. When
communication is not FIFO, special care must be taken to ensure that
messages do not accidentally overtake one another in the composed
program. We show that no program that sends or receives messages
can automatically be composed with arbitrary programs without
jeopardizing their intended behaviour. A notion of sealing is
defined, where a program P that is immediately followed by a
program Q that seals P will be communication-closed--it will
execute as if it runs in isolation. Causal precedence in the sense
of Lamport plays a central role in sealing. A characterization of
sealable programs is given, as well as efficient algorithms for
testing if Q seals P and for constructing a seal for a sealable
straight-line program P.
Download a version of this paper similar to the submitted one.
(PDF, 269kB)
by Kai Engelhardt and Yoram Moses, April 2005.
Abstract:
As part of a larger study of the problem of composing distributed
programs for asynchronous message-passing systems, we consider the
model RelDFi of FIFO channels with possible duplication but no
message loss. The basic question is when will an execution of P*Q, in which program Q is layered after P with no barriers, be
guaranteed to execute as if P ran in isolation, and then Q did.
If a message sent by one of these programs is received by the other,
it may affect and modify the other's execution. The notion of
communication-closed layers (CCLs) introduced by Elrad and Francez in 1982 is a
useful tool for studying such interference. CCLs have been
considered mainly in the context of reliable FIFO channels (without
duplication), where one can design programs P that are immune to
interference from the next layer.
When communication is less orderly, such immunity becomes elusive.
In RelDFi, for example, a terminating program that performs any
communication whatsoever cannot be immune to interference by all
possible next layers.
Using a communication phase operator, the fits after relation
among programs is defined. If program Q fits after P then P
and Q will not interfere with each other in executions of P*Q. For programs P and Q in a natural class of programs we
outline efficient algorithms for the following: (1) deciding whether
Q fits after P; (2) deciding whether Q seals P,
meaning that Q fits after P and no following program can
communicate with P; and (3) constructing a separator S
that both fits after P and satisfies that Q fits after P*S.
The programs we consider in RelDFi communicate by exchanging
tagged messages. We motivate this by proving that no protocol
exchanging only one bit messages between two processes can transmit
more than two different values (overall).
Download a version of this paper similar to the submitted one.
(PDF, 106kB)
- AL88
-
Martín Abadi and Leslie Lamport.
The existence of refinement mappings.
Technical Report 29, Digital Systems Research Center, 130 Lytton
Avenue, Palo Alto, CA 94301, August 1988.
- KMPS91
-
Alon Kleinman, Yael Moscowitz, Amir Pnueli, and Ehud Shapiro.
Communication with directed logic variables.
In Conference Record of the Eighteenth Annual ACM Symposium on
Principles of Programming Languages, pages 221-232. ACM, January 1991.
Abstracts of Publications
This document was generated using the
LaTeX2HTML translator Version 2K.1beta (1.61)
Copyright © 1993, 1994, 1995, 1996,
Nikos Drakos,
Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999,
Ross Moore,
Mathematics Department, Macquarie University, Sydney.
The command line arguments were:
latex2html -lcase_tags -no_math -html_version 4.0,math -accent_images textrm -scalable_fonts -short_index -split 0 -local_icons -nonavigation -noauto_navigation -t 'Kai Engelhardt's Publications' Ebib
The translation was initiated by Kai Engelhardt on 2005-04-04
Maintained by:
Kai Engelhardt
