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


3

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


Only top voted, non community-wiki answers of a minimum length are eligible