This is a follow up of a previous post where a formalization of the concept of behavior –bisimilarity– was presented. Now I want to focus into one approach to characterize “equivalence of behavior,” that is, when two states of a system are bisimilar.

So, let $s$ and $t$ be states of a Kripke frame $S$. It is fairly reasonable to try to perform some test on $s$ and $t$ (that is, to the system while standing in respective states), and check if both states respond evenly to all tests. Since we can only interact with the system by pressing buttons (this includes “just checkin’ if it was available!”), our main test will have the format “press $a$ and see what happens next”. More precisely, if a test $\phi$ is already given and $a\in L$ is an action, a new test can be constructed with the intended meaning: Test if it is possible to make an $a$-transition, to a state passing test $\phi$. We will denote this test by $\modal{a}\phi$. To have something to start with, we let $\top$ to be the trivial, always successful test; and given two tests $\phi$ and $\psi$, $\phi\y\psi$ is the test that is successful only when both tests are successful. Finally, the negation of a test $\neg\phi$ is successful iff $\phi$ is unsuccessful.

What we have defined is a fragment of basic modal logic, and we have the next beautiful result.

Theorem. (Hennessy-Milner, van Benthem). If $S$ is finite, two states passing exactly the same tests are bisimilar.

In our example in the previous post, $s$ will fail the test $\modal{a}(\neg\modal{c}\top)$ (because every $a$-successor of $s$ can perform a $c$-transition), while $t$ would pass it. (This example might give the wrong impression that $\y$ is superfluous; it is actually necessary, and showing this is a nice exercise.)

$\newcommand{\trans}[1]{\stackrel{#1}{\to}}$The hypothesis that $S$ be finite can be greatly relaxed to only requiring that for each state $s$ and each action $a$, the set $\{s’\in S : s\trans{a}s’\}$ of successors of $s$ be finite. There is another version of the same theorem for arbitrary $S$, with the same proof, but now we need the ability to do infinitely many tests at once; that is, we need infinite conjunctions $\bigwedge_i\phi_i$. As always, passing to the Infinite brings all kinds of both interesting and creepy stuff. To put things into the right perspective, consider only countable frames. In this case, one only needs countable conjunctions. In some sense, the HMvB Theorem keeps much of its beauty and elegance, but now we have uncountable many tests. The very first question to think of, couldn’t we do with just countably many tests?!? comes to one’s mind. Putting this properly, we would like to know if there is some alternative, countable logic that characterizes bisimilarity. The answer is yes, but at a cost. This in turn comes from another elegant argument by X. Caicedo, who proceeds to define the new logic with countably many “atomic” tests (like $\top$) $C_n$ ($n\in\N$), and proving that this logic characterizes bisimilarity.

The second thing to ask is, OK, tell me what buttons do I press to perform test $C_n$. The problem is that there is no simple way to describe these tests. In other words, a uniform description of the tests $C_n$ will be at least as difficult as describing behavior completely in all countable frames. Even more is true: Every countable logic describing behavior for countable Kripke frames will suffer this shortcoming.

This result was recently published in Math. Struct. Comp. Sci. under the title Bisimilarity is not Borel. People at Cambridge University Press decided it was convenient to associate to Kudos, a web company that helps your papers get to be known (at least they say this, but I couldn’t check yet), and the latter suggested that I answer three basic questions concerning this paper, as an alternative to the plain abstract. I’ll copy here what I wrote, with some changes to fit the notation of this post.

What is it about? Bisimilarity is one of the main notions of “equivalence of behavior” in Theoretical Computer Science; in particular it can be defined on the space of all countable transition systems [Kripke frames] with a fixed countable set of labelled actions. The latter has a natural topological structure, and it is proved that the relation of bisimilarity on this space has high complexity in the hierarchy of its subsets; namely, more complex than open and closed sets, and their countable unions and intersections (it is not Borel).

Why is it important?  The most important application of this result is that for transitions systems that include probabilities and “infinite non-determinism”, the complexity of bisimilarity obstructs all known techniques known to prove the logical characterization.

My personal view on this result. I was very glad to find this result, because it is a basic example of “complete analytic” relation between countable structures and thus a basic result in descriptive set theory, although hitherto not mentioned explicitly in the literature. This is independent of its application to computer science, being its initial motivation.

In some forthcoming posts I will discuss about “transitions systems that include probabilities and infinite non-determinism” and Descriptive Set Theory, one very concrete and nice chapter of Set Theory that helps measuring the complexity of various subsets in spaces.