Computing distinguishing formulas for branching bisimulation

Abstract

Branching bisimulation is a behavioral equivalence on labeled transition systems which has been proposed by Van Glabbeek and Weijland as an alternative to Milner’s observation equivalence. This paper presents an algorithm which, given two branching bisimulation inequivalent finite state processes, produces a distinguishing formula in Hennessy-Milner logic extended with an ‘until’ operator. The algorithm, which is a modification of an algorithm due to Cleaveland, works in conjunction with a partition-refinement algorithm for deciding branching bisimulation equivalence. Our algorithm provides a useful extension to the algorithm for deciding equivalence because it tells a user why certain finite state systems are inequivalent. Note: The research of the author is supported by the European Communities under RACE project no. 1046, Specification and Programming Environment for Communication Software (SPECS). This article does not necessarily reflect the view of the SPECS project.