New answers tagged lo.logic
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
