Is modal $\mu$-calculus "equivalent" to bisimulation? I know that propositional modal $\mu$-calculus $L\mu$ is bisimulation-invariant.  However, I'm curious to what degree it captures bisimulation.

Q1:  Given two labeled transition systems $T_1$, $T_2$ that are not bisimilar, is there an $L\mu$ formula which has $T_1$ as a model but not $T_2$?


Q2 (stronger):  What is a maximal class $\mathcal{C}$ of labeled transition systems such that given any $T \in \mathcal{C}$, there exists an $L\mu$ formula which has $T$ as its unique model in $\mathcal{C}$?

I hope this makes sense!  Basically I'm wondering to what degree I could replace discussion of transition systems with modal mu calculus formulas.  Thanks! :)
For Q1, the answer is yes if we consider image-finite systems: for all node $t$ and label $a$, the number of $a$-successors of $t$ must be finite. In this case you don't even need fixpoints of the $\mu$-calculus, only the fragment called Hennessy-Milner Logic to distinguish non-bisimilar structures [HM85]. This is known as the Hennessy-Milner Theorem. Intuitively, the non-bisimilarity can be seen in a finite amount of steps of the form &quot;there exists an $a$-successor&quot;, or &quot;for all $a$-successor&quot;.
For more general cases, the paper [FCM17] might be of interest, in particular it gives at the end an example of two non image-finite structures (actually two nodes in the same structure) which are not bisimilar, but cannot be distinguished with  HML formulas. I suspect this is still true for $\mu$-calculus formulas, but to be verified.
As for Q2, I'm not sure there is a clear &quot;maximal class&quot;. A class $\mathcal C$ with your conditions must at least satisfy the following requirements:

at most one element per bisimulation equivalence class
$\mathcal C$ is countable

But then you have some room, since starting from such a class you can always replace one element by another which is bisimilar to it.
It is not even true that $\mathcal C$ must only contain finitely describable elements, since you can always take $\mathcal C=\{T\}$, where $T$ is any structure, and complete it to a maximal class, and it would satisfy the requirements (although artificially). You probably have other conditions in mind for such a class, that would rule out the above example.
A natural such class is the set of regular ranked binary trees (where successors are ordered). Here &quot;regular&quot; means that the number of distincts subtrees is finite, even though the tree can be infinite.
[HM85] Matthew Hennessy &amp; Robin Milner (1985): Algebraic laws for nondeterminism and concurrency. Journal of the ACM, doi:10.1145/2455.2460.
[FCM17] Ferlez, J., Cleaveland, R. and Marcus, S., 2017. Bisimulation and Hennessy-Milner Logic for Generalized Synchronization Trees. arXiv preprint arXiv:1709.00827.