# 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  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... – wanderingmathematician Oct 16 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. – Denis Oct 16 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)$. – Denis Oct 17 at 0:00