<p>For Q1, the answer is yes if we consider <em>image-finite</em> systems: for all node <span class="math-container">$t$</span> and label <span class="math-container">$a$</span>, the number of <span class="math-container">$a$</span>-successors of <span class="math-container">$t$</span> must be finite. In this case you don't even need fixpoints of the <span class="math-container">$\mu$</span>-calculus, only the fragment called <a href="https://en.wikipedia.org/wiki/Hennessy%E2%80%93Milner_logic" rel="nofollow noreferrer">Hennessy-Milner Logic</a> to distinguish non-bisimilar structures [HM85]. This is known as the Hennessy-Milner Theorem. Intuitively, the non-bisimilarity can be seen in a finite amount of steps of the form &quot;there exists an <span class="math-container">$a$</span>-successor&quot;, or &quot;for all <span class="math-container">$a$</span>-successor&quot;.</p>
<p>For more general cases, the paper [FCM17] might be of interest, in particular it gives at the end an example of two non image-finite structures (actually two nodes in the same structure) which are not bisimilar, but cannot be distinguished with  HML formulas. I suspect this is still true for <span class="math-container">$\mu$</span>-calculus formulas, but to be verified.</p>
<p>As for Q2, I'm not sure there is a clear &quot;maximal class&quot;. A class <span class="math-container">$\mathcal C$</span> with your conditions must at least satisfy the following requirements:</p>
<ul>
<li>at most one element per bisimulation equivalence class</li>
<li><span class="math-container">$\mathcal C$</span> is countable</li>
</ul>
<p>But then you have some room, since starting from such a class you can always replace one element by another which is bisimilar to it.
It is not even true that <span class="math-container">$\mathcal C$</span> must only contain finitely describable elements, since you can always take <span class="math-container">$\mathcal C=\{T\}$</span>, where <span class="math-container">$T$</span> is any structure, and complete it to a maximal class, and it would satisfy the requirements (although artificially). You probably have other conditions in mind for such a class, that would rule out the above example.</p>
<p>A natural such class is the set of regular ranked binary trees (where successors are ordered). Here &quot;regular&quot; means that the number of distincts subtrees is finite, even though the tree can be infinite.</p>
<p>[HM85] Matthew Hennessy &amp; Robin Milner (1985): Algebraic laws for nondeterminism and concurrency. Journal of the ACM, doi:10.1145/2455.2460.</p>
<p>[FCM17] Ferlez, J., Cleaveland, R. and Marcus, S., 2017. Bisimulation and Hennessy-Milner Logic for Generalized Synchronization Trees. arXiv preprint arXiv:1709.00827.</p>

CC BY-SA 4.0
2020-10-14T13:05:10.903Z
Are you sure about Q1? Since Hennessy–Milner logic is finitary, I’d think it may only characterize bisimilarity of finite (or at least image-finite) LTS. Don’t you need infinitary disjunctions and conjunctions for general LTS?
Emil Jeřábek
CC BY-SA 4.0
2020-10-14T14:24:57.690Z
@EmilJeřábek You're right I forgot the image-finite restriction, I add it.
Denis
CC BY-SA 4.0
2020-10-16T19:25:29.530Z
I used the words "a maximal" rather than "the maximum" in Q2 to avoid issues of uniqueness. In math, maximal typically means you can't add anything else to it but not necessarily that it is the only such class (of course it's also possible that even maximal classes don't exist).  In your analysis of Q2, the example of $\mathcal{C}=\{T\}$ does not work though because it will never be maximal, a fact which is an immediate corollary of your answer to Q1 since I can always add another non-bisimilar LTS and still satisfy my unique model condition.
wanderingmathematician
CC BY-SA 4.0
2020-10-16T22:22:37.313Z
I meant you can start with $\mathcal C=\{T\}$ and complete it to a maximal class, thereby showing that your maximal classes could contain any structure.
Denis
CC BY-SA 4.0
2020-10-16T23:11:10.833Z
I edited for clarity
Denis
CC BY-SA 4.0
2020-10-14T12:00:32.080Z
2020-10-16T23:09:59.107Z
2020-10-16T23:09:59.107Z
Denis
<p>I know that propositional modal <span class="math-container">$\mu$</span>-calculus <span class="math-container">$L\mu$</span> is bisimulation-invariant.  However, I'm curious to what degree it captures bisimulation.</p>
<blockquote>
<p>Q1:  Given two labeled transition systems <span class="math-container">$T_1$</span>, <span class="math-container">$T_2$</span> that are not bisimilar, is there an <span class="math-container">$L\mu$</span> formula which has <span class="math-container">$T_1$</span> as a model but not <span class="math-container">$T_2$</span>?</p>
</blockquote>
<blockquote>
<p>Q2 (stronger):  What is a maximal class <span class="math-container">$\mathcal{C}$</span> of labeled transition systems such that given any <span class="math-container">$T \in \mathcal{C}$</span>, there exists an <span class="math-container">$L\mu$</span> formula which has <span class="math-container">$T$</span> as its unique model in <span class="math-container">$\mathcal{C}$</span>?</p>
</blockquote>
<p>I hope this makes sense!  Basically I'm wondering to what degree I could replace discussion of transition systems with modal mu calculus formulas.  Thanks! :)</p>

