Up-to techniques for branching bisimilarity

DOI10.1007/978-3-030-38919-2_24MaRDI QIDQ3297777zbMATH OpenOpenAlexFDO

Authors Rick Erkens, Jurriaan Rot, Bas Luttik

Publication date 20 July 2020

Published in SOFSEM 2020: Theory and Practice of Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2001.08944

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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.

Recommendations

• Automata, Languages and Programming
• New up-to techniques for weak bisimulation
• Beyond Bisimulation: The “up-to” Techniques
• Coalgebraic bisimulation-up-to
• Lax bialgebras and up-to techniques for weak bisimulations

Cites work

• A complete axiomatisation for observational congruence of finite-state behaviours
• A general account of coinduction up-to
• An efficiency preorder for processes
• Bisimulation can't be traced
• Coinduction All the Way Up
• Divide and congruence. II: From decomposition of modal formulas to preservation of delay and weak bisimilarity
• Divide and congruence. III: From decomposition of modal formulas to preservation of stability and divergence
• Enhancements of the bisimulation proof method
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• Introduction to coalgebra. Towards mathematics of states and observation
• New up-to techniques for weak bisimulation
• On cool congruence formats for weak bisimulations
• On the proof method for bisimulation
• Simulations in coalgebra
• Structural operational semantics for weak bisimulations
• The -calculus: A theory of mobile processes
• Universal coalgebra: A theory of systems
• Weak bisimulation for coalgebras over order enriched monads

Cited in

(6)

• Combining semilattices and semimodules
• scientific article; zbMATH DE number 7453959 (Why is no real title available?)
• Lax bialgebras and up-to techniques for weak bisimulations
• Automata, Languages and Programming
• Branching bisimulation semantics enables noninterference analysis of reversible systems
• Rooted divergence-preserving branching bisimilarity is a congruence for guarded CCS

This page was built for publication: Up-to techniques for branching bisimilarity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3297777)