<p>Q1: Yes, every LTS is bisimilar to its unfolding, which is a tree.</p>
<p>Q2: No, by a cardinality argument. For instance take infinite binary trees with <span class="math-container">$L=\{a,b\}$</span>. 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 <span class="math-container">$\mu$</span>-calculus formulas, so some bisimilarity classes are not captured by formulas.</p>
<p>Actually in this setting, a bisimilarity class can be exactly captured by a <span class="math-container">$L_\mu$</span> formula if and only if it is the bisimilarity class of a finite structure. The unfolding of a finite structure is called a <em>regular tree</em>. 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.</p>
<p>[1] The mu-calculus and model checking.
J Bradfield, I Walukiewicz.
Handbook of Model Checking, 871-919</p>

CC BY-SA 4.0
2020-10-16T23:23:33.633Z
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
CC BY-SA 4.0
2020-10-16T23:27:41.547Z
... to wrap my head around your second comment.  Weird to try to think up an example of a finite LTS which is bisimilar to a non-regular tree!
wanderingmathematician
CC BY-SA 4.0
2020-10-16T23:51:49.803Z
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
CC BY-SA 4.0
2020-10-17T00:00:59.367Z
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
CC BY-SA 4.0
2020-10-16T22:54:43.420Z
2020-10-16T23:07:45.173Z
2020-10-16T23:07:45.173Z
Denis
<p>Let <span class="math-container">$L$</span> be a finite set of labels, and let <span class="math-container">$\mathcal{C}$</span> be the set of finitely-branching transition systems labeled by <span class="math-container">$L$</span> and with a countable set of states.  Let <span class="math-container">$\sim$</span> denote the bisimulation relation, and let <span class="math-container">$\mathcal{C} / \sim$</span> denote the set of bisimulation equivalence classes of LTS's in <span class="math-container">$\mathcal{C}$</span>.</p>
<blockquote>
<p><strong>Q1:</strong>  Does every bisimilarity equivalence class <span class="math-container">$\alpha \in \mathcal{C} / \sim$</span> have a tree model?</p>
</blockquote>
<p>Let <span class="math-container">$L\mu$</span> denote the set of closed formulas in modal <span class="math-container">$\mu$</span>-calculus.</p>
<blockquote>
<p><strong>Q2:</strong>  True or false:  <span class="math-container">$\forall \alpha \in \mathcal{C} / \sim$</span>, <span class="math-container">$\exists F \in L\mu$</span> such that models<span class="math-container">$(F) \cap \mathcal{C} = \alpha$</span>.  Or in plain English, every bisimilarity class of countable and finitely-branching LTS's over <span class="math-container">$L$</span> is exactly the set of countable and finitely-branching models of some modal <span class="math-container">$\mu$</span>-calculus formula.</p>
</blockquote>
<p>An answer to either would be helpful, and answers to both would be sublime :)</p>

<lo.logic><model-checking><temporal-logic><process-algebra><mu-calculus>
Is every countable, finite-branching LTS bisimilar to a tree?
wanderingmathematician
# Is every countable, finite-branching LTS bisimilar to a tree?

(Asked by: username_0 on 2020-10-16)

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.

An answer to either would be helpful, and answers to both would be sublime :)

**Tags:** lo.logic, model-checking, temporal-logic, process-algebra, mu-calculus

---

## 1 answers

### Answer by username_1 on 2020-10-16. Score: 3 | Accepted answer

Q1: Yes, every LTS is bisimilar to its unfolding, which is a tree.

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.

[1] The mu-calculus and model checking.
J Bradfield, I Walukiewicz.
Handbook of Model Checking, 871-919

> **Comments:**
> **username_0**: 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...  
> **username_0**: ... to wrap my head around your second comment.  Weird to try to think up an example of a finite LTS which is bisimilar to a non-regular tree!  
> **username_1**: 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.  
> **username_1**: 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)$.  

---

