Top

Published in:

2020 | OriginalPaper | Chapter

Up-to Techniques for Branching Bisimilarity

Authors : Rick Erkens, Jurriaan Rot, Bas Luttik

Published in: SOFSEM 2020: Theory and Practice of Computer Science

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter The Order Type of Scattered Context-Free Orderings of Rank One Is Computable

next chapter Crowd Detection for Drone Safe Landing Through Fully-Convolutional Neural Networks

Note that this is fundamentally different from reducing weak bisimilarity to strong bisimilarity on a saturated transition system; there, a challenging transition is weak as well. Here, instead, strong transitions are answered by weak transitions.

Arun-Kumar, S., Hennessy, M.: An efficiency preorder for processes. Acta Inf. 29(8), 737–760 (1992)MathSciNetCrossRef

Bloom, B.: Structural operational semantics for weak bisimulations. TCS 146(1&2), 25–68 (1995)MathSciNetCrossRef

Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. In: POPL, pp. 229–239. ACM (1988)

Bonchi, F., Petrisan, D., Pous, D., Rot, J.: A general account of coinduction up-to. Acta Inf. 54(2), 127–190 (2017)MathSciNetCrossRef

Bonchi, F., Pous, D.: Hacking nondeterminism with induction and coinduction. Commun. ACM 58(2), 87–95 (2015)CrossRef

Brengos, T.: Weak bisimulation for coalgebras over order enriched monads. Log. Methods Comput. Sci. 11(2), 1–44 (2015) MathSciNetCrossRef

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)MathSciNetCrossRef

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 pagesMathSciNetCrossRefMATH

van Glabbeek, R.: On cool congruence formats for weak bisimulations. TCS 412(28), 3283–3302 (2011)MathSciNetCrossRef

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_39CrossRef

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)

12.

Jacobs, B., Hughes, J.: Simulations in coalgebra. ENTCS 82(1), 128–149 (2003)MATH

13.

Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)

14.

Milner, R.: A complete axiomatisation for observational congruence of finite-state behaviors. Inf. Comput. 81(2), 227–247 (1989)CrossRef

15.

Pous, D.: New up-to techniques for weak bisimulation. TCS 380(1–2), 164–180 (2007)MathSciNetCrossRef

16.

Pous, D.: Coinduction all the way up. In: LICS, pp. 307–316. ACM (2016)

17.

Pous, D., Sangiorgi, D.: Enhancements of the bisimulation proof method (2012)

18.

Rutten, J.: Universal coalgebra: a theory of systems. TCS 249(1), 3–80 (2000)MathSciNetCrossRef

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_153CrossRef

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/BFb0084781CrossRef

21.

Sangiorgi, D., Walker, D.: The Pi-Calculus - A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)MATH

22.

Turi, D., Plotkin, G.: Towards a mathematical operational semantics. In: LICS, pp. 280–291. IEEE (1997)

Title: Up-to Techniques for Branching Bisimilarity
Authors: Rick Erkens
Jurriaan Rot
Bas Luttik
Publisher: Springer International Publishing
Book: SOFSEM 2020: Theory and Practice of Computer Science
Print ISBN: 978-3-030-38918-5

Electronic ISBN: 978-3-030-38919-2

Copyright Year: 2020
DOI: https://doi.org/10.1007/978-3-030-38919-2_24

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner