Multiparty session types are designed to abstractly capture the structure of communication protocols and verify behavioural properties. One important such property is progress, i.e., the absence of deadlock. Distributed algorithms often resemble multiparty communication protocols. But proving their properties, in particular termination that is closely related to progress, can be elaborate. Since distributed algorithms are often designed to cope with faults, a first step towards using session types to verify distributed algorithms is to integrate fault-tolerance. We extend multiparty session types to cope with system failures such as unreliable communication and process crashes. Moreover, we augment the semantics of processes by failure patterns that can be used to represent system requirements (as, e.g., failure detectors). To illustrate our approach we analyse a variant of the well-known rotating coordinator algorithm by Chandra and Toueg.

We introduce a generalization of the bisimulation game that finds distinguishing Hennessy-Milner logic formulas from every finitary, subformula-closed language in van Glabbeek's linear-time--branching-time spectrum between two finite-state processes. We identify the relevant dimensions that measure expressive power to yield formulas belonging to the coarsest distinguishing behavioral preorders and equivalences; the compared processes are equivalent in each coarser behavioral equivalence from the spectrum. We prove that the induced algorithm can determine the best fit of (in)equivalences for a pair of processes.

Abstract We introduce a generalization of the bisimulation game that can be employed to find all relevant distinguishing Hennessy–Milner logic formulas for two compared finite-state processes. By measuring the use of expressive powers, we adapt the formula generation to just yield formulas belonging to the coarsest distinguishing behavioral preorders/equivalences from the linear-time–branching-time spectrum. The induced algorithm can determine the best fit of (in)equivalences for a pair of processes.

Coupled similarity is a notion of equivalence for systems with internal actions. It has outstanding applications in contexts where internal choices must transparently be distributed in time or space, for example, in process calculi encodings or in action refinements. No tractable algorithms for the computation of coupled similarity have been proposed up to now. Accordingly, there has not been any tool support. We present a game-theoretic algorithm to compute coupled similarity , running in cubic time and space with respect to the number of states in the input transition system. We show that one cannot hope for much better because deciding the coupled simulation preorder is at least as hard as deciding the weak simulation preorder. Our results are backed by an Isabelle/HOL formalization, as well as by a parallelized implementation using the Apache Flink framework. Data or code related to this paper is available at: [ 2 ].

Event Structures (ESs) address the representation of direct relationships between individual events, usually capturing the notions of causality and conflict. Up to now, such relationships have been static, i.e., they cannot change during a system run. Thus, the common ESs only model a static view on systems. We make causality dynamic by allowing causal dependencies between some events to be changed by occurrences of other events. We first model and study the case in which events may entail the removal of causal dependencies, then we consider the addition of causal dependencies, and finally we combine both approaches in the so-called Dynamic Causality ESs. For all three newly defined types of ESs, we study their expressive power in comparison to the well-known Prime ESs, Dual ESs, Extended Bundle ESs, and ESs for Resolvable Conflicts. Interestingly, Dynamic Causality ESs subsume Extended Bundle ESs and Dual ESs but are incomparable with ESs for Resolvable Conflicts.

Topological self-stabilization is the ability of a distributed system to have its nodes themselves establish a meaningful overlay network. Independent from the initial network topology, it converges to the desired topology via forwarding, inserting, and deleting links to neighboring nodes. We adapt a linearization algorithm, originally designed for a shared memory model, to asynchronous message-passing. We use an extended localized pi-calculus to model the algorithm and to formally prove its essential self-stabilization properties: closure and weak convergence for every arbitrary initial configuration, and strong convergence for restricted cases.

What does it mean that an encoding is fully abstract? What does itnotmean? In this position paper, we want to help the reader to evaluate the real benefits of using such a notion when studying the expressiveness of programming languages. Several examples and counterexamples are given. In some cases, we work at a very abstract level; in other cases, we give concrete samples taken from the field of process calculi, where the theory of expressiveness has been mostly developed in the last years.

A well-known result by Palamidessi tells us that πmix(the π-calculus with mixed choice) is more expressive than πsep(its subset with only separate choice). The proof of this result analyses their different expressive power concerning leader election in symmetric networks. Later on, Gorla offered an arguably simpler proof that, instead of leader election in symmetric networks, employed the reducibility of ‘incestual’ processes (mixed choices that include both enabled senders and receivers for the same channel) when running two copies in parallel. In both proofs, the role ofbreaking (initial) symmetriesis more or less apparent. In this paper, we shed more light on this role by re-proving the above result – based on a proper formalization of what it means to break symmetries – without referring to another problem domain like leader election. Both Palamidessi and Gorla rephrased their results by stating that there is no uniform and reasonable encoding from πmixinto πsep. We indicate how their proofs can be adapted and exhibit the consequences of varying notions of uniformity and reasonableness. In each case, the ability to break initial symmetries turns out to be essential. Moreover, by abandoning the uniformity criterion, we show that there indeed is a reasonable encoding. We emphasize its underlying principle, which highlights the difference between breaking symmetries locally instead of globally.

Given a synchronous system, we study the question whether – or, under which conditions – the behaviour of that system can be realized by a (non-trivially) distributed and hence asynchronous implementation. In this paper, we partially answer this question by examining the role of causality for the implementation of synchrony in two fundamental different formalisms of concurrency, Petri nets and the π-calculus. For both formalisms it turns out that each ‘good’ encoding of synchronous interactions using just asynchronous interactions introduces causal dependencies in the translation.

This paper introduces the Inverse Implementation method, that augments classical software development processes by a step of formal conformity verification. Our method is based on a formal model of the machine that executes programs of the chosen programming language. The model can automatically be combined with the code of a concrete program to gain a model of the execution of that program. The execution model is expressed in the same language that the program is specified in. This reduces the task of verifying the conformity of the program to finding and proving a refinement relation between two models within the same formalism. We introduce the Inverse Implementation method, show how it fits into classic software engineering processes and discuss how the choice of a suitable formalism can allow to combine manual and automated proof techniques. We further show a prototypical formalization of the Java Virtual Machine in TLA+and demonstrate how it can be used within an Inverse Implementation workflow to verify the adherence of a simple - yet multithreaded - Java program to a TLA+specification.

Protocol composition frameworks provide off-the-shelf composable protocols to simplify the development of custom protocol stacks. All recent protocol frameworks use a general-purpose event-driven model to manage the interactions between protocols. In complex compositions, where protocols offer their service to more than one other protocol, the one-to-many interaction scheme of the eventdriven model introduces composition problems by mixing up the targets to which data (list of headers) should be delivered. To solve these problems, we propose to shift the driving force behind interactions from the events to the headers they carry. We show that the resulting domain-specific header-driven model solves the composition problems, provides statically typed header handling and enhances protocol readability.