Abstracts of Publications by Kai Engelhardt


Contents

1 Book(s)
 1.1 Data refinement book
   Reviews
2 Book Chapters
 2.1 Smaller Abstractions for CTL* without Next
 2.2 Modal Logics with a Linear Hierarchy of Local Propositional Quantifiers
3 Journal Articles
 3.1 Causing Communication Closure: Safe Program Composition with Reliable Non-FIFO Channels
 3.2 Single-bit messages are insufficient for data link over duplicating channels
 3.3 Towards a Practitioners’ Approach to Abadi and Lamport’s Method
4 Conference Papers
 4.1 seL4: Formal Verification of an OS Kernel
 4.2 Model checking knowledge and linear time: PSPACE cases
 4.3 Safe Composition of Distributed Programs Communicating over Order-Preserving Imperfect Channels
 4.4 Single-Bit Messages are Insufficient in the Presence of Duplication
 4.5 Causing Communication Closure: Safe Program Composition with Non-FIFO Channels
 4.6 A Refinement Theory that Supports Reasoning about Knowledge and Time for Synchronous Agents
 4.7 A Program Refinement Framework Supporting Reasoning about Knowledge and Time
 4.8 Knowledge and the Logic of Local Propositions
 4.9 Simulation of Specification Statements in Hoare Logic
 4.10 Generalizing Abadi & Lamport’s Method to Solve a Problem Posed by A. Pnueli
5 Invited Talk(s)
 5.1 Towards a Refinement Theory that Supports Reasoning about Knowledge and Time for Multiple Agents (Work in Progress)
6 Refereed Workshop Papers
 6.1 Modal Logics with a Linear Hierarchy of Local Propositional Quantifiers
 6.2 Modal Logics with a Hierarchy of Local Propositional Quantifiers (Extended Abstract)
7 Miscellaneous
 7.1 New Wine
d for Old Bags
8 Theses
 8.1 Dissertation
 8.2 Diploma thesis

For referring to the publications from within LATEX, download the .bib-file (10 kB, depends on string definitions)

1 Book(s)

1.1 Data Refinement: Model-Oriented Proof Methods and their Comparison

small picture of an earlier cover sketch

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, hardcover: 1998, paperback: 2009.

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.

Reviews

2 Book Chapters

2.1 Smaller Abstractions for CTL* without Next

by Kai Engelhardt and Ralf Huuck (to appear in Dennis Dams, Ulrich Hannemann, and Martin Steffen, editors, Festschrift Dedicated to Willem-Paul de Roever, LNCS, Springer-Verlag).

The success of applying model-checking to large systems depends crucially 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 that is typically smaller than the usual functional one while at the same time more precise, i.e., it has less spurious counter-examples.

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

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)

3 Journal Articles

3.1 Causing Communication Closure: Safe Program Composition with Reliable Non-FIFO Channels

by Kai Engelhardt and Yoram Moses. (Distributed Computing, 22(2):73–91, ©Springer-Verlag, October 2009.)

A rigorous framework for analyzing safe composition of distributed programs is presented. It facilitates specifying notions of safe sequential execution of distributed programs in various models of communication. A notion of sealing is defined, where if a program P is immediately followed by a program Q that seals P then P will be communication-closed—it will execute as if it runs in isolation. None of its send or receive actions will match or interact with actions outside P.

The applicability of sealing is illustrated by a study of program composition when communication is reliable but not necessarily FIFO. In this model, special care must be taken to ensure that messages do not accidentally overtake one another in the composed program. In this model no program that sends or receives messages can be composed automatically with arbitrary programs without jeopardizing their intended behavior. Safety of composition becomes context-sensitive and new tools are needed for ensuring it. The investigation of sealing in this model reveals a novel connection between Lamport causality and safe composition. 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 class of straight-line programs. It is shown that every sealable program can be sealed using O(n) messages. In fact, 3n - 4 messages are necessary and sufficient in the worst case, despite the fact that a sealable program may be open to interference on Ω(n2) channels.

3.2 Single-bit messages are insufficient for data link over duplicating channels

by Kai Engelhardt and Yoram Moses. (Information Processing Letters 107(6):235–239, Elsevier BV, August 2008.)

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

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)

4 Conference Papers

published (or to appear) in refereed proceedings.

4.1 seL4: Formal Verification of an OS Kernel

by Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. (To appear in Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP), Big Sky, MT, USA, October 2009, ACM.)

Complete formal verification is the only known way to guarantee that a system is free of programming errors.

We present our experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation. We assume correctness of compiler, assembly code, and hardware, and we used a unique design approach that fuses formal and operating systems techniques. To our knowledge, this is the first formal proof of functional correctness of a complete, general-purpose operating-system kernel. Functional correctness means here that the implementation always strictly follows our high-level abstract specification of kernel behaviour. This encompasses traditional design and implementation safety properties such as the kernel will never crash, and it will never perform an unsafe operation. It also proves much more: we can predict precisely how the kernel will behave in every possible situation.

seL4, a third-generation microkernel of L4 provenance, comprises 8,700 lines of C code and 600 lines of assembler. Its performance is comparable to other high-performance L4 kernels.

At the conference site, the paper is available for download: HTTP .pdf, 412kB.

4.2 Model checking knowledge and linear time: PSPACE cases

