Up-to techniques for branching bisimilarity. (English) Zbl 1440.68176
Chatzigeorgiou, Alexander (ed.) et al., SOFSEM 2020: theory and practice of computer science. 46th international conference on current trends in theory and practice of informatics, SOFSEM 2020, Limassol, Cyprus, January 20–24, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12011, 285-297 (2020).
Summary: 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.
For the entire collection see [Zbl 1435.68022].
For the entire collection see [Zbl 1435.68022].
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
References:
| [1] | Arun-Kumar, S., Hennessy, M.: An efficiency preorder for processes. Acta Inf. 29(8), 737-760 (1992) · Zbl 0790.68039 · doi:10.1007/BF01191894 |
| [2] | Bloom, B.: Structural operational semantics for weak bisimulations. TCS 146(1&2), 25-68 (1995) · Zbl 0873.68130 · doi:10.1016/0304-3975(94)00152-9 |
| [3] | Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. In: POPL, pp. 229-239. ACM (1988) · Zbl 0886.68027 |
| [4] | Bonchi, F., Petrisan, D., Pous, D., Rot, J.: A general account of coinduction up-to. Acta Inf. 54(2), 127-190 (2017) · Zbl 1371.68186 · doi:10.1007/s00236-016-0271-4 |
| [5] | Bonchi, F., Pous, D.: Hacking nondeterminism with induction and coinduction. Commun. ACM 58(2), 87-95 (2015) · doi:10.1145/2713167 |
| [6] | Brengos, T.: Weak bisimulation for coalgebras over order enriched monads. Log. Methods Comput. Sci. 11(2), 1-44 (2015) · Zbl 1391.68083 · doi:10.2168/LMCS-11(2:14)2015 |
| [7] | Fokkink, W., van Glabbeek, R.: Divide and congruence II: from decomposition of modal formulas to preservation of delay and weak bisimilarity. Inf. Comput. 257, 79-113 (2017) · Zbl 1380.68295 · doi:10.1016/j.ic.2017.10.003 |
| [8] | Fokkink, W., van Glabbeek, R., Luttik, B.: Divide and congruence III: from decomposition of modal formulas to preservation of stability and divergence. Inf. Comput. 268, 104435 (2019). https://doi.org/10.1016/j.ic.2019.104435. Article no. 31 pages · Zbl 1430.68162 · doi:104435&publication_year=2019&doi=10.1016/j.ic.2019.104435 |
| [9] | van Glabbeek, R.: On cool congruence formats for weak bisimulations. TCS 412(28), 3283-3302 (2011) · Zbl 1216.68199 · doi:10.1016/j.tcs.2011.02.036 |
| [10] | van Glabbeek, R.J.: A complete axiomatization for branching bisimulation congruence of finite-state behaviours. In: Borzyszkowski, A.M., Sokołowski, S. (eds.) MFCS 1993. LNCS, vol. 711, pp. 473-484. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57182-5_39 · doi:10.1007/3-540-57182-5_39 |
| [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) · Zbl 1364.68001 |
| [12] | Jacobs, B., Hughes, J.: Simulations in coalgebra. ENTCS 82(1), 128-149 (2003) · Zbl 1270.68191 |
| [13] | Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989) · Zbl 0683.68008 |
| [14] | Milner, R.: A complete axiomatisation for observational congruence of finite-state behaviors. Inf. Comput. 81(2), 227-247 (1989) · Zbl 0688.68050 · doi:10.1016/0890-5401(89)90070-9 |
| [15] | Pous, D.: New up-to techniques for weak bisimulation. TCS 380(1-2), 164-180 (2007) · Zbl 1118.68095 · doi:10.1016/j.tcs.2007.02.060 |
| [16] | Pous, D.: Coinduction all the way up. In: LICS, pp. 307-316. ACM (2016) · Zbl 1394.68352 |
| [17] | Pous, D., Sangiorgi, D.: Enhancements of the bisimulation proof method (2012) · Zbl 1285.68111 |
| [18] | Rutten, J.: Universal coalgebra: a theory of systems. TCS 249(1), 3-80 (2000) · Zbl 0951.68038 · doi:10.1016/S0304-3975(00)00056-6 |
| [19] | Sangiorgi, D.: On the proof method for bisimulation. In: Wiedermann, J., Hájek, P. (eds.) MFCS 1995. LNCS, vol. 969, pp. 479-488. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60246-1_153 · Zbl 1193.68177 · doi:10.1007/3-540-60246-1_153 |
| [20] | Sangiorgi, D., Milner, R.: The problem of “weak bisimulation up to”. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 32-46. Springer, Heidelberg (1992). https://doi.org/10.1007/BFb0084781 · doi:10.1007/BFb0084781 |
| [21] | Sangiorgi, D., Walker, D.: The Pi-Calculus - A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001) · Zbl 0981.68116 |
| [22] | Turi, D. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
