The Hennessy-Milner Logic (HML) is a modal logic that expresses behavioural properties of states in LTSs. We are interested in explaining behavioural inequivalence by constructing a formula that /distinguishes/ a pair of states, i.e. a formula that is true in exactly one of the states. Cleaveland presented a method to generate a HML-formula by back-tracking information from a partition refinement algorithm like the Kanellakis-Smolka  algorithm. This method yields a formula which is “often minimal in a precisely defined sense” – [1]. In this talk we cover the following:

1. ) We note that Cleaveland’s definition of minimal can be deceitful, and show that it is not always optimal to follow the choices made by a partition refinement algorithm.

2.) Sketch a polynomial time algorithm to compute distinguishing formulas minimal with respect to observation-depth (number of nested diamond modalities) and negation-depth (number of nested negations).

3.) Show by a reduction from CNF-SAT that the problem of computing a minimal distinguishing formula is NP-hard.

[1] Cleaveland, Rance. “On automatically explaining bisimulation inequivalence.” International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg, 1991.