- two bisimilar states in a labelled transition system satisfy exactly the same formulae in a multi-modal logic now called Hennessy-Milner logic, and
- two states in a labelled transition system that satisfy a mild finiteness constraint (called image finiteness) and enjoy the same properties expressible in Hennessy-Milner logic are bisimilar.
Characteristic formulae have a long history in concurrency theory. However, to be best of my knowledge, the complexity of determining whether a formula is characteristic had not been studied before Antonis Achilleos first addressed the problem in this conference paper. In that paper, Antonis focused on the complexity of the problem of determining whether a formula F is complete, in the sense that, for each formula G, it can derive either G or its negation.
Our recent preprint The Complexity of Identifying Characteristic Formulae extends the results originally obtained by Antonis to a variety of modal logics, possibly including least and greatest fixed-point operators. In the paper, we show that completeness, characterization, and validity have the same complexity — with some exceptions for which there are, in general, no complete formulae. So, for most modal logics of interest, the problem is coNP-complete or PSPACE-complete, and becomes EXPTIME-complete for modal logics with fixed points. To prove our upper bounds, we present a nondeterministic procedure with an oracle for validity that combines tableaux and a test for bisimilarity, and determines whether a formula is complete.
I think that there is still a lot of work that can be done in studying this problem, with respect to a variety of other notions of equivalence considered in concurrency theory, so stay tuned for further updates.