by Kai Engelhardt, Peter Gammie, and Ron van der Meyden. (Anil Nerode and Sergei Artëmov, editors, Logical Foundations of Computer Science, volume 4515 of LNCS, pages 195–211, ©Springer-Verlag, 2007.)

Modal logics of knowledge have been proposed as a formalism for information flow properties in distributed and multi-agent systems. Model checking the logic of knowledge and linear time with respect to a perfect recall interpretation of knowledge is known to be decidable, but of non-elementary complexity, and undecidable once common knowledge operators are added to the language. The paper presents a general algorithm scheme for model checking logics of knowledge, common knowledge and linear time, based on simulations to a class of structures that capture the way that agents update their knowledge. It is shown that the scheme leads to PSPACE implementations of model checking the logic of knowledge and linear time in several special cases: perfect recall systems with a single agent or in which all communication is by synchronous broadcast, and systems in which knowledge is interpreted using either the agents’ current observation only or its current observation and clock value. In all these results, common knowledge operators may be included in the language. Matching lower bounds are provided, and it is shown that although the complexity bound matches the PSPACE complexity of the linear time temporal logic LTL, as a function of the model size the problems considered have a higher complexity than LTL.

4.3 Safe Composition of Distributed Programs Communicating over Order-Preserving Imperfect Channels

by Kai Engelhardt and Yoram Moses. (To appear in: Ajit Pal, Ajay Kshemkalyani, Rajeev Kumar, and Arobinda Gupta, editors, 7th International Workshop on Distributed Computing IWDC 2005, volume 3741 of LNCS, pages 32–44, ©Springer-Verlag, December 2005.)

The fundamental question considered in this paper is when program Q, if executed immediately after program P, is guaranteed not to interfere with P and be safe from interference by P. 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 layers that do not interfere with any other layer. When channels are less than perfect such programs are no longer feasible. The absence of interference between layers becomes context-dependent. In this paper we study the impact of message duplication and loss on the safety of layer composition. 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.

Download a fuller version of the paper. It contains proof sketches for the main results. (FTP .pdf, 102kB, HTTP .pdf, 102kB)

4.4 Single-Bit Messages are Insufficient in the Presence of Duplication

by Kai Engelhardt and Yoram Moses. (To appear in: Ajit Pal, Ajay Kshemkalyani, Rajeev Kumar, and Arobinda Gupta, editors, 7th International Workshop on Distributed Computing IWDC 2005, volume 3741 of LNCS, pages 25–31, ©Springer-Verlag, December 2005.)

Ideal communication channels in asynchronous systems are reliable, deliver messages in FIFO order, and do not deliver spurious or duplicate messages. A message vocabulary of size two (i.e., single-bit messages) suffices to encode and transmit messages of arbitrary finite length over such channels. This note proves that single-bit messages are insufficient once channels potentially deliver duplicate messages. In particular, it is shown that no protocol allows the sender to notify the receiver which of three values it holds, over a bidirectional, reliable, FIFO channel that may duplicate messages. This implies that messages must encode some additional control information, e.g., in the form of headers or tags.

Download a version of this paper similar to the submitted one. (PDF, 71kB)

4.5 Causing Communication Closure: Safe Program Composition with Non-FIFO Channels

by Kai Engelhardt and Yoram Moses. (To appear in: Pierre Fraigniaud, editor, DISC 2005 19th International Symposium on Distributed Computing, volume 3724 of LNCS, pages 229–243, ©Springer-Verlag, September 2005.)

A semantic framework for analyzing safe composition of distributed programs is presented. Its applicability is illustrated by a study of program composition when communication is reliable but not necessarily FIFO. In this model, special care must be taken to ensure that messages do not accidentally overtake one another in the composed program. We show that barriers do not exist in this model. Indeed, no program that sends or receives messages can automatically be composed with arbitrary programs without jeopardizing their intended behavior. Safety of composition becomes context-sensitive and new tools are needed for ensuring it. A notion of sealing is defined, where if a program P is immediately followed by a program Q that seals P then P will be communication-closed—it will execute as if it runs in isolation. The investigation of sealing in this model reveals a novel connection between Lamport causality and safe composition. 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 significant class of programs. It is shown that every sealable program that is open to interference on O(n2) channels can be sealed using O(n) messages.

Download a version of this paper similar to the submitted one. (PDF, 335kB)

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

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)

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

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)

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

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)

4.9 Simulation of Specification Statements in Hoare Logic

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

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)

4.10 Generalizing Abadi & Lamport’s Method to Solve a Problem Posed by A. Pnueli

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

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

Download a version of this paper similar to the published one. (gnuzipped PostScript, 85kB)

Recommendation: Get 3.3 instead.

5 Invited Talk(s)

5.1 Towards a Refinement Theory that Supports Reasoning about Knowledge and Time for Multiple Agents (Work in Progress)

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

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.

6 Refereed Workshop Papers

6.1 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)

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 2.2 above.)

6.2 Modal Logics with a Hierarchy of Local Propositional Quantifiers (Extended Abstract)

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 2.2 above.)

7 Miscellaneous

7.1 New Wine
d for Old Bags

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.

8 Theses

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

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.

8.2 Verallgemeinerungen der Methode von Abadi und Lamport um ein von A. Pnueli gestelltes Problem zu lösen

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

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

References

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

Id: pubs.tex,v 1.2 2009/04/14 07:55:16 kaie Exp kaie