Divergence-Preserving Branching Bisimilarity

Branching bisimilarity was proposed by van Glabbeek and Weijland as an upgrade of (strong) bisimilarity that facilitates abstraction from internal activity [17]. It preserves the branching structure of processes more strictly than Milner’s observation equivalence [22], which, according to van Glabbeek and Weijland, makes it, e.g., better suited for verification purposes. A case in point is the argument by Graf and Sifakis that there is no temporal logic with an eventually operator that is adequate for observation equivalence in the sense that two processes satisfy the same formulas if, and only if, they are observationally equivalent [18]. The crux is that observation equivalence insufficiently takes into account the intermediate states of an internal computation. Indeed, branching bisimilarity requires a stronger correspondence between the intermediate states of an internal computation.

Branching bisimilarity is also not compatible with a temporal logic that includes an eventually operator, because it abstracts to some extent from divergence (i.e., infinite internal computations). Thus, a further upgrade is necessary, removing the abstraction from divergence. De Nicola and Vaandrager show that divergence-sensitive branching bisimilarity coincides with the equivalence induced by satisfaction of formulas of the temporal logic CTL${}^{*}_{\_}{-X}$ [7]. (CTL^∗ [9] is an expressive state-based logic that includes both linear time and branching time modalities; CTL${}^{*}_{\_}{-X}$ refers to the variant of CTL^∗ obtained by omitting the next-state modality, which is incompatible with abstraction from internal activity.)

Divergence-sensitive branching bisimilarity still has one drawback when it comes to verification: it identifies deadlock and livelock and, as an immediate consequence, is not compatible with parallel composition. It turns out that the notion of divergence-preserving branching bisimilarity¹¹1For stylistic reasons we prefer the term “divergence-preserving branching bisimilarity” over “branching bisimilarity with explicit divergence”, which is used in earlier articles on the topic., which is the topic of this note, has all the right properties: it is the coarsest equivalence that is compatible with parallel composition, preserves CTL${}^{*}_{\_}{-X}$ formulas, and distinguishes deadlock and livelock [16]. Moreover, on finite processes divergence-preserving branching bisimilarity can be decided efficiently [19].

In [17], a coloured-trace characterisation of divergence-preserving branching bisimilarity is provided. In [14], relational and modal characterisations of the notion are given. For some time it was simply assumed that these three characterisations of the notion coincide, but this was only proved in [15]. To establish that the relational characterisation coincides with the coloured-trace and modal characterisations, it needs to be proved that the relational characterisation yields an equivalence relation that satisfies the so-called stuttering property, and this is surprisingly involved. A similar phenomenon is observed in the proof that a rooted version of divergence-preserving branching bisimilarity is compatible with the recursion construct $\mu X.\_$ [13]. Due to the divergence condition, Milner’s ingenious argument in [24] that strong bisimilarity is compatible with recursion required several novel twists.

In this note we shall give a survey of results pertaining to divergence-preserving branching bisimilarity that were obtained in the past one-and-a-half decade. in Section 2 we shall present and discuss a relational characterisation of the notion. In Section 3 we comment on modal characterisations of the notion, and discuss the relationship with the temporal logic CTL${}^{*}_{\_}{-X}$. In Section 4 we briefly discuss to what extent the notion is compatible with familiar process algebraic operators. In Section 5, we explain how it plays a role in expressiveness results. In Section 6 we arrive at some conclusions and mention some ideas for future work.

We presuppose a set ${\mathcal{A}{}_{{\tau}}}$ of actions including a special element ${\tau}$, and we presuppose a labelled transition system $({S},{\longrightarrow})$ with labels from ${\mathcal{A}{}_{{\tau}}}$, i.e., ${S}$ is a set of states and ${\longrightarrow}\subseteq{S}\times{\mathcal{A}{}_{{\tau}}}\times{S}$ is a transition relation on ${S}$. Let ${s},{s^{\prime}}\in{S}$ and ${\alpha}\in{\mathcal{A}{}_{{\tau}}}$; we write ${s}\overset{{\alpha}}{\longrightarrow}{s^{\prime}}$ for $({s},{\alpha},{s^{\prime}})\in{\longrightarrow}$ and we abbreviate the statement ‘${s}\overset{{\alpha}}{\longrightarrow}{s^{\prime}}$ or (${\alpha}={\tau}$ and ${s}={s^{\prime}}$)’ by ${s}\overset{\mbox{\tiny\rm(}{\alpha}\mbox{\tiny\rm)}}{\longrightarrow}{s^{\prime}}$. We denote by $\mathbin{\rightarrow^{+}}$ the transitive closure of the binary relation $\overset{{\tau}}{\longrightarrow}$, and by $\mathbin{\twoheadrightarrow}$ its reflexive-transitive closure. A process is given by a state $s$ in a labelled transition system, and encompasses all the states and transitions reachable from $s$.

