# Is every countable, finite-branching LTS bisimilar to a tree?

Let $$L$$ be a finite set of labels, and let $$\mathcal{C}$$ be the set of finitely-branching transition systems labeled by $$L$$ and with a countable set of states. Let $$\sim$$ denote the bisimulation relation, and let $$\mathcal{C} / \sim$$ denote the set of bisimulation equivalence classes of LTS's in $$\mathcal{C}$$.

Q1: Does every bisimilarity equivalence class $$\alpha \in \mathcal{C} / \sim$$ have a tree model?

Let $$L\mu$$ denote the set of closed formulas in modal $$\mu$$-calculus.

Q2: True or false: $$\forall \alpha \in \mathcal{C} / \sim$$, $$\exists F \in L\mu$$ such that models$$(F) \cap \mathcal{C} = \alpha$$. Or in plain English, every bisimilarity class of countable and finitely-branching LTS's over $$L$$ is exactly the set of countable and finitely-branching models of some modal $$\mu$$-calculus formula.

Q2: No, by a cardinality argument. For instance take infinite binary trees with $$L=\{a,b\}$$. Each tree has countable set of states and is finitely-branching, but you have uncountably many such trees, even up to bisimilarity. However you have only countably many $$\mu$$-calculus formulas, so some bisimilarity classes are not captured by formulas.
Actually in this setting, a bisimilarity class can be exactly captured by a $$L_\mu$$ formula if and only if it is the bisimilarity class of a finite structure. The unfolding of a finite structure is called a regular tree. Any formula accepting a non-regular tree must also accept a regular tree, which is not bisimilar to it. See for instance [1] for more details.
• Wow, way shorter answers than I expected! I think I dissuaded myself from thinking Q1 was easy because I first considered countably branching LTS's and then was thinking that unfolding might give me cardinality problems that would take the result outside of $\mathcal{C}$ by creating too many states, although now that I rethink about it, even with countable branching I would have each level of the unfolding as a countable union of countable sets and the entire state space would be the countable union of levels, so still countable. Q2 answer makes perfect sense as well, although I'm trying... Oct 16, 2020 at 23:23
• There is probably a little misunderstanding: a non-regular infinite binary tree cannot be bisimilar to a finite LTS. What my last comment means is that if a formula accepts such a non-regular tree, it must accept a union of several $\sim$-classes, actually uncountably many, one of which contains a regular tree. Oct 16, 2020 at 23:51
• Maybe the confusion comes from the distinction between "captures" and "accept". I used "$\varphi$ captures $\alpha$" to say that $\textit{models}(\varphi)\cap\mathcal C=\alpha$ , and "$\varphi$ accepts $M$" for $M\in\textit{models}(\varphi)$. Oct 17, 2020 at 0:00