In: Department of Interactive Systems, Report CS-R9121, Amsterdam. 1991.
Abstract: Branching bisimulation is a behavioral equivalence on labeled transition systems which has been proposed by Van Glabbeek und Weijland as an alternative to Milner's observational 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 conjection 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.