The divergence condition (D) in the definition above is slightly weaker than the divergence condition used in the relation characterisation of divergence-preserving branching bisimilarity presented in [14], which actually requires that ${t}$ admits an infinite sequence of ${\tau}$-transitions and every state on this sequence is related to some state on the infinite sequence of ${\tau}$-transitions from ${s}$. Nevertheless, as is established in [15], the notion of divergence-preserving branching bisimilarity defined here is equivalent to the one defined in [14]. In [15] it is also proved that $\mathrel{\hbox{\kern 0.43057pt\vbox{\hbox{\raise 0.43057pt\hbox{\kern-0.43057pt{$\leftrightarrow$}\kern-0.43057pt}}\hrule}\kern 0.43057pt}^{\Delta}_{b}}$ is an equivalence, that the relation $\mathrel{\hbox{\kern 0.43057pt\vbox{\hbox{\raise 0.43057pt\hbox{\kern-0.43057pt{$\leftrightarrow$}\kern-0.43057pt}}\hrule}\kern 0.43057pt}^{\Delta}_{b}}$ is itself a divergence-preserving branching bisimulation, and that it satisfies the so-called stuttering property: if ${t_{0}}\overset{{\tau}}{\longrightarrow}\cdots{t_{n}}$, ${s}\mathrel{\hbox{\kern 0.43057pt\vbox{\hbox{\raise 0.43057pt\hbox{\kern-0.43057pt{$\leftrightarrow$}\kern-0.43057pt}}\hrule}\kern 0.43057pt}^{\Delta}_{b}}{t_{0}}$ and ${s}\mathrel{\hbox{\kern 0.43057pt\vbox{\hbox{\raise 0.43057pt\hbox{\kern-0.43057pt{$\leftrightarrow$}\kern-0.43057pt}}\hrule}\kern 0.43057pt}^{\Delta}_{b}}{t_{n}}$, then ${s}\mathrel{\hbox{\kern 0.43057pt\vbox{\hbox{\raise 0.43057pt\hbox{\kern-0.43057pt{$\leftrightarrow$}\kern-0.43057pt}}\hrule}\kern 0.43057pt}^{\Delta}_{b}}{t_{i}}$ for all $0\leq i\leq n$.

Let us say that a state ${s}$ is divergent if there exists an infinite sequence of states $({s_{k}})_{\_}{k\in{\omega}}$ such that ${s}={s_{0}}$ and ${s_{k}}\overset{{\tau}}{\longrightarrow}{s_{k+1}}$ for all $k\in{\omega}$. It is a straightforward consequence of the definition that divergence-preserving branching bisimilarity relates divergent states to divergent states only, i.e., that we have the following proposition.

As the following example illustrates, however, a symmetric binary relation on ${S}$ relating states that satisfies (T) of Definition 1 and relates divergent states to divergent states only is not necessarily included in a divergence-preserving branching bisimulation relation. In other words, a symmetric binary relation on ${S}$ that satisfies (T) and only relates divergent states to divergent states may relate states that are not divergence-preserving branching bisimilar.

