The simulation equivalence of Exercise 1.4.17 drops the symmetry of the bisimulation game: the challenge transitions may only be launched by one of the processes in the pairs. We have seen that simulation equivalence is strictly coarser than bisimilarity. Unfortunately, it does not respect deadlock. In this section we discuss a few refinements of simulation equivalence without this drawback. They are coinductively defined, much like bisimilarity, while being coarser than bisimilarity. Thus they can allow us to use coinduction in situations where bisimilarity may be over-discriminating. Another possible advantage of a simulationlike relation is that it naturally yields a preorder (with all the advantages mentioned in Section 5.5). With respect to simulation-based relations, however, bisimilarity remains mathematically more robust and natural. The most interesting refinements we examine are represented by ready similarity and coupled similarity.

We begin in Section 6.1 with complete simulation, and continue in Section 6.2 with ready simulation. They are to simulation what complete trace equivalence and failure (or ready) equivalence are to trace equivalence. In Section 6.3 we discuss two-nested simulation equivalence. In Section 6.4 we consider the weak versions of the relations in the previous sections. In Section 6.5 we present coupled similarity, which aims at relaxing the bisimulation requirements on the internal actions of processes. Finally, in Section 6.6, we summarise the various equivalences discussed in this and previous chapters.

Complete simulation

The arguments about the deadlock-insensitivity of trace equivalence in Section 1.3.2, such as the equality between the processes in Figure 1.4, apply to simulation equivalence too.

In the first part of this chapter we present (yet) another characterisation of bisimilarity, namely bisimilarity as a testing equivalence. In a testing scenario two processes are equivalent if no experiment can distinguish them. An experiment on a process is set up by defining a test, that is, intuitively, a pattern of demands on the process (e.g., the ability of performing a certain sequence of actions, or the inability of performing certain actions). Depending on how the process behaves when such a test is conducted, the observer emits a verdict about the success or failure of the experiment. The experiments are means of understanding how the processes react to stimuli from the environment. A testing scenario has two important parameters.

1. How are observations about the behaviour of a process gathered? In other words, what can the observer conducting the experiment do on a process? For instance, is he/she allowed to observe the inability of a process to perform certain actions? Is he/she allowed to observe whether a process can immediately perform two distinct actions? Is he/she allowed to make a copy of a process? These decisions are embodied in the language for the tests.

2. How is the success or the failure of an experiment determined?

The choice for these parameters has an impact on the distinctions that can be made on the processes. We will set up a testing scenario whose induced equivalence is precisely bisimilarity.

Introduction

Algebra is a well-established part of mathematics, dealing with sets with operations satisfying certain properties, like groups, rings, vector spaces, etc. Its results are essential throughout mathematics and other sciences. Universal algebra is a part of algebra in which algebraic structures are studied at a high level of abstraction and in which general notions like homomorphism, subalgebra, congruence are studied in themselves, see e.g. [Coh81, MT92, Wec92]. A further step up the abstraction ladder is taken when one studies algebra with the notions and tools from category theory. This approach leads to a particularly concise notion of what is an algebra (for a functor or for a monad), see for example [Man74]. The conceptual world that we are about to enter owes much to this categorical view, but it also takes inspiration from universal algebra, see e.g. [Rut00].

In general terms, a program in some programming language manipulates data. During the development of computer science over the past few decades it became clear that an abstract description of these data is desirable, for example to ensure that one's program does not depend on the particular representation of the data on which it operates. Also, such abstractness facilitates correctness proofs. This desire led to the use of algebraic methods in computer science, in a branch called algebraic specification or abstract data type theory. The objects of study are data types in themselves, using notions and techniques which are familiar from algebra.

In this chapter we introduce some common process operators, which impose a structure on processes and bring in concepts from algebra. The operators we consider are inspired by those of the Calculus of Communicating Systems (CCS) [Mil89, AILS07], one of the most studied process calculi. Given a process calculus (or a language), one obtains an LTS by providing, for each operator, a set of inference rules that determine the possible transitions of the processes in the syntax-driven fashion of Plotkin's Structured Operational Semantics (SOS) [Plo04a, Plo04b]. We restrain from going into a thorough discussion on process calculi. We do present, however, nearly all the operators of CCS. What here, and in the following chapters, is called CCS is in fact very close to the standard presentation as in, e.g., [Mil89, AILS07]. The only technical differences are that we do not introduce the relabelling operator, and, for writing processes with an infinite behaviour, we use constant symbols instead of recursive process equations; each constant comes with its own transitions. These differences are discussed in Remark 3.5.8 and following exercises, and Remark 3.2.3.

The chapter offers a number of examples of the bisimulation proof method. The method is used to prove that bisimilarity is preserved by the operators considered (and that therefore it is a congruence in CCS), to prove some basic algebraic laws, and in various examples.

Why bisimulation and coinduction

Induction is a pervasive tool in Computer Science and Mathematics for defining objects and proving properties of them. Coinduction is less known. It has been discovered and studied only in recent years. It is therefore not part of the standard scientific culture. The interest in coinduction is, however, growing: more and more application areas are suggested, and with compelling evidence.

Coinduction brings in tools for defining and reasoning on objects that are new and quite different from the tools provided by induction. This is because coinduction is the dual of induction. Induction has to do with least fixed points, coinduction with greatest fixed points. Greatest fixed points are as natural as least fixed points; in the same way coinduction is as natural as induction.

