In the crash-recovery failure model of asynchronous distributed systems, processes can temporarily stop to execute steps and later restart their computation from a predefined local state. The crash-recovery model is much more realistic than the crash-stop failure model in which processes merely are allowed to stop executing steps. The additional complexity is reflected in the multitude of assumptions and the technical complexity of algorithms which have been developed for that model. We focus on the problem of consensus in the crash-recovery model, but instead of developing completely new algorithms from scratch, our approach aims at re-using existing crash-stop consensus algorithms in a modular way using the abstraction of failure detectors. As a result, we present three new consensus algorithms for the crash-recovery model for different types of assumptions.

We present a compositional analysis of deadlock-freedom in component systems with multiway cooperation. We require the systems to satisfy architectural constraints which make sure that the communication structure between the components is given by a tree. Only pairs of components have to be examined for the analysis, therefore the cost is polynomial in the size of the input.

We study architectural constraints for component systems in order to be able to guarantee safety-properties. Representing safety-properties, we investigate deadlock-freedom. We present a compositional and hence polynomial time condition for deadlock-freedom for a class of component-systems whose architecture is tree-like. The architectural constraints that are developed can be understood as a design pattern that helps to construct systems satisfying safety-properties on the one hand. On the other hand, they might help to draw attention to potentially critical situations in a design. To model component-systems we use the formalism of interaction systems as proposed by Sifakis et al. The ideas can be transferred to other formal models where subsystems are cooperating via synchronous communication.

Abstract In modular approaches to specify concurrent systems a system is built up from components using various operators as e.g. the sequential, the parallel, or the choice (+) operator. Usually the choice between two components, i.e. P 1 + P 2 , is taken in favor of that component that is first to start an action. We follow here the alternative view that a choice is taken in favor of that component that is the first to terminate an action (end-based choice). This alternative has various applications and interesting implications. In particular the different points of view lead to different action refinement operators. The contribution of this paper is to present here an action refinement operator for the end-based view in a suitable true concurrency setting and to establish two equivalences that are the coarsest congruences for this refinement operator with respect to trace (respectively bisimulation) equivalence.

Action refinement is an essential operation in the design of concurrent systems, real-time or not. In this paper, we develop an action refinement technique in a real-time non-interleaving causality-based setting, a timed extension of bundle event structures that allows for urgent interactions to model time-out. A syntactic action refinement operation is presented in a timed process algebra based on the internationally standardised specification language LOTOS. We show: (1) that the behavior of the refined system can be inferred compositionally from the behavior of the original system; (2) from the behaviors of the processes substituted for actions with explicitly represented start-points, that the timed versions of a linear-time equivalence (pomset trace equivalence) and a branching-time equivalence (history-preserving bisimulation equivalence) are both congruences under our refinement; and (3) that the syntactic and semantic action refinements we developed coincide under these equivalence notions with respect to a metric and a CPO (complete partial order) based denotational semantics. Therefore, our refinement operations behave well. They also meet the commonly expected properties.

Abstract The purpose of this paper is twofold: First, we show in which way the initial solution of a domain equation for cpo's and the unique solution of a corresponding domain equation for metric spaces are related. Second, we present a technique to lift a given domain equation for cpo's to a corresponding domain equation for metric spaces.

It is meaningful that a language is provided with several semantic descriptions: e.g. one which serves the needs of the implementor, another one that is suitable for specification and yet another one that will be used to explain the language to the user. In this case one has to guarantee that the various semantics are ‘consistent’. The attempt of this paper is to clarify the notion ‘consistency’ and to present a general framework and theorems for consistency results.

This paper presents an on-line algorithm for the construction of position trees, i.e., an algorithm which constructs the position tree for a given string while reading the string from left to right. In addition, an on-line correction algorithm is presented which—upon a change in the string—can be used to construct the new position tree. Moreover, special attention is paid to computers with small memory. compactification of the trees and transport costs between main and secondary storage are discussed.