As shown in [14], to get an (action-based) modal logic that is adequate for branching bisimilarity one could take an adaptation of standard Hennessy-Milner logic replacing, for all actions ${\alpha}\in{\mathcal{A}{}_{{\tau}}}$ in the usual unary may and must modalities $\langle{a}\rangle$ and $[{a}]$ by a binary just-before modality $\mathbin{{a}}$. A state ${s}$ satisfies the formula $\varphi\mathbin{{a}}\psi$ if, and only if, there exist states ${s}^{\prime\prime}$ and ${s}^{\prime}$ such that ${s}\mathbin{{\buildrel\over{\hbox to16.11119pt{$\smash{-missing}\mkern-7.0mu\cleaders\hbox{$\mkern-2.0mu\smash{-missing}\mkern-2.0mu$}\hfill\mkern-7.0mu\mathord{\twoheadrightarrow}$}}}}{s}^{\prime\prime}\overset{\mbox{\tiny\rm(}{\alpha}\mbox{\tiny\rm)}}{\longrightarrow}{s}^{\prime}$, $\varphi$ holds in ${s}^{\prime\prime}$ and $\psi$ holds in ${s}^{\prime}$. To get an adequate logic for divergence-preserving branching bisimilarity, it suffices to add a unary divergence modality ${\Delta}{}$ such that ${s}$ satisfies ${\Delta}{\varphi}$ if, and only if, there exists an infinite sequence of states $({s_{k}})_{\_}{k\in{\omega}}$ such that ${s}\mathbin{{\buildrel\over{\hbox to16.11119pt{$\smash{-missing}\mkern-7.0mu\cleaders\hbox{$\mkern-2.0mu\smash{-missing}\mkern-2.0mu$}\hfill\mkern-7.0mu\mathord{\twoheadrightarrow}$}}}}{s_{0}}$, ${s_{k}}\overset{{\tau}}{\longrightarrow}{s_{k+1}}$ and $\varphi$ holds in ${s_{k}}$ for all $k\in{\omega}$.

Let $\Phi$ be the class of formulas generated by the following grammar:

We then have that states ${s}$ and ${t}$ are divergence-proving branching bisimilar if, and only if, ${s}$ and ${t}$ satisfy exactly the same formula in $\Phi$ [15]. We may restrict the cardinality of $\Phi^{\prime}$ in conjunctions to the cardinality of the set of states ${S}$.

There is also an intuitive correspondence between branching bisimilarity and the state-based temporal logic CTL${}^{*}_{\_}{-X}$ (CTL^∗ without the next-state modality) [8]. The standard semantics of CTL${}^{*}_{\_}{-X}$ is, however, with respect to Kripke structures, in which states rather than transitions have labels and the transition relation is assumed to be total. To formalise the correspondence, De Nicola and Vaandrager devised a framework of translations between labelled transition systems and Kripke structures [7]. The main idea of the translation from labelled transition systems to Kripke structures is that

1. 1.

   every transition ${s}\overset{{a}}{\longrightarrow}{t}$ (${a}\neq{\tau}$) is replaced by two transitions ${s}\overset{}{\longrightarrow}{t}_{\_}{{a}}$ and ${t}_{\_}{{a}}\overset{}{\longrightarrow}{t}$, where $t_{\_}{{a}}$ is a fresh state that is labelled with $\{{a}\}$;

2. 2.

   every transition ${s}\overset{{\tau}}{\longrightarrow}{t}$ gives rise to a transition ${s}\overset{}{\longrightarrow}{t}$; and

3. 3.

   for every state ${s}$ without outgoing transitions (i.e., every deadlock state of the labelled transition system) a transition ${s}\overset{}{\longrightarrow}{s}$ is added to satisfy the totality requirement of Kripke structures.

De Nicola and Vaandrager propose a notion of divergence-sensitive branching bisimilarity on finite LTSs and establish that two states in an LTS are divergence-sensitive branching bisimilar if, and only if, in the Kripke resulting from the translation sketched above they satisfy the same CTL${}^{*}_{\_}{-X}$ formulas. Divergence-sensitive branching bisimilarity coincides with divergence-preserving branching bisimilarity on deadlock-free LTSs. In fact, the only difference between divergence-sensitive branching bisimilarity and divergence-preserving branching bisimilarity is that the latter distinguishes between deadlock and livelock states, whereas the former does not.

To preserve the distinction between deadlock and livelock, a modified translation is proposed in [16], obtained from the translation sketched above by replacing clause 3 by

1. 3^′.

   add a fresh state $d$ labelled with $\{\delta\}$, and for every state ${s}$ without outgoing transitions a transition ${s}\overset{}{\longrightarrow}d$.

Two states in a labelled transition system are divergence-preserving branching bisimilar if they satisfy the same CTL${}^{*}_{\_}{-X}$ formulas in the Kripke structure that results from the modified transition [16].

An important reason to prefer divergence-preserving branching bisimilarity over divergence-sensitive branching bisimilarity is that the former is compatible with parallel composition, whereas the latter is not.

