# Tag Info

3

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 ...

2

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. ...

3

I stumbled upon this question now, many years later. In the interim the following paper has appeared: https://dl.acm.org/doi/10.1145/3278158 https://arxiv.org/abs/1704.08705 There the authors do precisely what Kaveh asks for in his question 2: they give a (uniform) TC0 algorithm for balancing, hence obtaining an alternative proof of the main result in Buss '...

Top 50 recent answers are included