The problem of “weak bisimulation up to”

  • Davide Sangiorgi
  • Robin Milner
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)


“Bisimulation up to” is a technique for reducing the size of the relation needed to define a bisimulalion. It works smoothly in the strong case, where it was first introduced ([4]). But this does not directly generalize to the weak case, as erroneously reported in [4]. To overcome this problem, two new “up-to” techniques are proposed: They are respectively based on the use of expansion ([1]) and of almost-weak bisimulation. The second solution is more general than the first one, but expansion enjoys a nicer mathematical treatment. The usefulness and generality of the solutions is motivated with non-trivial examples: two different implementations of a sorting machine.


Strong Case Visible Action Silent Action Weak Case Sorting Machine 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Arun-Kumar, S., and Hennessy, M., An efficiency preorder for Processes, Proceedings of Theoretical Aspects of Computer Science, Tokyo, (1991), LNCS vol. 526, pp 152–175. To appear in Acta Informatica.MathSciNetGoogle Scholar
  2. [2]
    Moller, F. The Edinburgh Concurrency Workbench (Version 6.0) Report No. LFCS-TN-34, Dept of Computer Science, University of Edinburgh.Google Scholar
  3. [3]
    van Glabeek, R., and Weijland, W. P., Branching Time and Abstraction in Bisimulation Semantics, in Information Processing '89 (G.X. Ritter ed.), Elsevier Science (1989), pp 613–618.Google Scholar
  4. [4]
    Milner, R., A Calculus of Communicating Systems, Prentice Hall, 1989.Google Scholar
  5. [5]
    Milner, R., Expansions — notes RM12, handwritten notes, Edinburgh, march 1990.Google Scholar
  6. [6]
    Park, D.M., Concurrency on Automata and infinite sequences, in Conf. on Theoretical Computer Science, (P. Deussen ed.) Springer Verlag (1981) Berlin, LNCS vol. 104.Google Scholar
  7. [7]
    Sangiorgi, D., Bisimulations up to context (provisory title), in preparation, Edinburgh.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Davide Sangiorgi
    • 1
  • Robin Milner
    • 1
  1. 1.LFCS - Department of Computer ScienceEdinburgh UniversityEdinburghUK

Personalised recommendations