Whenever two Labelled Transition Systems (LTSs) are behaviourally inequivalent to each other, one may be interested why this is the case. Using a modal logic that characterises such a behavioural equivalence one can create formulae that distinguish these two LTSs, exposing the reason for the inequivalence. In this presentation I will describe the work by Rance Cleaveland on computing distinguishing formulae for strong bisimulation and the work by Henri Korver on computing distinguishing formulae for branching bisimulation. Also, I will compare the work of Korver with an alternate logic for characterising branching bisimulation and propose ideas to (possibly) improve on Korvers work.