=Paper=
{{Paper
|id=Vol-2243/invited2
|storemode=property
|title=Bisimilarity Via Unique-Solution Techniques
|pdfUrl=https://ceur-ws.org/Vol-2243/invited2.pdf
|volume=Vol-2243
|authors=Davide Sangiorgi
|dblpUrl=https://dblp.org/rec/conf/ictcs/Sangiorgi18
}}
==Bisimilarity Via Unique-Solution Techniques==
https://ceur-ws.org/Vol-2243/invited2.pdf
Bisimilarity via unique-solution techniques
Davide Sangiorgi
University of Bologna and INRIA
1 Introduction
Bisimilarity is employed to de ne behavioural equivalences and reason about them.
Finding its origins in concurrency theory, bisimilarity is now widely used also in
other areas, as well as outside Computer Science.
In proofs of bisimilarity results, the bisimulation proof method has become
predominant, particularly with the enhancements of the method provided by the
so called `up-to techniques' [13]. Among these, one of the most powerful ones is
`up-to context', whereby, during the bisimulation game, a common context in the
derivatives of two terms can be erased. Forms of `bisimulations up-to context'
have been shown to be e ective in various elds, including process calculi [13, 18,
11], -calculi [7, 6, 5, 22], and automata [1, 16]. A lot of work has been carried out
recently on 'up-to context' and other up-to techniques, as well as on trying to give
a systematic treatment of the set of all such techniques (e.g., the tutorial [13]).
In this paper we summarise a di erent, ongoing, strand of work about tech-
niques for proving bisimilarity results. This strand is inspired by Milner's theorem
about unique solution of equations in his landmark book on CCS [8]. This theorem
roughly says that two tuples of processes are componentwise bisimilar if they are
solutions of the same system of equations. Milner's theorem has however syntactic
constraints, on the shape of the equations. For instance, the theorem heavily relies
on the sum operator { any other operator but pre x and sum is essentially for-
bidden. This limits the expressiveness of the technique (since occurrences of other
operators above the variables, such as parallel composition and restriction, in gen-
eral cannot be removed), and its transport onto other languages (e.g., languages
for distributed systems or higher-order languages, which usually do not include
the sum operator).
An important remark has to be made before providing more technical details.
In this paper, behavioural equivalences, hence also bisimilarity, are meant to be
weak because they abstract from internal moves of terms, as opposed to the strong
ones, which make no distinctions between the internal moves and the external ones
(i.e., the interactions with the environment). Weak equivalences are, practically,
the most relevant ones: e.g., two equal programs may produce the same result with
di erent numbers of evaluation steps. The problems mentioned above concerning
Milner's theorem do not exist in the case of strong bisimilarity.
We outline two directions for improving Milner's unique-solution technique.
The rst consists in replacing equations with special inequations called contrac-
tions [21]. The second consists in replacing the most severe syntactic constraint in
Milner's theorem with a semantic condition that has to do with divergence [3, 4].
Other motivations for the work on unique solutions are the following. First,
the unique-solution techniques convey the avour of 'bisimilarity up-to context'
techinques, as the equations (or contractions) intuitively bring out those contexts
that would be erased in an 'up-to context' proof (indeed there are completeness
results with respect to certain forms of up-to context, in CCS-like languages [21]).
Thus here the goal is to bring light into the up-to-context techniques. For instance,
in higher-order languages, while there are well-developed techniques for proving
congruence [12], up-to context is still poorly understood [7, 6, 5, 22, 11].
Another possible interest for the unique-solution techniques is that they can be
transported onto other equivalences, including contextually-de ned equivalences
such as barbed congruence, and non-coinductive equivalences such as contextual
equivalence (i.e., may testing) and trace equivalence.
2 Equations and Milner's theorem
We recall equations and Milner's theorem, in the setting of CCS. We omit the
standard de nitions of syntax and operational semantics of the calculus, as well
of weak bisimulation, written , [8].
Uniqueness of solutions of equations [8] intuitively says that if a context C obeys
certain conditions, then all processes P that satisfy the equation P C[P ] are
bisimilar with each other. We use capital letters X; Y; Z for variable of equations.
The body of an equation is a CCS expression possibly containing variables.
De nition 1. Given, for each i of a countable indexing set I , variables Xi , and
expressions Ei possibly containing such variables, fXi = Ei gi2I is a system of
equations. (There is one equation for each variable Xi .)
We write E[Pe] for the expression resulting from E by replacing each variable
Xi with the process Pi
De nition 2. Suppose fXi = Ei gi2I is a system of equations:
{ Pe is a solution of the system of equations for if for each i it holds that
Pi Ei [Pe].
{ the system has a unique solution for if whenever Pe and Qe are both solutions
for , then Pe Q e.
De nition 3. A system of equations fXi = Ei gi2I is
{ guarded if, in each Ei , each occurrence of an equation variable is underneath
a visible pre x (i.e., a pre x that is not );
{ sequential if, in each Ei , each occurrence of an equation variable only appears
underneath pre xes and sums.
In other words, if the system is sequential, then for every expression Ei , any
subexpression of Ei in which Xj appears, apart from Xj itself, is a sum (of pre xed
terms). For instance, X = . X + . 0 is sequential but not guarded; using `
for a visible pre x, X = `. X j P is guarded but not sequential, whereas X =
`. X + . a (a. b j a. 0), as well as X = . (a. X + . b. X + ) are both guarded
and sequential.
Theorem 1 (unique solution of equations, [8]). A system of guarded and
sequential equations has a unique solution for .
3 Contractions
Intuitively, for a behavioural equivalence , its contraction is a preorder in
which P Q holds if P Q and, in addition, Q has the possibility of being at
least as ecient as P . That is, if P can do some work (i.e., some interactions with
its environment), then Q should be able to do the same work at least as quickly
as P (i.e., performing no more -steps then those performed by P ). Process Q,
however, may be nondeterministic and may have other ways of doing the same
work, and these could be slow (i.e., involving more -steps than those performed
by P ). The bisimilarity contraction is written bis and is a precongruence in CCS;
see [20, 21] for the formal de nition. A system of contractions is de ned as a system
of equations, except that the contraction symbol is used in the place of the
equality symbol =. Thus a system of contractions is a set fXi Ei gi2I where I is
an indexing set and expressions Ei may contain the contraction variables fXi gi2I .
De nition 4. Given a behavioural equivalence and its contraction , and a
system of contractions fXi Ei gi2I , we say that:
{ Pe is a solution for of the system of contractions if Pe E[
e Pe];
{ the system has a unique solution for if whenever P and Q are both solutions
e e
for then Pe Q e.
When we reason about bisimilarity, the contraction symbol is interpreted as
the bisimilarity contraction bis , and the equivalence as the bisimilarity . Thus
Pe being a solution for bis of the system of contractions fXi Ei gi2I means that
Pe bis E[
e Pe]; and the system having a unique solution for means that whenever
P and Q are both solutions for bis then Pe Q.
e e e
Lemma 1. If a system of equations fXi = Ei gi2I has a unique solution for ,
then also the corresponding system of contractions fXi Ei gi2I has a unique
solution for .
The converse of the lemma, in contrast, is false: systems of contractions more
easily have a unique solution.
De nition 5. A system of contractions fXi Ei gi2I is weakly guarded if, in
each Ei , each occurrence of a contraction variable is underneath a pre x.
Theorem 2 (unique solution of contractions for ). A system of weakly-
guarded contractions has a unique solution for .
We refer to [20, 21] for discussions on completeness (the method is complete, in
the sense that any process bisimilarity can be proved with the method), examples
of application, abstract formulation of the method, and generalisation to other
languages and to other equivalences, including non-coinductive equivalences.
4 Divergence in equations
In this section we highlight a di erent approach, whereby one goes back to equa-
tions, but adds a condition based in divergence. In its basic form, the method (in-
spired by results by Roscoe in CSP [15, 14] essentially says that a guarded equation
(or system of equations) whose in nite unfolding never produces a divergence has
the unique-solution property.
We discuss the approach in CCS, as before, and assuming for simplicity a single
equation X = E (the results can be generalised to systems of equations). We need
to reason with the unfoldings of the given equation X = E: we de ne the n-th
unfolding of E to be E n ; thus E 1 is de ned as E, E 2 as E[E], and E n+1 as
E n [E]. The in nite unfolding represents the simplest and most intuitive solution
to the equation. In the CCS grammar, such a solution is obtained by turning the
4
equation into a recursive de nition, namely the process KE with KE = E[KE ].
Process KE is the syntactic solution of the equation.
Theorem 3 (Unique solution). A guarded system of equations whose syntactic
solutions do not diverge has a unique solution for .
The theorem can be strengthened by distinguishing between di erent forms
of divergence; in particular, ignoring divergences that already show up in partial
unfoldings of the equations, i.e., E n for some n 0, called innocuous divergences.
We refer to [3] for abstract formulations of the method, application to other
languages, equivalences, as well as preorders. In [4] the method is applied to show-
ing what is the equivalence induced on -terms by Milner's encoding into the
-calculus (for call-by-value), a problem that had remained open since Milner's
work on functions as processes [10, 9]. Such proofs seem hard to carry out with
the ordinary bisimulation proof method, even when enhanced by means of `up-to
techniques'.
4.1 Comparison
In comparison with the method based on contractions, the main drawback for
the method based on equations is the presence of a semantic condition, involving
divergence: the unfoldings of the equations should not produce divergences, or only
produce innocuous divergences. Various techniques for checking divergence exist in
the literature, including type-based techniques [23, 19, 2]; a syntactic condition is
proposed in [3]. However, in general divergence is undecidable, and therefore, the
check may sometimes be unfeasible. Nevertheless, the equations that one writes
for proofs usually involve forms of `normalised' processes, and as such they are
divergence free (or at most, contain only innocuous divergences). More experiments
are needed to validate this claim or to understand how limiting this problem is.
On the other hand, using contractions for proving an equivalence, one needs
also the theory of the associated contraction preorder; moreover there may be
processes for which the contraction technique is not applicable simply because the
contraction preorder is strictly ner than the equivalence, and therefore one of the
processes fails to be a solution.
References
1. Bonchi, F., Pous, D.: Checking nfa equivalence with bisimulations up to congruence.
In: Giacobazzi, R., Cousot, R. (eds.) Proc. POPL'13. pp. 457{468. ACM (2013)
2. Demangeon, R., Hirschko , D., Sangiorgi, D.: Termination in impure concurrent
languages. In: Proc. 21th CONCUR. LNCS 6269, pp. 328{342. Springer (2010)
3. Durier, A., Hirschko , D., Sangiorgi, D.: Divergence and unique solution of equa-
tions. In: 28th CONCUR. LIPIcs, vol. 85, pp. 11:1{11:16. Schloss Dagstuhl - Leibniz-
Zentrum fuer Informatik (2017)
4. Durier, A., Hirschko , D., Sangiorgi, D.: Eager functions as processes. In: 33nd An-
nual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. IEEE Com-
puter Society (2018)
5. Koutavas, V., Wand, M.: Small bisimulations for reasoning about higher-order im-
perative programs. In: Proc. 33rd POPL. pp. 141{152 (2006)
6. Lassen, S.: Relational reasoning about contexts. In: Higher-order operational tech-
niques in semantics. pp. 91{135. Cambridge University Press (1998)
7. Lassen, S.: Bisimulation in untyped lambda calculus: Bohm trees and bisimulation
up to context. Electr. Notes Theor. Comput. Sci. 20, 346{374 (1999)
8. Milner, R.: Communication and Concurrency. Prentice Hall (1989)
9. Milner, R.: Functions as processes. Journal of Mathematical Structures in Computer
Science 2(2), 119{141 (1992)
10. Milner, R.: Functions as processes. In: ICALP. LNCS 443, pp. 167{180. Springer
(1990)
11. Pierard, A., Sumii, E.: Sound bisimulations for higher-order distributed process cal-
culus. In: Proc. FOSSACS. LNCS 6604, pp. 123{137. Springer (2011)
12. Pitts, A.: Howe's method. In: Sangiorgi, D., Rutten, J. (eds.) Advanced Topics in
Bisimulation and Coinduction. Cambridge University Press (2012)
13. Pous, D., Sangiorgi, D.: Enhancements of the bisimulation proof method. In: San-
giorgi, D., Rutten, J. (eds.) Advanced Topics in Bisimulation and Coinduction. Cam-
bridge University Press (2012)
14. Roscoe, A.W.: An alternative order for the failures model. J. Log. Comput. 2(5),
557{577 (1992)
15. Roscoe, A.W.: The theory and practice of concurrency. Prentice Hall (1998).
16. Rot, J., Bonsangue, M.M., Rutten, J.J.M.M.: Coinductive proof techniques for lan-
guage equivalence. In: Proc. LATA. LNCS 7810, pp. 480{492. Springer (2013)
17. Sangiorgi, D., Milner, R.: The problem of \Weak Bisimulation up to". In: Proc.
CONCUR '92. LNCS 630, pp. 32{46. Springer Verlag (1992)
18. Sangiorgi, D., Walker, D.: The -calculus: a Theory of Mobile Processes. Cambridge
University Press (2001)
19. Sangiorgi, D.: Termination of processes. Mathematical Structures in Computer Sci-
ence 16(1), 1{39 (2006)
20. Sangiorgi, D.: Equations, contractions, and unique solutions. In: POPL 2015. pp.
421{432. ACM (2015),
21. Sangiorgi, D.: Equations, contractions, and unique solutions. ACM Trans. Comput.
Log. 18(1), 4:1{4:30 (2017),
22. Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order
languages. ACM Trans. Program. Lang. Syst. 33(1), 5 (2011)
23. Yoshida, N., Berger, M., Honda, K.: Strong Normalisation in the Pi-Calculus. Infor-
mation and Computation 191(2), 145{202 (2004)