CC BY-SA 4.0
2020-10-12T20:42:49.883Z
is the question restricted to finite systems ?
Denis
CC BY-SA 4.0
2020-10-13T23:54:01.160Z
@Denis No, although if you have a constructive way to generate a formula which uniquely characterizes a finite transition system, that would be interesting and perhaps something I could generalize.  The kind of systems I am interested in usually are product systems where at least one factor is an inductively defined system (e.g. the natural numbers with successor as edge).
wanderingmathematician
<lo.logic><model-checking><temporal-logic><modal-logic><mu-calculus>
Is modal $\mu$-calculus "equivalent" to bisimulation?
wanderingmathematician
# Is modal $\mu$-calculus "equivalent" to bisimulation?

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

I know that propositional modal $\mu$-calculus $L\mu$ is bisimulation-invariant. However, I'm curious to what degree it captures bisimulation.

> Q1: Given two labeled transition systems $T\_1$, $T\_2$ that are not bisimilar, is there an $L\mu$ formula which has $T\_1$ as a model but not $T\_2$?

> Q2 (stronger): What is a maximal class $\mathcal{C}$ of labeled transition systems such that given any $T \in \mathcal{C}$, there exists an $L\mu$ formula which has $T$ as its unique model in $\mathcal{C}$?

I hope this makes sense! Basically I'm wondering to what degree I could replace discussion of transition systems with modal mu calculus formulas. Thanks! :)

**Tags:** lo.logic, model-checking, temporal-logic, modal-logic, mu-calculus
> **Comments:**
> **username_1**: is the question restricted to finite systems ?  
> **username_0**: @Denis No, although if you have a constructive way to generate a formula which uniquely characterizes a finite transition system, that would be interesting and perhaps something I could generalize.  The kind of systems I am interested in usually are product systems where at least one factor is an inductively defined system (e.g. the natural numbers with successor as edge).  

---

## 1 answers

### Answer by username_1 on 2020-10-14. Score: 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](https://en.wikipedia.org/wiki/Hennessy%E2%80%93Milner_logic) to distinguish non-bisimilar structures [HM85]. This is known as the Hennessy-Milner Theorem. Intuitively, the non-bisimilarity can be seen in a finite amount of steps of the form "there exists an $a$-successor", or "for all $a$-successor".

For more general cases, the paper [FCM17] might be of interest, in particular it gives at the end an example of two non image-finite structures (actually two nodes in the same structure) which are not bisimilar, but cannot be distinguished with HML formulas. I suspect this is still true for $\mu$-calculus formulas, but to be verified.

As for Q2, I'm not sure there is a clear "maximal class". A class $\mathcal C$ with your conditions must at least satisfy the following requirements:

* at most one element per bisimulation equivalence class
* $\mathcal C$ is countable

But then you have some room, since starting from such a class you can always replace one element by another which is bisimilar to it.
It is not even true that $\mathcal C$ must only contain finitely describable elements, since you can always take $\mathcal C=\{T\}$, where $T$ is any structure, and complete it to a maximal class, and it would satisfy the requirements (although artificially). You probably have other conditions in mind for such a class, that would rule out the above example.

A natural such class is the set of regular ranked binary trees (where successors are ordered). Here "regular" means that the number of distincts subtrees is finite, even though the tree can be infinite.

[HM85] Matthew Hennessy & Robin Milner (1985): Algebraic laws for nondeterminism and concurrency. Journal of the ACM, doi:10.1145/2455.2460.

[FCM17] Ferlez, J., Cleaveland, R. and Marcus, S., 2017. Bisimulation and Hennessy-Milner Logic for Generalized Synchronization Trees. arXiv preprint arXiv:1709.00827.

> **Comments:**
> **username_2**: Are you sure about Q1? Since Hennessy–Milner logic is finitary, I’d think it may only characterize bisimilarity of finite (or at least image-finite) LTS. Don’t you need infinitary disjunctions and conjunctions for general LTS?  
> **username_1**: @EmilJeřábek You're right I forgot the image-finite restriction, I add it.  
> **username_0**: I used the words "a maximal" rather than "the maximum" in Q2 to avoid issues of uniqueness. In math, maximal typically means you can't add anything else to it but not necessarily that it is the only such class (of course it's also possible that even maximal classes don't exist).  In your analysis of Q2, the example of $\mathcal{C}=\{T\}$ does not work though because it will never be maximal, a fact which is an immediate corollary of your answer to Q1 since I can always add another non-bisimilar LTS and still satisfy my unique model condition.  
> **username_1**: I meant you can start with $\mathcal C=\{T\}$ and complete it to a maximal class, thereby showing that your maximal classes could contain any structure.  
> **username_1**: I edited for clarity  

---

