Minimal Depth Distinguishing Formulas Without Until for Branching Bisimulation

In [16] an algorithm for distinguishing formulas for branching bisimulation is proposed. This algorithm has two shortcomings. First, it uses a dedicated until operator, and second, the generated formulas are in no sense minimal. Here we propose a method that generates formulas fitting in the modal mu-calculus, or more precisely, in Hennessy-Milner logic with one regular modality. We provide a polynomial-time algorithm that generates a distinguishing formula that is guaranteed to have minimal depth. Our technical exposition heavily relies on branching apartness, the dual of branching bisimulation.