Divergence-preserving branching bisimilarity is the coarsest equivalence included in divergence-sensitive branching bisimilarity that is compatible with parallel composition [16]. Hence, it is also the coarsest congruence for parallel composition relating only processes that satisfy the same CTL${}^{*}_{\_}{-X}$ formulas.

It is well-known that branching bisimilarity is not compatible with non-deterministic choice, and that the coarsest behavioural equivalence that is included in branching bisimilarity and that is compatible with non-deterministic choice, is obtained by adding a so-called root condition. The same holds for divergence-preserving branching bisimilarity.

In [12], formats for transition system specifications are presented that guarantee that divergence-preserving branching bisimilarity and its rooted variant are compatible with the operators defined by the transition system specification. These formats relax the requirements of the branching bisimulation and rooted branching bisimulation formats of [11]. The relaxation of the formats is meaningful: the process-algebraic operations for priority [2] and sequencing [6, 5, 4], with which (rooted) branching bisimilarity is not compatible, are in the rooted divergence-preserving branching bisimulation format. So, in contrast to its divergence-insensitive variant, rooted divergence-preserving branching bisimilarity is compatible with priority and sequencing.

The structural operational rule for the recursion operator $\mu X.\_$, which was considered in the context of observation equivalence by Milner [23] and in the context of divergence-sensitive variants of observation equivalence by Lohrey, D’Argenio and Hermanns [20], is not in the format for rooted divergence-preserving branching bisimilarity. Nevertheless, rooted divergence preserving branching bisimilarity is compatible also with this operator [13]. The proof of this fact requires an adaption of the up-to technique used by Milner in his argument that (strong) bisimilarity is compatible with recursion [24].

Phillips showed that abstraction from divergence can be exploited to prove that every recursively enumerable transition system is branching bisimilar to a boundedly branching computable transition system [26]²²2Phillips actually claimed the correspondence modulo observation equivalence, but it is easy to see that his proof also works modulo branching bisimilarity.. In contrast, there exist recursively enumerable transition systems that are not divergence-preserving branching bisimilar to a computable transition system (cf., e.g., Example 3.6 in [3]). Hence, in a theory that aims to integrate computability and concurrency, divergence preservation is important.

In [3], interactivity is added to Turing machines by associating an action with every computation step. This so-called reactive Turing machine has a transition system semantics and can be studied from a concurrency-theoretic perspective. A transition system is called executable if it is behaviourally equivalent to the transition system associated with a reactive Turing machine. The notion of executability provides a way to characterise the absolute expressiveness of a process calculus. If every transition system that can be specified in the calculus is executable, then the calculus is said to be executable. Conversely, if every executable transition system can be specified in the calculus, then the calculus is said to be behaviourally complete.

A calculus with constants for deadlock and successful termination, unary action prefixes, binary operations for non-deterministic choice, sequencing and ACP-style parallel composition, iteration and nesting is both executable and behaviourally complete up to divergence-preserving branching bisimilarity [4]. The $\pi$-calculus is also behaviourally complete up to divergence-preserving branching bisimilarity. Since it allows the specification of transition systems with unbounded branching, it is, however, not executable up to divergence-preserving branching bisimilarity; it is nominally orbit-finitely executable up to the divergence-insensitive variant of branching bisimilarity [21].

The aforementioned results illustrate the role of divergence in the consideration of the absolute expressiveness of process calculi. Preservation of divergence is also widely accepted as an important criterion when comparing the relative expressiveness of process calculi [25].

We have discussed ther relational and modal characterisations of divergence-preserving branching bisimilarity, commented on its compatibility with respect to process algebraic operations and on its role in the study of the absolute expressiveness. We conclude by briefly mentioning some directions for future work.

Sound and complete axiomatisations for the divergence-sensitive spectrum of observation congruence for basic CCS with recursion are provided in [20]. The congruence result in [13] can serve as a stepping stone for providing similar sound and complete axiomatisations for divergence-preserving branching bisimilarity. Then, it would also be interesting to consider the axiomatisation of divergence-preserving branching bisimilarity for full CCS with recursion, although that would first require a non-trivial extension of the congruence result.

Ad hoc up-to techniques for divergence-preserving branching bisimilarity have already been used, e.g., in the congruence proof in [13] and in proof that the $\pi$-calculus is behaviourally complete [21]. Recently, several more generic up-to techniques for branching bisimilarity were proved sound [10]. An interesting direction for future work would be to consider extending those up-to techniques for divergence-preserving branching bisimilarity too.