Computing minimal distinguishing Hennessy-Milner formulas is NP-hard, but variants are tractable

TL;DR

This paper investigates the computational complexity of generating minimal distinguishing Hennessy-Milner formulas, showing NP-hardness in general but providing polynomial algorithms for specific variants, with practical benefits demonstrated by a prototype.

Contribution

It establishes NP-hardness results for minimal formulas and introduces polynomial algorithms for variants based on nested modalities and negations.

Findings

Minimal formulas are NP-hard to compute in general.

Polynomial algorithms exist for variants with minimal nested modalities.

Prototype implementation produces significantly smaller formulas than previous methods.

Abstract

We study the problem of computing minimal distinguishing formulas for non-bisimilar states in finite LTSs. We show that this is NP-hard if the size of the formula must be minimal. Similarly, the existence of a short distinguishing trace is NP-complete. However, we can provide polynomial algorithms, if minimality is formulated as the minimal number of nested modalities, and it can even be extended by recursively requiring a minimal number of nested negations. A prototype implementation shows that the generated formulas are much smaller than those generated by the method introduced by Cleaveland.