In the world of induction, constructions are stratified. Objects are hereditarily constructed, starting from basic atoms or primitive objects at the bottom, and then iteratively moving upward through higher or composite objects. Coinduction liberates us from the constraints of stratification. An immediate consequence is that the objects can be circular; more generally, they can be infinite. Examples of infinite structures are streams, as infinite sequences of elements, and real numbers, as infinite digit streams or Cauchy sequences. Another example is a process that continuously accepts interactions with the environment: semantically it is an infinite object, as it can engage in an infinite number of interactions.

One of the main reasons for the success of bisimilarity is the strength of the associated proof method. We discuss here the method on processes, more precisely, on Labelled Transition Systems (LTSs). However the reader should bear in mind that the bisimulation concept has applications in many areas beyond concurrency [San12]. According to the proof method, to establish that two processes are bisimilar it suffices to find a relation on processes that contains the given pair and that is a bisimulation. Being a bisimulation means that related processes can match each other's transitions so that the derivatives are again related.

In general, when two processes are bisimilar there may be many relations containing the pair, including the bisimilarity relation, defined as the union of all bisimulations. However, the amount of work needed to prove that a relation is a bisimulation depends on its size, since there are transition diagrams to check for each pair. It is therefore important to use relations as small as possible.

In this chapter we show that the bisimulation proof method can be enhanced, by employing relations called ‘bisimulations up to’. These relations need not be bisimulations; they are just contained in a bisimulation. The proof that a relation is a ‘bisimulation up to’ follows diagram-chasing arguments similar to those in bisimulation proofs. The reason why ‘bisimulations up to’ are interesting is that they can be substantially smaller than any enclosing bisimulation; hence they may entail much less work in proofs.

Introduction

In this chapter,we look at the origins of bisimulation.We showthat bisimulation has been discovered not only in computer science, but also – and roughly at the same time – in other fields: philosophical logic (more precisely, modal logic), and set theory. In each field, we discuss the main steps that led to the discovery, and introduce the people who made these steps possible.

In computer science, philosophical logic, and set theory, bisimulation has been derived through refinements of notions of morphism between algebraic structures. Roughly, morphisms are maps (i.e. functions) that are ‘structurepreserving’. The notion is therefore fundamental in all mathematical theories in which the objects of study have some kind of structure, or algebra. The most basic forms of morphism are the homomorphisms. These essentially give us a way of embedding a structure (the source) into another one (the target), so that all the relations in the source are present in the target. The converse, however, need not be true; for this, stronger notions of morphism are needed. One such notion is isomorphism, which is, however, extremely strong – isomorphic structures must be essentially the same, i.e. ‘algebraically identical’. It is a quest for notions in between homomorphism and isomorphism that led to the discovery of bisimulation.

The kind of structures studied in computer science, philosophical logic, and set theory were forms of rooted directed graphs.

Introduction

A model for reactive computation, for example that of labelled transition systems [Kel76], or a process algebra (such asACP [BW90], CCS [Mil89], CSP [Hoa85]) can be used to describe both implementations of processes and specifications of their expected behaviours. Process algebras and labelled transition systems therefore naturally support the so-called single-language approach to process theory, that is, the approach in which a single language is used to describe both actual processes and their specifications. An important ingredient of the theory of these languages and their associated semantic models is therefore a notion of behavioural equivalence or behavioural approximation between processes. One process description, say SYS, may describe an implementation, and another, say SPEC, may describe a specification of the expected behaviour. To say that SYS and SPEC are equivalent is taken to indicate that these two processes describe essentially the same behaviour, albeit possibly at different levels of abstraction or refinement. To say that, in some formal sense, SYS is an approximation of SPEC means roughly that every aspect of the behaviour of this process is allowed by the specification SPEC, and thus that nothing unexpected can happen in the behaviour of SYS. This approach to program verification is also sometimes called implementation verification or equivalence checking.

Designers using implementation verification to validate their (models of) reactive systems need only learn one language to describe both their systems and their specifications, and can benefit from the intrinsic compositionality of their descriptions, at least when they are using a process algebra for denoting the labelled transition systems in their models and an equivalence (or preorder) that is preserved by the operations in the algebra.

After introducing bisimulation on processes in the previous chapter, we see here other examples of predicates and relations that are defined in a similar style, and proof techniques for them. This style is quite different with respect to that of ordinary inductive definitions and proofs. It is in fact the style of coinduction. Through the examples we will begin to build up some intuition about the difference between coinduction and induction. Then we will make these intuitions formal, using fixed-point theory.

Intuitively, a set A is defined coinductively if it is the greatest solution of an inequation of a certain form; then the coinduction proof principle just says that any set that is solution of the same inequation is contained in A. Dually, a set A is defined inductively if it is the least solution of an inequation of a certain form, and the induction proof principle then says that any other set that is solution to the same inequation contains A. As we will see, familiar inductive definitions and proofs can be formalised in this way.

An abstract formalisation of the meaning of coinduction is not necessary for applications. In the previous chapter, for instance, we have seen that bisimulation can be defined on processes without talking about fixed points. But the theory of fixed points allows us to understand what we are doing, and to understand the analogies among different worlds.