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

07/11/2023
by   Jan Martens, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset