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.

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.

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.

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.

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.

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.

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.

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(n²) channels can be sealed using O(n) messages.

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.

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.

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.

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.

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

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.

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.

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.

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