The problem of “weak bisimulation up to”
“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 (). But this does not directly generalize to the weak case, as erroneously reported in . To overcome this problem, two new “up-to” techniques are proposed: They are respectively based on the use of expansion () 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.
KeywordsStrong Case Visible Action Silent Action Weak Case Sorting Machine
Unable to display preview. Download preview PDF.
- Moller, F. The Edinburgh Concurrency Workbench (Version 6.0) Report No. LFCS-TN-34, Dept of Computer Science, University of Edinburgh.Google Scholar
- 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
- Milner, R., A Calculus of Communicating Systems, Prentice Hall, 1989.Google Scholar
- Milner, R., Expansions — notes RM12, handwritten notes, Edinburgh, march 1990.Google Scholar
- 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
- Sangiorgi, D., Bisimulations up to context (provisory title), in preparation, Edinburgh.Google Scholar