Up-to Techniques for Branching Bisimilarity
Ever since the introduction of behavioral equivalences on processes one has been searching for efficient proof techniques that accompany those equivalences. Both strong bisimilarity and weak bisimilarity are accompanied by an arsenal of up-to techniques: enhancements of their proof methods. For branching bisimilarity, these results have not been established yet. We show that a powerful proof technique is sound for branching bisimilarity by combining the three techniques of up to union, up to expansion and up to context for Bloom’s BB cool format. We then make an initial proposal for casting the correctness proof of the up to context technique in an abstract coalgebraic setting, covering branching but also \(\eta \), delay and weak bisimilarity.
We thank Filippo Bonchi for the idea how to encode branching bisimilarity coalgebraically, and the reviewers for their useful comments.
- 3.Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. In: POPL, pp. 229–239. ACM (1988)Google Scholar
- 11.Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science, vol. 59. Cambridge University Press, Cambridge (2016)Google Scholar
- 13.Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)Google Scholar
- 16.Pous, D.: Coinduction all the way up. In: LICS, pp. 307–316. ACM (2016)Google Scholar
- 17.Pous, D., Sangiorgi, D.: Enhancements of the bisimulation proof method (2012)Google Scholar
- 22.Turi, D., Plotkin, G.: Towards a mathematical operational semantics. In: LICS, pp. 280–291. IEEE (1997)Google Scholar