2
$\begingroup$

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

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ is the question restricted to finite systems ? $\endgroup$
    – Denis
    Oct 12, 2020 at 20:42
  • $\begingroup$ @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). $\endgroup$
    – wanderingmathematician
    Oct 13, 2020 at 23:54

1 Answer 1

Reset to default
3
$\begingroup$

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

Improve this answer
$\endgroup$
5
  • $\begingroup$ 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? $\endgroup$
    – Emil Jeřábek
    Oct 14, 2020 at 13:05
  • $\begingroup$ @EmilJeřábek You're right I forgot the image-finite restriction, I add it. $\endgroup$
    – Denis
    Oct 14, 2020 at 14:24
  • $\begingroup$ 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. $\endgroup$
    – wanderingmathematician
    Oct 16, 2020 at 19:25
  • $\begingroup$ 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. $\endgroup$
    – Denis
    Oct 16, 2020 at 22:22
  • $\begingroup$ I edited for clarity $\endgroup$
    – Denis
    Oct 16, 2020 at 23:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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