1
$\begingroup$

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 :)

Improve this question
$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

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

Improve this answer
$\endgroup$
4
  • $\begingroup$ 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... $\endgroup$
    – wanderingmathematician
    Oct 16, 2020 at 23:23
  • $\begingroup$ ... 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! $\endgroup$
    – wanderingmathematician
    Oct 16, 2020 at 23:27
  • 1
    $\begingroup$ 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. $\endgroup$
    – Denis
    Oct 16, 2020 at 23:51
  • 1
    $\begingroup$ 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)$. $\endgroup$
    – Denis
    Oct 17, 2020 at 0:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.