Rick Erkens: Up-to Techniques for Branching Bisimulation

Event Details

Branching bisimilarity is a notion of behavioral equivalence between processes. To prove that two processes are branching bisimilar one should provide a relation (a set of pairs) containing the two processes, such that the relation satisfies some properties. For recursive processes this relation often becomes infinite and complicated, which may lead to awkward and long proofs. We discuss improvements of the branching bisimulation proof technique that are based on the so-called ‘up-to techniques’ that already exist for strong and weak bisimulation.