I am trying to understand bisimulation contraction of Kripke models.
I have read these lecture slides and this Wikipedia page, but I still don't fully understand it.
I can understand that the two models below are bisimilar
In the lecture slides, the partition refinement algorithm is given as
I do understand that from the graph on the left in the first picture, the initial partition becomes
initial_partition = {
'p': ['n1', 'n2'],
'q': ['n3', 'n4']
}
or just
[['n1', 'n2'], ['n3', 'n4]]
where $n_1$ is the first node holding a $p$, $n_2$ is the node on the left also holding a $p$, $n_3$ is the last node in the left branch holding a $q$, and $n_4$ is the last node in the right branch holding a $q$.
But now I need to understand the second step in the algorithm. It seems to me that I should first loop through each of the two blocks in the initial partition, and for each node check its relations to nodes in the other blocks in the initial partition.
What I mean is that the model in the middle of this picture
shows the initial partition (consisting of 2 blocks), but I don't know what the next partition look like, and why I can suddenly remove two of the nodes.
Can someone give me an example of a larger model (more nodes), and show me the steps in reducing the larger model to a smaller model, or give me a hint on where to find literature about it where it is described more easy?
Edit
Is this correct?
From the figure above, it seems I cannot make the last partition, but as one of the nodes has a 1-transition into its own block while the other hasn't, I think it should be separated?
You don't "remove two of the nodes", you collect them into (equivalence) classes. Your state $x_1$ is the set of the two top-left states of the original transition system, and $x_2$ is the set consisting of the two others.
For the next step, note that $x_2$ can take no transition whereas $x_1$ can, so by the algorithm you can not collect them into one. Hence the next step will look the same, so your algorithm terminates, and $x_1$ and $x_2$ are your equivalence classes.
This also makes sense intuitively, since both the bottom-right states can do nothing, and hence have the same behaviour, whereas the top-left two states both can do am arbitrary number of $\pi_1$ transitions, then do exactly one $\pi_2$ transition, and then nothing, so they also have the same behaviour.
Let me try an example. Let $S = \{x_1,x_2,x_3,x_4,x_5\}$ be the state space, $\rightarrow = \{(x_1,a,x_2),(x_1,b,x_3),(x_2,a,x_2),(x_3,a,x_4),(x_3,b,x_5),(x_4,a,x_4),(x_5,a,x_5),(x_5,b,x_5)\}$ be the transition relation, and let all states have the same valuation (for simplicity). Then we start with the partition $$\Pi_1 = \{\{x_1,x_2,x_3,x_4,x_5\}\}$$ where all the states are lumped together. Now, $x_2$ and $x_4$ can both always do an $a$-transition to a state, but no $b$-transitions, whereas the remaining states can do both $a$- and $b$-transitions, so we split the state space as $$\Pi_2 = \{\{x_1,x_3,x_5\},\{x_2,x_4\}\}.$$ Next, $x_5$ can do an $a$-transition into the class $\{x_1,x_3,x_5\}$, but $x_1$ and $x_3$ can not, since their $a$-transitions go into the class $\{x_2,x_4\}$. Hence these should again be split, so we get $$\Pi_3 = \{\{x_1,x_3\},\{x_5\},\{x_2,x_4\}\}.$$ Now it should come as no surprise that $x_3$ can do a $b$-transition into the class $\{x_5\}$, but $x_1$ can not, so they must also be split, so we get $$\Pi_4 = \{\{x_1\},\{x_3\},\{x_5\},\{x_2,x_4\}\},$$ and if you do one more step, you will see that $\Pi_4 = \Pi_5$, so this is the result. Hence, the only states that are bisimilar are $x_2$ and $x_4$, because they share an equivalence class, whereas the rest all have different behaviour, as you should easily be able to convince yourself if you do a drawing of the transition system and look at what's going on.