In earlier work (with Komi Golov) we defined a notion of directed branching bisimulation and its associated positive Hennessy-Milner logic with until (PHMLU). It has the nice property that s is directed bisimular with t if and only if the PHMLU theory of s is a subset of the theory of t.
This has various good properties, but the intuition that s is directed bisimular with t if “everything that s can do can be done by t” is not fully captured.
To solve this we now present a refinement of directed branching bisimulation and the logic PHMLU that captures the idea that “possible behaviour is preserved” for directed bisimilar states.

Joint work with Tanja Muller and Komi Golov.